diff --git a/.travis.yml b/.travis.yml index 52d548e3de2..6987a0b55d7 100644 --- a/.travis.yml +++ b/.travis.yml @@ -38,6 +38,13 @@ jobs: script: scripts/travis_lint.sh before_cache: + - &string-table-check + stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test + env: NAME="string-table" + install: + script: scripts/string_table_check.sh + before_cache: + - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test env: NAME="DOXYGEN-CHECK" addons: diff --git a/scripts/string_table_check.sh b/scripts/string_table_check.sh new file mode 100755 index 00000000000..5bf6d4b2dd2 --- /dev/null +++ b/scripts/string_table_check.sh @@ -0,0 +1,30 @@ +#!/bin/bash + +whitelist=" \ +" + +cleanup() +{ + rm -f "$ids_file" +} + +ids_file=$(mktemp) + +trap cleanup EXIT + +gcc -E -P -x c src/util/irep_ids.def \ + -D'IREP_ID_ONE(x)=ID_ ## x' -D'IREP_ID_TWO(x,y)=ID_ ## x' > $ids_file + +for w in $whitelist +do + perl -p -i -e "s/^$w\n//" $ids_file +done + +for i in $(<$ids_file) +do + if ! git grep -w -q -c -F $i + then + echo "$i is never used" + exit 1 + fi +done diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index afc841da20b..647e1e14e46 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -839,11 +839,11 @@ exprt cpp_typecheck_resolvet::do_builtin( << ": " << original_scope->prefix << messaget::eom; } - else if(base_name=="size_t") + else if(base_name == ID_size_t) { dest=type_exprt(size_type()); } - else if(base_name=="ssize_t") + else if(base_name == ID_ssize_t) { dest=type_exprt(signed_size_type()); } diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp index 0a514d04487..d93032a33aa 100644 --- a/src/goto-programs/remove_asm.cpp +++ b/src/goto-programs/remove_asm.cpp @@ -195,7 +195,7 @@ void remove_asmt::process_instruction( { gcc_asm_function_call("__asm_"+id2string(command), code, tmp_dest); } - else if(command=="sync") // Power + else if(command == ID_sync) // Power { goto_programt::targett t=tmp_dest.add_instruction(OTHER); t->source_location=code.source_location(); @@ -210,7 +210,7 @@ void remove_asmt::process_instruction( t->code.set(ID_RRcumul, true); t->code.set(ID_WRcumul, true); } - else if(command=="lwsync") // Power + else if(command == ID_lwsync) // Power { goto_programt::targett t=tmp_dest.add_instruction(OTHER); t->source_location=code.source_location(); @@ -223,7 +223,7 @@ void remove_asmt::process_instruction( t->code.set(ID_RWcumul, true); t->code.set(ID_RRcumul, true); } - else if(command=="isync") // Power + else if(command == ID_isync) // Power { goto_programt::targett t=tmp_dest.add_instruction(OTHER); t->source_location=code.source_location(); diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp index 5218870e96f..9fe0036911d 100644 --- a/src/goto-symex/slice_by_trace.cpp +++ b/src/goto-symex/slice_by_trace.cpp @@ -244,7 +244,7 @@ void symex_slice_by_tracet::compute_ts_back( !i->io_args.empty() && i->io_args.front().id()=="trace_event") { - irep_idt event=i->io_args.front().get("event"); + irep_idt event = i->io_args.front().get(ID_event); if(!alphabet.empty()) { diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 39bb7c0d519..d52bb8eafa1 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -774,7 +774,7 @@ exprt smt2_parsert::function_application() } else if(id=="rotate_left" || id=="rotate_right" || - id=="repeat" || + id == ID_repeat || id=="sign_extend" || id=="zero_extend") { @@ -826,7 +826,7 @@ exprt smt2_parsert::function_application() return typecast_exprt(op[0], unsigned_type); } - else if(id=="repeat") + else if(id == ID_repeat) { return nil_exprt(); } diff --git a/src/util/irep_ids.cpp b/src/util/irep_ids.cpp index 5151cd92fed..5a6bc4e525d 100644 --- a/src/util/irep_ids.cpp +++ b/src/util/irep_ids.cpp @@ -27,6 +27,14 @@ const char *irep_ids_table[]= #ifdef USE_DSTRING +enum class idt:unsigned +{ +#define IREP_ID_ONE(the_id) id_##the_id, +#define IREP_ID_TWO(the_id, str) id_##the_id, + +#include "irep_ids.def" // NOLINT(build/include) +}; + #define IREP_ID_ONE(the_id) \ const dstringt ID_##the_id=dstringt::make_from_table_index( \ static_cast(idt::id_##the_id)); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 4f68f78051c..78ff9b00e16 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -1,4 +1,5 @@ -/// \file List of irep id names and values. +/// \file +/// List of irep id names and values. /// For an explanation of how this works, see irep_ids.h. IREP_ID_TWO(empty_string, ) @@ -34,7 +35,6 @@ IREP_ID_ONE(dynamic_cast) IREP_ID_ONE(const_cast) IREP_ID_ONE(reinterpret_cast) IREP_ID_ONE(index) -IREP_ID_ONE(index_range) IREP_ID_ONE(ptrmember) IREP_ID_ONE(member) IREP_ID_ONE(member_name) @@ -47,7 +47,6 @@ IREP_ID_ONE(nand) IREP_ID_ONE(or) IREP_ID_ONE(nor) IREP_ID_ONE(xor) -IREP_ID_ONE(xnor) IREP_ID_ONE(not) IREP_ID_ONE(bitand) IREP_ID_ONE(bitor) @@ -61,7 +60,6 @@ IREP_ID_ONE(if) IREP_ID_ONE(symbol) IREP_ID_ONE(next_symbol) IREP_ID_ONE(nondet_symbol) -IREP_ID_ONE(predicate) IREP_ID_ONE(predicate_symbol) IREP_ID_ONE(predicate_next_symbol) IREP_ID_ONE(nondet_bool) @@ -148,13 +146,6 @@ IREP_ID_ONE(range) IREP_ID_ONE(from) IREP_ID_ONE(to) IREP_ID_ONE(module) -IREP_ID_ONE(module_instance) -IREP_ID_ONE(macromodule) -IREP_ID_ONE(primitive_module_instance) -IREP_ID_ONE(module_items) -IREP_ID_ONE(module_source) -IREP_ID_ONE(parameter_decl) -IREP_ID_ONE(local_parameter_decl) IREP_ID_ONE(parameter) IREP_ID_ONE(component_name) IREP_ID_ONE(component_number) @@ -170,13 +161,9 @@ IREP_ID_ONE(width) IREP_ID_ONE(components) IREP_ID_ONE(bv) IREP_ID_ONE(f) -IREP_ID_ONE(ports) -IREP_ID_ONE(port) -IREP_ID_ONE(offset) IREP_ID_ONE(with) IREP_ID_ONE(trans) IREP_ID_ONE(throw) -IREP_ID_ONE(catch) IREP_ID_ONE(try_catch) IREP_ID_ONE(noexcept) IREP_ID_ONE(CPROVER_throw) @@ -193,7 +180,6 @@ IREP_ID_ONE(constexpr) IREP_ID_ONE(inline) IREP_ID_ONE(forall) IREP_ID_ONE(exists) -IREP_ID_ONE(forever) IREP_ID_ONE(repeat) IREP_ID_ONE(extractbit) IREP_ID_ONE(extractbits) @@ -222,8 +208,6 @@ IREP_ID_ONE(java_string_literal) IREP_ID_ONE(printf) IREP_ID_ONE(input) IREP_ID_ONE(output) -IREP_ID_ONE(output_register) -IREP_ID_ONE(inout) IREP_ID_ONE(nondet) IREP_ID_ONE(NULL) IREP_ID_ONE(null) @@ -280,7 +264,6 @@ IREP_ID_ONE(ptr64) IREP_ID_ONE(char) IREP_ID_ONE(short) IREP_ID_ONE(long) -IREP_ID_ONE(longlong) IREP_ID_ONE(float) IREP_ID_ONE(double) IREP_ID_ONE(byte) @@ -299,9 +282,6 @@ IREP_ID_ONE(unsigned_long_long_int) IREP_ID_ONE(signed_int128) IREP_ID_ONE(unsigned_int128) IREP_ID_ONE(case) -IREP_ID_ONE(casex) -IREP_ID_ONE(casez) -IREP_ID_ONE(case_item) IREP_ID_TWO(C_inlined, #inlined) IREP_ID_TWO(C_hide, #hide) IREP_ID_ONE(hide) @@ -322,22 +302,6 @@ IREP_ID_ONE(bv_literals) IREP_ID_ONE(isfinite) IREP_ID_ONE(isinf) IREP_ID_ONE(isnormal) -IREP_ID_ONE(AG) -IREP_ID_ONE(AF) -IREP_ID_ONE(AX) -IREP_ID_ONE(EG) -IREP_ID_ONE(EF) -IREP_ID_ONE(EX) -IREP_ID_ONE(U) -IREP_ID_ONE(R) -IREP_ID_ONE(A) -IREP_ID_ONE(F) -IREP_ID_ONE(E) -IREP_ID_ONE(G) -IREP_ID_ONE(X) -IREP_ID_ONE(continuous_assign) -IREP_ID_ONE(blocking_assign) -IREP_ID_ONE(non_blocking_assign) IREP_ID_ONE(alignof) IREP_ID_ONE(clang_builtin_convertvector) IREP_ID_ONE(gcc_builtin_va_arg) @@ -353,11 +317,6 @@ IREP_ID_ONE(gcc_decimal128) IREP_ID_ONE(builtin_offsetof) IREP_ID_ONE(0) IREP_ID_ONE(1) -IREP_ID_ONE(8) -IREP_ID_ONE(16) -IREP_ID_ONE(32) -IREP_ID_ONE(64) -IREP_ID_ONE(128) IREP_ID_ONE(sizeof) IREP_ID_ONE(type_arg) IREP_ID_ONE(expr_arg) @@ -382,11 +341,9 @@ IREP_ID_TWO(mult, *) IREP_ID_TWO(div, /) IREP_ID_TWO(power, **) IREP_ID_ONE(factorial_power) -IREP_ID_ONE(component) IREP_ID_ONE(pretty_name) IREP_ID_TWO(C_class, #class) IREP_ID_TWO(C_interface, #interface) -IREP_ID_ONE(interface) IREP_ID_ONE(targets) IREP_ID_ONE(location) IREP_ID_ONE(labels) @@ -396,7 +353,6 @@ IREP_ID_ONE(designated_initializer) IREP_ID_ONE(designator) IREP_ID_ONE(member_designator) IREP_ID_ONE(index_designator) -IREP_ID_ONE(offset_designator) IREP_ID_TWO(C_constant, #constant) IREP_ID_TWO(C_volatile, #volatile) IREP_ID_TWO(C_restricted, #restricted) @@ -411,7 +367,6 @@ IREP_ID_ONE(byte_extract_little_endian) IREP_ID_ONE(byte_update_big_endian) IREP_ID_ONE(byte_update_little_endian) IREP_ID_ONE(replication) -IREP_ID_ONE(dummy) IREP_ID_ONE(init) IREP_ID_ONE(cprover_atomic) IREP_ID_ONE(atomic) @@ -424,18 +379,10 @@ IREP_ID_ONE(specc_notify) IREP_ID_ONE(specc_par) IREP_ID_ONE(specc_wait) IREP_ID_ONE(specc_event) -IREP_ID_ONE(bp_enforce) -IREP_ID_ONE(bp_abortif) -IREP_ID_ONE(bp_constrain) -IREP_ID_ONE(bp_schoose) -IREP_ID_ONE(bp_dead) -IREP_ID_ONE(instance) -IREP_ID_ONE(cover) IREP_ID_ONE(coverage_criterion) IREP_ID_ONE(initializer) IREP_ID_ONE(anonymous) IREP_ID_TWO(C_is_anonymous, #is_anonymous) -IREP_ID_ONE(is_macro) IREP_ID_ONE(is_enum_constant) IREP_ID_ONE(is_inline) IREP_ID_ONE(is_extern) @@ -475,34 +422,14 @@ IREP_ID_ONE(typename) IREP_ID_ONE(C) IREP_ID_ONE(cpp) IREP_ID_ONE(java) -IREP_ID_ONE(SpecC) -IREP_ID_ONE(SystemC) IREP_ID_ONE(decl_block) IREP_ID_ONE(decl_type) -IREP_ID_ONE(genvar) -IREP_ID_ONE(realtime) IREP_ID_ONE(parameters) -IREP_ID_ONE(parameter_assignments) -IREP_ID_ONE(named_parameter_assignment) -IREP_ID_ONE(specify) -IREP_ID_ONE(pullup) -IREP_ID_ONE(pulldown) -IREP_ID_ONE(automatic) -IREP_ID_ONE(rcmos) -IREP_ID_ONE(cmos) -IREP_ID_ONE(nmos) -IREP_ID_ONE(pmos) -IREP_ID_ONE(rnmos) -IREP_ID_ONE(rpmos) IREP_ID_ONE(wchar_t) IREP_ID_ONE(char16_t) IREP_ID_ONE(char32_t) IREP_ID_ONE(size_t) IREP_ID_ONE(ssize_t) -IREP_ID_ONE(inst) -IREP_ID_ONE(inst_builtin) -IREP_ID_ONE(always) -IREP_ID_ONE(initial) IREP_ID_ONE(mode) IREP_ID_ONE(this) IREP_ID_TWO(C_this, #this) @@ -514,7 +441,6 @@ IREP_ID_ONE(reduction_xor) IREP_ID_ONE(reduction_xnor) IREP_ID_TWO(C_zero_initializer, #zero_initializer) IREP_ID_ONE(body) -IREP_ID_ONE(entity) IREP_ID_ONE(temporary_object) IREP_ID_TWO(overflow_plus, overflow-+) IREP_ID_TWO(overflow_minus, overflow--) @@ -531,10 +457,7 @@ IREP_ID_ONE(static_object) IREP_ID_ONE(stack_object) IREP_ID_TWO(C_is_failed_symbol, #is_failed_symbol) IREP_ID_TWO(C_failed_symbol, #failed_symbol) -IREP_ID_ONE(list) -IREP_ID_ONE(map) IREP_ID_ONE(set) -IREP_ID_ONE(storage) IREP_ID_ONE(friend) IREP_ID_ONE(explicit) IREP_ID_ONE(storage_spec) @@ -548,21 +471,6 @@ IREP_ID_ONE(aligned) IREP_ID_TWO(C_alignment, #alignment) IREP_ID_ONE(vector) IREP_ID_ONE(abstract) -IREP_ID_ONE(bit) -IREP_ID_ONE(logic) -IREP_ID_ONE(chandle) -IREP_ID_ONE(reg) -IREP_ID_ONE(wire) -IREP_ID_ONE(tri) -IREP_ID_ONE(tri1) -IREP_ID_ONE(supply0) -IREP_ID_ONE(wand) -IREP_ID_ONE(triand) -IREP_ID_ONE(tri0) -IREP_ID_ONE(supply1) -IREP_ID_ONE(wor) -IREP_ID_ONE(trior) -IREP_ID_ONE(trireg) IREP_ID_ONE(function_application) IREP_ID_ONE(cpp_declarator) IREP_ID_ONE(cpp_linkage_spec) @@ -576,57 +484,12 @@ IREP_ID_TWO(C_c_type, #c_type) IREP_ID_ONE(namespace) IREP_ID_ONE(linkage) IREP_ID_ONE(decltype) -IREP_ID_ONE(buf) -IREP_ID_ONE(bufif0) -IREP_ID_ONE(bufif1) -IREP_ID_ONE(notif0) -IREP_ID_ONE(notif1) -IREP_ID_ONE(task) -IREP_ID_TWO(C_little_endian, #little_endian) -IREP_ID_TWO(C_offset, #offset) IREP_ID_TWO(C_tag_only_declaration, #tag_only_declaration) IREP_ID_ONE(struct_tag) IREP_ID_ONE(union_tag) IREP_ID_ONE(c_enum_tag) -IREP_ID_ONE(enum_constant) -IREP_ID_ONE(bit_select) -IREP_ID_ONE(part_select) -IREP_ID_ONE(indexed_part_select_plus) -IREP_ID_ONE(indexed_part_select_minus) -IREP_ID_ONE(generate_block) -IREP_ID_ONE(generate_assign) -IREP_ID_ONE(generate_skip) -IREP_ID_ONE(generate_case) -IREP_ID_ONE(generate_if) -IREP_ID_ONE(generate_for) -IREP_ID_ONE(delay) -IREP_ID_ONE(verilog_cycle_delay) -IREP_ID_ONE(sva_cycle_delay) -IREP_ID_ONE(sva_sequence_throughout) -IREP_ID_ONE(sva_sequence_concatenation) -IREP_ID_ONE(sva_sequence_first_match) -IREP_ID_ONE(sva_always) -IREP_ID_ONE(sva_nexttime) -IREP_ID_ONE(sva_s_nexttime) -IREP_ID_ONE(sva_eventually) -IREP_ID_ONE(sva_s_eventually) -IREP_ID_ONE(sva_until) -IREP_ID_ONE(sva_s_until) -IREP_ID_ONE(sva_until_with) -IREP_ID_ONE(sva_s_until_with) -IREP_ID_ONE(sva_overlapped_implication) -IREP_ID_ONE(sva_non_overlapped_implication) -IREP_ID_ONE(hierarchical_identifier) -IREP_ID_ONE(named_port_connection) -IREP_ID_ONE(named_block) -IREP_ID_ONE(verilog_primitive_module) -IREP_ID_ONE(verilog_module) IREP_ID_ONE(verilog_case_equality) IREP_ID_ONE(verilog_case_inequality) -IREP_ID_ONE(event_guard) -IREP_ID_ONE(posedge) -IREP_ID_ONE(negedge) -IREP_ID_ONE(pointer_and_address_pair) IREP_ID_ONE(user_specified_predicate) IREP_ID_ONE(user_specified_parameter_predicates) IREP_ID_ONE(user_specified_return_predicates) @@ -644,13 +507,9 @@ IREP_ID_ONE(msc_if_not_exists) IREP_ID_ONE(msc_underlying_type) IREP_ID_ONE(msc_based) IREP_ID_ONE(alias) -IREP_ID_ONE(auto_object) -IREP_ID_ONE(ssa_object) IREP_ID_ONE(ptr_object) IREP_ID_TWO(C_c_sizeof_type, #c_sizeof_type) IREP_ID_ONE(array_update) -IREP_ID_ONE(struct_update) -IREP_ID_ONE(union_update) IREP_ID_ONE(update) IREP_ID_ONE(float_debug1) IREP_ID_ONE(float_debug2) @@ -659,10 +518,7 @@ IREP_ID_ONE(gcc_attribute_mode) IREP_ID_TWO(built_in, ) IREP_ID_ONE(exception_list) IREP_ID_ONE(exception_id) -IREP_ID_ONE(priority) IREP_ID_ONE(predicate_passive_symbol) -IREP_ID_ONE(all) -IREP_ID_ONE(when) IREP_ID_ONE(cw_va_arg_typeof) IREP_ID_ONE(fence) IREP_ID_ONE(sync) @@ -676,7 +532,6 @@ IREP_ID_ONE(RRcumul) IREP_ID_ONE(RWcumul) IREP_ID_ONE(WWcumul) IREP_ID_ONE(WRcumul) -IREP_ID_ONE(claim) IREP_ID_ONE(generic_selection) IREP_ID_ONE(generic_associations) IREP_ID_ONE(generic_association) @@ -685,13 +540,7 @@ IREP_ID_ONE(floatbv_minus) IREP_ID_ONE(floatbv_mult) IREP_ID_ONE(floatbv_div) IREP_ID_ONE(floatbv_rem) -IREP_ID_ONE(floatbv_sin) -IREP_ID_ONE(floatbv_cos) IREP_ID_ONE(floatbv_typecast) -IREP_ID_ONE(read) -IREP_ID_ONE(write) -IREP_ID_ONE(native) -IREP_ID_ONE(final) IREP_ID_ONE(compound_literal) IREP_ID_ONE(custom_bv) IREP_ID_ONE(custom_unsignedbv) @@ -699,7 +548,6 @@ IREP_ID_ONE(custom_signedbv) IREP_ID_ONE(custom_fixedbv) IREP_ID_ONE(custom_floatbv) IREP_ID_TWO(C_SSA_symbol, #SSA_symbol) -IREP_ID_TWO(C_full_identifier, #full_identifier) IREP_ID_ONE(L0) IREP_ID_ONE(L1) IREP_ID_ONE(L2) @@ -707,26 +555,12 @@ IREP_ID_ONE(L1_object_identifier) IREP_ID_ONE(already_typechecked) IREP_ID_TWO(C_va_arg_type, #va_arg_type) IREP_ID_ONE(smt2_symbol) -IREP_ID_ONE(VHDL) -IREP_ID_ONE(Verilog) -IREP_ID_ONE(verilog_realtime) IREP_ID_ONE(onehot) IREP_ID_ONE(onehot0) -IREP_ID_ONE(verilog_star_event) -IREP_ID_ONE(verilog_attribute) -IREP_ID_ONE(time) -IREP_ID_ONE(fork) -IREP_ID_ONE(disable) -IREP_ID_ONE(wait) -IREP_ID_ONE(deassign) -IREP_ID_ONE(force) -IREP_ID_ONE(release) IREP_ID_ONE(popcount) IREP_ID_ONE(function_type) IREP_ID_ONE(noreturn) IREP_ID_TWO(C_noreturn, #noreturn) -IREP_ID_ONE(process) -IREP_ID_ONE(signal) IREP_ID_ONE(weak) IREP_ID_ONE(is_weak) IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant) @@ -736,13 +570,6 @@ IREP_ID_ONE(virtual_function) IREP_ID_TWO(C_element_type, #element_type) IREP_ID_ONE(working_directory) IREP_ID_ONE(section) -IREP_ID_ONE(msb) -IREP_ID_ONE(lsb) -IREP_ID_ONE(verilog_signed_vector) -IREP_ID_ONE(verilog_unsigned_vector) -IREP_ID_ONE(verilog_array) -IREP_ID_ONE(low) -IREP_ID_ONE(high) IREP_ID_ONE(bswap) IREP_ID_ONE(java_bytecode_index) IREP_ID_ONE(java_instanceof) @@ -758,7 +585,6 @@ IREP_ID_ONE(cprover_associate_array_to_pointer_func) IREP_ID_ONE(cprover_associate_length_to_array_func) IREP_ID_ONE(cprover_char_literal_func) IREP_ID_ONE(cprover_string_literal_func) -IREP_ID_ONE(cprover_string_array_of_char_pointer_func) IREP_ID_ONE(cprover_string_char_at_func) IREP_ID_ONE(cprover_string_char_set_func) IREP_ID_ONE(cprover_string_code_point_at_func) @@ -794,13 +620,11 @@ IREP_ID_ONE(cprover_string_insert_bool_func) IREP_ID_ONE(cprover_string_insert_char_func) IREP_ID_ONE(cprover_string_insert_float_func) IREP_ID_ONE(cprover_string_insert_double_func) -IREP_ID_ONE(cprover_string_insert_char_array_func) IREP_ID_ONE(cprover_string_is_prefix_func) IREP_ID_ONE(cprover_string_is_suffix_func) IREP_ID_ONE(cprover_string_is_empty_func) IREP_ID_ONE(cprover_string_last_index_of_func) IREP_ID_ONE(cprover_string_length_func) -IREP_ID_ONE(cprover_string_data_func) IREP_ID_ONE(cprover_string_of_int_func) IREP_ID_ONE(cprover_string_of_int_hex_func) IREP_ID_ONE(cprover_string_of_long_func) @@ -809,17 +633,14 @@ IREP_ID_ONE(cprover_string_of_float_func) IREP_ID_ONE(cprover_string_of_float_scientific_notation_func) IREP_ID_ONE(cprover_string_of_double_func) IREP_ID_ONE(cprover_string_of_char_func) -IREP_ID_ONE(cprover_string_of_char_array_func) IREP_ID_ONE(cprover_string_parse_int_func) IREP_ID_ONE(cprover_string_replace_func) IREP_ID_ONE(cprover_string_set_length_func) IREP_ID_ONE(cprover_string_startswith_func) IREP_ID_ONE(cprover_string_substring_func) -IREP_ID_ONE(cprover_string_to_char_array_func) IREP_ID_ONE(cprover_string_to_lower_case_func) IREP_ID_ONE(cprover_string_to_upper_case_func) IREP_ID_ONE(cprover_string_trim_func) -IREP_ID_ONE(cprover_string_value_of_func) IREP_ID_ONE(skip_initialize) IREP_ID_ONE(basic_block_covered_lines) IREP_ID_ONE(is_nondet_nullable) @@ -831,7 +652,6 @@ IREP_ID_ONE(integer_dereference) IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter) IREP_ID_TWO(C_java_generic_type, #java_generic_type) IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) -IREP_ID_TWO(C_specialized_generic_java_class, #specialized_generic_java_class) IREP_ID_TWO(C_java_implicitly_generic_class_type, #java_implicitly_generic_class_type) IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol) IREP_ID_TWO(generic_types, #generic_types) @@ -846,5 +666,13 @@ IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation) IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation) IREP_ID_ONE(annotations) +// Projects depending on this code base that wish to extend the list of +// available ids should provide a file local_irep_ids.h in their source tree and +// add -D'LOCAL_IREP_IDS=' to their compiler command +// line. +#ifdef LOCAL_IREP_IDS +#include LOCAL_IREP_IDS +#endif + #undef IREP_ID_ONE #undef IREP_ID_TWO diff --git a/src/util/irep_ids.h b/src/util/irep_ids.h index 2fec6ff4114..7d946bed305 100644 --- a/src/util/irep_ids.h +++ b/src/util/irep_ids.h @@ -33,14 +33,6 @@ Author: Reuben Thomas, reuben.thomas@me.com /// into a const extern irep_idt with the variable name `ID_param` and the /// string value `"contents"`. -enum class idt:unsigned -{ -#define IREP_ID_ONE(the_id) id_##the_id, -#define IREP_ID_TWO(the_id, str) id_##the_id, - -#include "irep_ids.def" -}; - #ifdef USE_DSTRING #define IREP_ID_ONE(the_id) extern const dstringt ID_##the_id; @@ -53,6 +45,6 @@ enum class idt:unsigned #endif -#include "irep_ids.def" // NOLINT(build/include) +#include "irep_ids.def" #endif diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 652fe422c56..95676c17dfc 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -73,86 +73,6 @@ std::ostream &operator<<(std::ostream &out, return out; } -irept symbolt::to_irep() const -{ - irept dest; - - dest.clear(); - dest.add(ID_type)=type; - dest.add(ID_value)=value; - dest.add(ID_location)=location; - dest.set(ID_name, name); - dest.set(ID_module, module); - dest.set(ID_base_name, base_name); - dest.set(ID_mode, mode); - dest.set(ID_pretty_name, pretty_name); - - if(is_type) - dest.set("is_type", true); - if(is_macro) - dest.set("is_macro", true); - if(is_exported) - dest.set("is_exported", true); - if(is_input) - dest.set("is_input", true); - if(is_output) - dest.set("is_output", true); - if(is_state_var) - dest.set("is_statevar", true); - if(is_parameter) - dest.set("is_parameter", true); - if(is_auxiliary) - dest.set("is_auxiliary", true); - if(is_weak) - dest.set("is_weak", true); - if(is_property) - dest.set("is_property", true); - if(is_lvalue) - dest.set("is_lvalue", true); - if(is_static_lifetime) - dest.set("is_static_lifetime", true); - if(is_thread_local) - dest.set("is_thread_local", true); - if(is_file_local) - dest.set("is_file_local", true); - if(is_extern) - dest.set("is_extern", true); - if(is_volatile) - dest.set("is_volatile", true); - - return dest; -} - -void symbolt::from_irep(const irept &src) -{ - type=static_cast(src.find(ID_type)); - value=static_cast(src.find(ID_value)); - location=static_cast(src.find(ID_location)); - - name=src.get(ID_name); - module=src.get(ID_module); - base_name=src.get(ID_base_name); - mode=src.get(ID_mode); - pretty_name=src.get(ID_pretty_name); - - is_type=src.get_bool("is_type"); - is_macro=src.get_bool("is_macro"); - is_exported=src.get_bool("is_exported"); - is_input=src.get_bool("is_input"); - is_output=src.get_bool("is_output"); - is_state_var=src.get_bool("is_state_var"); - is_parameter=src.get_bool("is_parameter"); - is_auxiliary=src.get_bool("is_auxiliary"); - is_weak=src.get_bool("is_weak"); - is_property=src.get_bool("property"); - is_lvalue=src.get_bool("lvalue"); - is_static_lifetime=src.get_bool("static_lifetime"); - is_thread_local=src.get_bool("thread_local"); - is_file_local=src.get_bool("file_local"); - is_extern=src.get_bool("is_extern"); - is_volatile=src.get_bool("is_volatile"); -} - void symbolt::swap(symbolt &b) { #define SYM_SWAP1(x) x.swap(b.x) diff --git a/src/util/symbol.h b/src/util/symbol.h index ca26306d6bf..078f80ad7b2 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -91,10 +91,6 @@ class symbolt void swap(symbolt &b); void show(std::ostream &out) const; - // serialization - irept to_irep() const; - void from_irep(const irept &src); - class symbol_exprt symbol_expr() const; bool is_shared() const