From 4a02c7518f3dd4b3fc547ed35b60b974c1199d02 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Oct 2018 07:28:33 +0000 Subject: [PATCH 1/3] Use CPROVER_PREFIX macro instead of hardcoded __CPROVER_ string Using string literals is prone to typos and sometimes, but not always, using the CPROVER_PREFIX macro removes the potential for central modifications. Fixes: #735 --- .../java_bytecode_internal_additions.cpp | 4 +- .../gen_nondet_string_init.cpp | 4 +- src/analyses/custom_bitvector_analysis.cpp | 17 ++-- src/analyses/escape_analysis.cpp | 14 ++-- src/ansi-c/ansi_c_internal_additions.cpp | 77 +++++++++---------- src/ansi-c/c_typecheck_base.cpp | 2 +- src/ansi-c/c_typecheck_type.cpp | 4 +- src/ansi-c/cprover_library.cpp | 2 +- src/ansi-c/expr2c.cpp | 28 +++---- src/ansi-c/scanner.l | 42 +++++----- src/cpp/cpp_convert_type.cpp | 2 +- src/cpp/cpp_internal_additions.cpp | 55 ++++++------- src/goto-cc/linker_script_merge.cpp | 9 ++- .../cover_instrument_other.cpp | 2 +- src/goto-instrument/dump_c.cpp | 2 +- .../goto_instrument_parse_options.cpp | 5 +- src/goto-instrument/goto_program2code.cpp | 26 ++++--- src/goto-instrument/model_argc_argv.cpp | 2 +- .../thread_instrumentation.cpp | 4 +- src/goto-programs/goto_convert.cpp | 2 +- src/goto-programs/goto_convert_functions.cpp | 2 +- src/goto-programs/goto_inline_class.cpp | 12 +-- src/goto-programs/read_bin_goto_object.cpp | 2 +- src/goto-programs/slice_global_inits.cpp | 3 +- src/jsil/jsil_internal_additions.cpp | 4 +- src/linking/static_lifetime_init.cpp | 2 +- src/solvers/flattening/boolbv_index.cpp | 11 ++- unit/path_strategies.cpp | 2 +- 28 files changed, 181 insertions(+), 160 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp index 1fc8e06b4b2..02e4e7f5dd8 100644 --- a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp @@ -21,7 +21,7 @@ void java_internal_additions(symbol_table_baset &dest) { symbolt symbol; - symbol.base_name="__CPROVER_rounding_mode"; + symbol.base_name = CPROVER_PREFIX "rounding_mode"; symbol.name=CPROVER_PREFIX "rounding_mode"; symbol.type=signed_int_type(); symbol.mode=ID_C; @@ -35,7 +35,7 @@ void java_internal_additions(symbol_table_baset &dest) { symbolt symbol; - symbol.base_name="__CPROVER_malloc_object"; + symbol.base_name = CPROVER_PREFIX "malloc_object"; symbol.name=CPROVER_PREFIX "malloc_object"; symbol.type=pointer_type(empty_typet()); symbol.mode=ID_C; diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 53cc0e7f5ef..6aceb495460 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -80,8 +80,8 @@ SCENARIO( const std::vector reference_code = { // NOLINT "int tmp_object_factory;", "tmp_object_factory = NONDET(int);", - "__CPROVER_assume(tmp_object_factory >= 0);", - "__CPROVER_assume(tmp_object_factory <= 20);", + CPROVER_PREFIX "assume(tmp_object_factory >= 0);", + CPROVER_PREFIX "assume(tmp_object_factory <= 20);", "char (*string_data_pointer)[INFINITY()];", "string_data_pointer = " "ALLOCATE(char [INFINITY()], INFINITY(), false);", diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 059756107e4..9cf4ace1324 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -320,10 +320,11 @@ void custom_bitvector_domaint::transform( { const irep_idt &identifier=to_symbol_expr(function).get_identifier(); - if(identifier=="__CPROVER_set_must" || - identifier=="__CPROVER_clear_must" || - identifier=="__CPROVER_set_may" || - identifier=="__CPROVER_clear_may") + if( + identifier == CPROVER_PREFIX "set_must" || + identifier == CPROVER_PREFIX "clear_must" || + identifier == CPROVER_PREFIX "set_may" || + identifier == CPROVER_PREFIX "clear_may") { if(code_function_call.arguments().size()==2) { @@ -333,13 +334,13 @@ void custom_bitvector_domaint::transform( // initialize to make Visual Studio happy modet mode = modet::SET_MUST; - if(identifier=="__CPROVER_set_must") + if(identifier == CPROVER_PREFIX "set_must") mode=modet::SET_MUST; - else if(identifier=="__CPROVER_clear_must") + else if(identifier == CPROVER_PREFIX "clear_must") mode=modet::CLEAR_MUST; - else if(identifier=="__CPROVER_set_may") + else if(identifier == CPROVER_PREFIX "set_may") mode=modet::SET_MAY; - else if(identifier=="__CPROVER_clear_may") + else if(identifier == CPROVER_PREFIX "clear_may") mode=modet::CLEAR_MAY; else UNREACHABLE; diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 2c4cdab1d5a..c6ff1cd49ed 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -11,16 +11,20 @@ Author: Daniel Kroening, kroening@kroening.com #include "escape_analysis.h" +#include #include bool escape_domaint::is_tracked(const symbol_exprt &symbol) { const irep_idt &identifier=symbol.get_identifier(); - if(identifier=="__CPROVER_memory_leak" || - identifier=="__CPROVER_malloc_object" || - identifier=="__CPROVER_dead_object" || - identifier=="__CPROVER_deallocated") + if( + identifier == CPROVER_PREFIX "memory_leak" || + identifier == CPROVER_PREFIX "malloc_object" || + identifier == CPROVER_PREFIX "dead_object" || + identifier == CPROVER_PREFIX "deallocated") + { return false; + } return true; } @@ -217,7 +221,7 @@ void escape_domaint::transform( if(function.id()==ID_symbol) { const irep_idt &identifier=to_symbol_expr(function).get_identifier(); - if(identifier=="__CPROVER_cleanup") + if(identifier == CPROVER_PREFIX "cleanup") { if(code_function_call.arguments().size()==2) { diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index b693b4a39d8..c0145b1f01c 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -109,17 +109,15 @@ const char windows_builtin_headers[]= static std::string architecture_string(const std::string &value, const char *s) { - return std::string("const char *__CPROVER_architecture_")+ - std::string(s)+ - "=\""+value+"\";\n"; + return std::string("const char *" CPROVER_PREFIX "architecture_") + + std::string(s) + "=\"" + value + "\";\n"; } template static std::string architecture_string(T value, const char *s) { - return std::string("const int __CPROVER_architecture_")+ - std::string(s)+ - "="+std::to_string(value)+";\n"; + return std::string("const int " CPROVER_PREFIX "architecture_") + + std::string(s) + "=" + std::to_string(value) + ";\n"; } void ansi_c_internal_additions(std::string &code) @@ -127,54 +125,55 @@ void ansi_c_internal_additions(std::string &code) // do the built-in types and variables code+= "# 1 \"\"\n" - "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n" + "typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n" "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+ - " __CPROVER_ssize_t;\n" - "const unsigned __CPROVER_constant_infinity_uint;\n" - "typedef void __CPROVER_integer;\n" - "typedef void __CPROVER_rational;\n" - "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n" - // NOLINTNEXTLINE(whitespace/line_length) - "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n" - "unsigned long __CPROVER_next_thread_id=0;\n" - // NOLINTNEXTLINE(whitespace/line_length) - "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n" + " " CPROVER_PREFIX "ssize_t;\n" + "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n" + "typedef void " CPROVER_PREFIX "integer;\n" + "typedef void " CPROVER_PREFIX "rational;\n" + CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n" + CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited[" + CPROVER_PREFIX "constant_infinity_uint];\n" + "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n" + "extern unsigned char " CPROVER_PREFIX "memory[" + CPROVER_PREFIX "constant_infinity_uint];\n" // malloc - "const void *__CPROVER_deallocated=0;\n" - "const void *__CPROVER_dead_object=0;\n" - "const void *__CPROVER_malloc_object=0;\n" - "__CPROVER_size_t __CPROVER_malloc_size;\n" - "__CPROVER_bool __CPROVER_malloc_is_new_array=0;\n" // for C++ - "const void *__CPROVER_memory_leak=0;\n" - "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n" + "const void *" CPROVER_PREFIX "deallocated=0;\n" + "const void *" CPROVER_PREFIX "dead_object=0;\n" + "const void *" CPROVER_PREFIX "malloc_object=0;\n" + CPROVER_PREFIX "size_t " CPROVER_PREFIX "malloc_size;\n" + CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++ + "const void *" CPROVER_PREFIX "memory_leak=0;\n" + "void *" CPROVER_PREFIX "allocate(" + CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n" // this is ANSI-C - // NOLINTNEXTLINE(whitespace/line_length) - "extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n" + "extern " CPROVER_PREFIX "thread_local const char __func__[" + CPROVER_PREFIX "constant_infinity_uint];\n" // this is GCC - // NOLINTNEXTLINE(whitespace/line_length) - "extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n" - // NOLINTNEXTLINE(whitespace/line_length) - "extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n" + "extern " CPROVER_PREFIX "thread_local const char __FUNCTION__[" + CPROVER_PREFIX "constant_infinity_uint];\n" + "extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__[" + CPROVER_PREFIX "constant_infinity_uint];\n" // float stuff - "int __CPROVER_thread_local __CPROVER_rounding_mode="+ + "int " CPROVER_PREFIX "thread_local " CPROVER_PREFIX "rounding_mode="+ std::to_string(config.ansi_c.rounding_mode)+";\n" // pipes, write, read, close - "struct __CPROVER_pipet {\n" + "struct " CPROVER_PREFIX "pipet {\n" " _Bool widowed;\n" " char data[4];\n" " short next_avail;\n" " short next_unread;\n" "};\n" - // NOLINTNEXTLINE(whitespace/line_length) - "extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n" + "extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes[" + CPROVER_PREFIX "constant_infinity_uint];\n" // offset to make sure we don't collide with other fds - "extern const int __CPROVER_pipe_offset;\n" - "unsigned __CPROVER_pipe_count=0;\n" + "extern const int " CPROVER_PREFIX "pipe_offset;\n" + "unsigned " CPROVER_PREFIX "pipe_count=0;\n" "\n" // This function needs to be declared, or otherwise can't be called // by the entry-point construction. @@ -201,13 +200,13 @@ void ansi_c_internal_additions(std::string &code) // For clang, __float128 is a keyword. // For gcc, this is a typedef and not a keyword. if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) - code += "typedef __CPROVER_Float128 __float128;\n"; + code += "typedef " CPROVER_PREFIX "Float128 __float128;\n"; } else if(config.ansi_c.arch == "ppc64le") { // https://patchwork.ozlabs.org/patch/792295/ if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) - code += "typedef __CPROVER_Float128 __ieee128;\n"; + code += "typedef " CPROVER_PREFIX "Float128 __ieee128;\n"; } else if(config.ansi_c.arch == "hppa") { @@ -225,7 +224,7 @@ void ansi_c_internal_additions(std::string &code) // clang doesn't do __float80 // Note that __float80 is a typedef, and not a keyword. if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) - code += "typedef __CPROVER_Float64x __float80;\n"; + code += "typedef " CPROVER_PREFIX "Float64x __float80;\n"; } // On 64-bit systems, gcc has typedefs diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 9baa07bf40b..dd5c2c220a7 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -771,7 +771,7 @@ void c_typecheck_baset::typecheck_declaration( ret_type=to_code_type(new_symbol.type).return_type(); assert(parameter_map.empty()); if(ret_type.id()!=ID_empty) - parameter_map["__CPROVER_return_value"]=ret_type; + parameter_map[CPROVER_PREFIX "return_value"] = ret_type; typecheck_spec_expr(contract, ID_C_spec_ensures); parameter_map.clear(); diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 73144121d2f..b337d7da65f 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -1508,11 +1508,11 @@ void c_typecheck_baset::typecheck_typedef_type(typet &type) type.set(ID_C_alignment, alignment); // CPROVER extensions - if(symbol.base_name=="__CPROVER_rational") + if(symbol.base_name == CPROVER_PREFIX "rational") { type=rational_typet(); } - else if(symbol.base_name=="__CPROVER_integer") + else if(symbol.base_name == CPROVER_PREFIX "integer") { type=integer_typet(); } diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index 965f0ca823b..285f9b7e108 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -25,7 +25,7 @@ static std::string get_cprover_library_text( "#undef inline\n"; if(config.ansi_c.string_abstraction) - library_text << "#define __CPROVER_STRING_ABSTRACTION\n"; + library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n"; // cprover_library.inc may not have been generated when running Doxygen, thus // make Doxygen skip this part diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index dbd1665a97e..59dc8197ce9 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -213,7 +214,7 @@ std::string expr2ct::convert_rec( } else if(src.id()==ID_string) { - return q+"__CPROVER_string"+d; + return q + CPROVER_PREFIX + "string" + d; } else if(src.id()==ID_natural || src.id()==ID_integer || @@ -244,7 +245,7 @@ std::string expr2ct::convert_rec( { std::string swidth=src.get_string(ID_width); std::string fwidth=src.get_string(ID_f); - return q+"__CPROVER_floatbv["+swidth+"]["+fwidth+"]"; + return q + CPROVER_PREFIX + "floatbv[" + swidth + "][" + fwidth + "]"; } } else if(src.id()==ID_fixedbv) @@ -252,9 +253,8 @@ std::string expr2ct::convert_rec( const std::size_t width=to_fixedbv_type(src).get_width(); const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits(); - return - q+"__CPROVER_fixedbv["+std::to_string(width)+"]["+ - std::to_string(fraction_bits)+"]"+d; + return q + CPROVER_PREFIX + "fixedbv[" + std::to_string(width) + "][" + + std::to_string(fraction_bits) + "]" + d; } else if(src.id()==ID_c_bit_field) { @@ -323,8 +323,8 @@ std::string expr2ct::convert_rec( } else { - return q+sign_str+ - "__CPROVER_bitvector["+integer2string(width)+"]"+d; + return q + sign_str + CPROVER_PREFIX + "bitvector[" + + integer2string(width) + "]" + d; } } else if(src.id()==ID_struct) @@ -2982,10 +2982,10 @@ std::string expr2ct::convert_code( return convert_code_unlock(src, indent); if(statement==ID_atomic_begin) - return indent_str(indent)+"__CPROVER_atomic_begin();"; + return indent_str(indent) + CPROVER_PREFIX + "atomic_begin();"; if(statement==ID_atomic_end) - return indent_str(indent)+"__CPROVER_atomic_end();"; + return indent_str(indent) + CPROVER_PREFIX + "atomic_end();"; if(statement==ID_function_call) return convert_code_function_call(to_code_function_call(src), indent); @@ -3282,7 +3282,8 @@ std::string expr2ct::convert_code_assume( return convert_norep(src, precedence); } - return indent_str(indent)+"__CPROVER_assume("+convert(src.op0())+");"; + return indent_str(indent) + CPROVER_PREFIX + "assume(" + convert(src.op0()) + + ");"; } std::string expr2ct::convert_code_label( @@ -3551,10 +3552,10 @@ std::string expr2ct::convert_with_precedence( return convert_function(src, "POINTER_OBJECT", precedence=16); else if(src.id()=="get_must") - return convert_function(src, "__CPROVER_get_must", precedence=16); + return convert_function(src, CPROVER_PREFIX "get_must", precedence = 16); else if(src.id()=="get_may") - return convert_function(src, "__CPROVER_get_may", precedence=16); + return convert_function(src, CPROVER_PREFIX "get_may", precedence = 16); else if(src.id()=="object_value") return convert_function(src, "OBJECT_VALUE", precedence=16); @@ -3572,7 +3573,8 @@ std::string expr2ct::convert_with_precedence( return convert_function(src, "POINTER_CONS", precedence=16); else if(src.id()==ID_invalid_pointer) - return convert_function(src, "__CPROVER_invalid_pointer", precedence=16); + return convert_function( + src, CPROVER_PREFIX "invalid_pointer", precedence = 16); else if(src.id()==ID_dynamic_object) return convert_function(src, "DYNAMIC_OBJECT", precedence=16); diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index a5e3e0c818c..1695539a65f 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -222,6 +222,8 @@ s_char [^"\\\n]|{escape_sequence} char_lit ("L"|"u"|"U")?[']{c_char}+['] string_lit ("L"|"u"|"U"|"u8")?["]{s_char}*["] +CPROVER_PREFIX "__CPROVER_" + %x GRAMMAR %x COMMENT1 %x COMMENT2 @@ -492,11 +494,11 @@ void ansi_c_scanner_init() return make_identifier(); } -"__CPROVER_Float64x" { +{CPROVER_PREFIX}"Float64x" { loc(); return TOK_GCC_FLOAT64X; } -"__CPROVER_Float80" { +{CPROVER_PREFIX}"Float80" { loc(); return TOK_GCC_FLOAT80; } @@ -514,7 +516,7 @@ void ansi_c_scanner_init() return make_identifier(); } -"__CPROVER_Float128" { +{CPROVER_PREFIX}"Float128" { loc(); return TOK_GCC_FLOAT128; } @@ -1205,23 +1207,23 @@ __decltype { if(PARSER.cpp98 && return make_identifier(); } -"__CPROVER_atomic" { loc(); return TOK_CPROVER_ATOMIC; } -"__CPROVER_forall" { loc(); return TOK_FORALL; } -"__CPROVER_exists" { loc(); return TOK_EXISTS; } -"__CPROVER_array_of" { loc(); return TOK_ARRAY_OF; } -"__CPROVER_thread_local" { loc(); return TOK_THREAD_LOCAL; } -"__CPROVER_bitvector" { loc(); return TOK_CPROVER_BITVECTOR; } -"__CPROVER_floatbv" { loc(); return TOK_CPROVER_FLOATBV; } -"__CPROVER_fixedbv" { loc(); return TOK_CPROVER_FIXEDBV; } -"__CPROVER_bool" { loc(); return TOK_CPROVER_BOOL; } -"__CPROVER_throw" { loc(); return TOK_CPROVER_THROW; } -"__CPROVER_catch" { loc(); return TOK_CPROVER_CATCH; } -"__CPROVER_try" { loc(); return TOK_CPROVER_TRY; } -"__CPROVER_finally" { loc(); return TOK_CPROVER_FINALLY; } -"__CPROVER_ID" { loc(); return TOK_CPROVER_ID; } -"__CPROVER_loop_invariant" { loc(); return TOK_CPROVER_LOOP_INVARIANT; } -"__CPROVER_requires" { loc(); return TOK_CPROVER_REQUIRES; } -"__CPROVER_ensures" { loc(); return TOK_CPROVER_ENSURES; } +{CPROVER_PREFIX}"atomic" { loc(); return TOK_CPROVER_ATOMIC; } +{CPROVER_PREFIX}"forall" { loc(); return TOK_FORALL; } +{CPROVER_PREFIX}"exists" { loc(); return TOK_EXISTS; } +{CPROVER_PREFIX}"array_of" { loc(); return TOK_ARRAY_OF; } +{CPROVER_PREFIX}"thread_local" { loc(); return TOK_THREAD_LOCAL; } +{CPROVER_PREFIX}"bitvector" { loc(); return TOK_CPROVER_BITVECTOR; } +{CPROVER_PREFIX}"floatbv" { loc(); return TOK_CPROVER_FLOATBV; } +{CPROVER_PREFIX}"fixedbv" { loc(); return TOK_CPROVER_FIXEDBV; } +{CPROVER_PREFIX}"bool" { loc(); return TOK_CPROVER_BOOL; } +{CPROVER_PREFIX}"throw" { loc(); return TOK_CPROVER_THROW; } +{CPROVER_PREFIX}"catch" { loc(); return TOK_CPROVER_CATCH; } +{CPROVER_PREFIX}"try" { loc(); return TOK_CPROVER_TRY; } +{CPROVER_PREFIX}"finally" { loc(); return TOK_CPROVER_FINALLY; } +{CPROVER_PREFIX}"ID" { loc(); return TOK_CPROVER_ID; } +{CPROVER_PREFIX}"loop_invariant" { loc(); return TOK_CPROVER_LOOP_INVARIANT; } +{CPROVER_PREFIX}"requires" { loc(); return TOK_CPROVER_REQUIRES; } +{CPROVER_PREFIX}"ensures" { loc(); return TOK_CPROVER_ENSURES; } "\xe2\x88\x80" | "\\forall" { /* Non-standard, obviously. Found in ACSL syntax. */ diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index 4b41a0c1fef..ba9c7ffcb8d 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -423,7 +423,7 @@ void cpp_convert_typet::write(typet &type) char16_t_cnt || char32_t_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt || int128_cnt || ptr32_cnt || ptr64_cnt) - throw "illegal type modifier for __CPROVER_bool"; + throw "illegal type modifier for " CPROVER_PREFIX "bool"; type.id(ID_bool); } diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 673c97442d6..f62f0880a25 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -49,11 +49,11 @@ void cpp_internal_additions(std::ostream &out) // types out << "typedef __typeof__(sizeof(int)) __CPROVER::size_t;" << '\n'; - out << "typedef __CPROVER::size_t __CPROVER_size_t;" << '\n'; + out << "typedef __CPROVER::size_t " CPROVER_PREFIX "size_t;" << '\n'; out << "typedef " << c_type_as_string(signed_size_type().get(ID_C_c_type)) << " __CPROVER::ssize_t;" << '\n'; - out << "typedef __CPROVER::ssize_t __CPROVER_ssize_t;" << '\n'; + out << "typedef __CPROVER::ssize_t " CPROVER_PREFIX "ssize_t;" << '\n'; // new and delete are in the root namespace! out << "void operator delete(void *);" << '\n'; @@ -63,25 +63,28 @@ void cpp_internal_additions(std::ostream &out) // CPROVER extensions out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n'; - out << "typedef void __CPROVER_integer;" << '\n'; - out << "typedef void __CPROVER_rational;" << '\n'; - // TODO - // out << "thread_local unsigned long __CPROVER_thread_id = 0;" << '\n'; - out << "__CPROVER_bool " - << "__CPROVER_threads_exited[__CPROVER::constant_infinity_uint];" << '\n'; - out << "unsigned long __CPROVER_next_thread_id = 0;" << '\n'; + out << "typedef void " CPROVER_PREFIX "integer;" << '\n'; + out << "typedef void " CPROVER_PREFIX "rational;" << '\n'; + // TODO: thread_local is still broken + // out << "thread_local unsigned long " + // << CPROVER_PREFIX "thread_id = 0;" << '\n'; + out << CPROVER_PREFIX "bool " + << CPROVER_PREFIX "threads_exited[__CPROVER::constant_infinity_uint];" + << '\n'; + out << "unsigned long " CPROVER_PREFIX "next_thread_id = 0;" << '\n'; out << "extern unsigned char " - << "__CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n'; + << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n'; // malloc - out << "const void *__CPROVER_deallocated = 0;" << '\n'; - out << "const void *__CPROVER_dead_object = 0;" << '\n'; - out << "const void *__CPROVER_malloc_object = 0;" << '\n'; - out << "__CPROVER::size_t __CPROVER_malloc_size;" << '\n'; - out << "__CPROVER_bool __CPROVER_malloc_is_new_array = 0;" << '\n'; - out << "const void *__CPROVER_memory_leak = 0;" << '\n'; - out << "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);" + out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n'; + out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n'; + out << "const void *" CPROVER_PREFIX "malloc_object = 0;" << '\n'; + out << "__CPROVER::size_t " CPROVER_PREFIX "malloc_size;" << '\n'; + out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;" << '\n'; + out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n'; + out << "void *" CPROVER_PREFIX "allocate(" + << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n'; // auxiliaries for new/delete out << "void *__new(__CPROVER::size_t);" << '\n'; @@ -93,22 +96,22 @@ void cpp_internal_additions(std::ostream &out) out << "void __delete_array(void *);" << '\n'; // float - // TODO: should the thread_local - out << "int __CPROVER_rounding_mode = " + // TODO: should be thread_local + out << "int " CPROVER_PREFIX "rounding_mode = " << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n'; // pipes, write, read, close - out << "struct __CPROVER_pipet {\n" + out << "struct " CPROVER_PREFIX "pipet {\n" << " bool widowed;\n" << " char data[4];\n" << " short next_avail;\n" << " short next_unread;\n" << "};\n"; - out << "extern struct __CPROVER_pipet " - << "__CPROVER_pipes[__CPROVER::constant_infinity_uint];" << '\n'; + out << "extern struct " CPROVER_PREFIX "pipet " + << "" CPROVER_PREFIX "pipes[__CPROVER::constant_infinity_uint];" << '\n'; // offset to make sure we don't collide with other fds - out << "extern const int __CPROVER_pipe_offset;" << '\n'; - out << "unsigned __CPROVER_pipe_count=0;" << '\n'; + out << "extern const int " CPROVER_PREFIX "pipe_offset;" << '\n'; + out << "unsigned " CPROVER_PREFIX "pipe_count=0;" << '\n'; // This function needs to be declared, or otherwise can't be called // by the entry-point construction. @@ -133,7 +136,7 @@ void cpp_internal_additions(std::ostream &out) // For gcc, this is a typedef and not a keyword. // C++ doesn't have _Float128. if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) - out << "typedef __CPROVER_Float128 __float128;" << '\n'; + out << "typedef " CPROVER_PREFIX "Float128 __float128;" << '\n'; } else if(config.ansi_c.arch == "hppa") { @@ -153,7 +156,7 @@ void cpp_internal_additions(std::ostream &out) // Note that __float80 is a typedef, and not a keyword, // and that C++ doesn't have _Float64x. if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) - out << "typedef __CPROVER_Float80 __float80;" << '\n'; + out << "typedef " CPROVER_PREFIX "Float80 __float80;" << '\n'; } // On 64-bit systems, gcc has typedefs diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 216667de32c..a05869a0cb3 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -656,9 +656,14 @@ int linker_script_merget::get_linker_script_data( const std::string &def_out_file) { for(auto const &pair : symbol_table.symbols) - if(pair.second.is_extern && pair.second.value.is_nil() && - pair.second.name!="__CPROVER_memory") + { + if( + pair.second.is_extern && pair.second.value.is_nil() && + pair.second.name != CPROVER_PREFIX "memory") + { linker_defined_symbols.push_back(pair.second.name); + } + } std::ostringstream linker_def_str; std::copy( diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp index ee33b8975d9..bb53cc2db53 100644 --- a/src/goto-instrument/cover_instrument_other.cpp +++ b/src/goto-instrument/cover_instrument_other.cpp @@ -53,7 +53,7 @@ void cover_cover_instrumentert::instrument( if( code_function_call.function().id() == ID_symbol && to_symbol_expr(code_function_call.function()).get_identifier() == - "__CPROVER_cover" && + CPROVER_PREFIX "cover" && code_function_call.arguments().size() == 1) { const exprt c = code_function_call.arguments()[0]; diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 673905b9bc1..6113ec6133c 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -455,7 +455,7 @@ void dump_ct::convert_compound( s=type_to_string(comp_type); } - if(s.find("__CPROVER_bitvector")==std::string::npos) + if(s.find(CPROVER_PREFIX "bitvector") == std::string::npos) { struct_body << s; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 311f9b802ad..b53b7503c11 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -994,7 +994,10 @@ void goto_instrument_parse_optionst::instrument_goto_program() { if(cmdline.isset("show-custom-bitvector-analysis") || cmdline.isset("custom-bitvector-analysis")) - config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS"); + { + config.ansi_c.defines.push_back( + std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS"); + } // add the library status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom; diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 60c8f9191b6..f4989e7d99d 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -222,8 +222,8 @@ goto_programt::const_targett goto_program2codet::convert_instruction( { const code_typet void_t({}, empty_typet()); code_function_callt f(symbol_exprt( - target->is_atomic_begin() ? "__CPROVER_atomic_begin" - : "__CPROVER_atomic_end", + target->is_atomic_begin() ? CPROVER_PREFIX "atomic_begin" + : CPROVER_PREFIX "atomic_end", void_t)); dest.move_to_operands(f); return target; @@ -255,7 +255,7 @@ void goto_program2codet::convert_labels( if(target->is_target()) { std::stringstream label; - label << "__CPROVER_DUMP_L" << target->target_number; + label << CPROVER_PREFIX "DUMP_L" << target->target_number; code_labelt l(label.str(), code_blockt()); l.add_source_location()=target->source_location; target_label=l.get_label(); @@ -269,9 +269,12 @@ void goto_program2codet::convert_labels( it!=target->labels.end(); ++it) { - if(has_prefix(id2string(*it), "__CPROVER_ASYNC_") || - has_prefix(id2string(*it), "__CPROVER_DUMP_L")) + if( + has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_") || + has_prefix(id2string(*it), CPROVER_PREFIX "DUMP_L")) + { continue; + } // keep all original labels labels_in_use.insert(*it); @@ -1250,16 +1253,19 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto( it!=target->get_target()->labels.end(); ++it) { - if(has_prefix(id2string(*it), "__CPROVER_ASYNC_") || - has_prefix(id2string(*it), "__CPROVER_DUMP_L")) + if( + has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_") || + has_prefix(id2string(*it), CPROVER_PREFIX "DUMP_L")) + { continue; + } label << *it; break; } if(label.str().empty()) - label << "__CPROVER_DUMP_L" << target->get_target()->target_number; + label << CPROVER_PREFIX "DUMP_L" << target->get_target()->target_number; labels_in_use.insert(label.str()); @@ -1313,7 +1319,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( it=target->labels.begin(); it!=target->labels.end(); ++it) - if(has_prefix(id2string(*it), "__CPROVER_ASYNC_")) + if(has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_")) { labels_in_use.insert(*it); @@ -1379,7 +1385,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( it=target->labels.begin(); it!=target->labels.end(); ++it) - if(has_prefix(id2string(*it), "__CPROVER_ASYNC_")) + if(has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_")) { labels_in_use.insert(*it); diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index 318292e324c..d91743cfa6c 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -91,7 +91,7 @@ bool model_argc_argv( << " " CPROVER_PREFIX "assume(ARGC>=1);\n" << " " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n" << " char arg_string[4096];\n" - << " __CPROVER_input(\"arg_string\", &arg_string[0]);\n" + << " " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n" << " for(int i=0; ilabels) - if(label=="__CPROVER_HIDE") + if(label == CPROVER_PREFIX "HIDE") return true; } diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 5f90f6b6d56..5a0accef26f 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -289,7 +289,7 @@ void goto_inlinet::insert_function_body( if(goto_function.is_hidden()) { for(auto &instruction : body.instructions) - instruction.labels.remove("__CPROVER_HIDE"); + instruction.labels.remove(CPROVER_PREFIX "HIDE"); } replace_return(body, lhs); @@ -661,13 +661,9 @@ const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive( bool goto_inlinet::is_ignored(const irep_idt id) const { - return - id=="__CPROVER_cleanup" || - id=="__CPROVER_set_must" || - id=="__CPROVER_set_may" || - id=="__CPROVER_clear_must" || - id=="__CPROVER_clear_may" || - id=="__CPROVER_cover"; + return id == CPROVER_PREFIX "cleanup" || id == CPROVER_PREFIX "set_must" || + id == CPROVER_PREFIX "set_may" || id == CPROVER_PREFIX "clear_must" || + id == CPROVER_PREFIX "clear_may" || id == CPROVER_PREFIX "cover"; } bool goto_inlinet::check_inline_map( diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index a9b5a246ead..b55434afc6b 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -125,7 +125,7 @@ static bool read_bin_goto_object_v4( { irep_idt label=irepconverter.read_string_ref(in); instruction.labels.push_back(label); - if(label=="__CPROVER_HIDE") + if(label == CPROVER_PREFIX "HIDE") hidden=true; // The above info is normally in the type of the goto_functiont object, // which should likely be stored in the binary. diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index df39dee7f71..2d7eaa772b5 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -43,7 +43,8 @@ void slice_global_inits(goto_modelt &goto_model) call_grapht::create_from_root_function(goto_model, entry_point, false); const auto directed_graph = call_graph.get_directed_graph(); INVARIANT( - !directed_graph.empty(), "At least __CPROVER_start should be reachable"); + !directed_graph.empty(), + "at least " + id2string(entry_point) + " should be reachable"); // gather all symbols used by reachable functions diff --git a/src/jsil/jsil_internal_additions.cpp b/src/jsil/jsil_internal_additions.cpp index af963454e25..46da672cd99 100644 --- a/src/jsil/jsil_internal_additions.cpp +++ b/src/jsil/jsil_internal_additions.cpp @@ -25,7 +25,7 @@ void jsil_internal_additions(symbol_tablet &dest) { symbolt symbol; - symbol.base_name="__CPROVER_rounding_mode"; + symbol.base_name = CPROVER_PREFIX "rounding_mode"; symbol.name=CPROVER_PREFIX "rounding_mode"; symbol.type=signed_int_type(); symbol.mode=ID_C; @@ -41,7 +41,7 @@ void jsil_internal_additions(symbol_tablet &dest) { symbolt symbol; - symbol.base_name="__CPROVER_malloc_object"; + symbol.base_name = CPROVER_PREFIX "malloc_object"; symbol.name=CPROVER_PREFIX "malloc_object"; symbol.type=pointer_type(empty_typet()); symbol.mode=ID_C; diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index ab9102b37f2..443118f58ea 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -39,7 +39,7 @@ void static_lifetime_init( code_blockt &dest=to_code_block(to_code(init_symbol.value)); // add the magic label to hide - dest.add(code_labelt("__CPROVER_HIDE", code_skipt())); + dest.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt())); // do assignments based on "value" diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index 43ab3616fd5..ef657aa939e 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -105,9 +106,8 @@ bvt boolbvt::convert_index(const index_exprt &expr) { static int uniform_array_counter; // Temporary hack - std::string identifier= - "__CPROVER_internal_uniform_array_"+ - std::to_string(uniform_array_counter++); + const std::string identifier = CPROVER_PREFIX "internal_uniform_array_" + + std::to_string(uniform_array_counter++); symbol_exprt result(identifier, expr.type()); bv = convert_bv(result); @@ -146,9 +146,8 @@ bvt boolbvt::convert_index(const index_exprt &expr) // Symbol for output static int actual_array_counter; // Temporary hack - std::string identifier= - "__CPROVER_internal_actual_array_"+ - std::to_string(actual_array_counter++); + const std::string identifier = CPROVER_PREFIX "internal_actual_array_" + + std::to_string(actual_array_counter++); symbol_exprt result(identifier, expr.type()); bv = convert_bv(result); diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 74221617055..620bf932447 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -168,7 +168,7 @@ SCENARIO("path strategies") "/* 1 */ int main() \n" "/* 2 */ { \n" "/* 3 */ int x; \n" - "/* 4 */ __CPROVER_assume(x == 1); \n" + "/* 4 */ " CPROVER_PREFIX "assume(x == 1);\n" "/* 5 */ \n" "/* 6 */ while(x) \n" "/* 7 */ --x; \n" From 0ce0ac2db2aaf0818503025947eb53dedcaa7756 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Oct 2018 08:50:31 +0000 Subject: [PATCH 2/3] Linter and clang-format ignores, and whitespace cleanup --- .../gen_nondet_string_init.cpp | 5 +++- src/ansi-c/ansi_c_internal_additions.cpp | 2 ++ unit/path_strategies.cpp | 23 +++++++++++-------- 3 files changed, 19 insertions(+), 11 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 6aceb495460..67d26161375 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -77,7 +77,9 @@ SCENARIO( std::regex_replace(line, spaces, " "), numbers, "")); } - const std::vector reference_code = { // NOLINT + // clang-format off + // NOLINTNEXTLINE + const std::vector reference_code = { "int tmp_object_factory;", "tmp_object_factory = NONDET(int);", CPROVER_PREFIX "assume(tmp_object_factory >= 0);", @@ -98,6 +100,7 @@ SCENARIO( "=\"java::java.lang.String\" }," " .length=tmp_object_factory, " ".data=*string_data_pointer };"}; + // clang-format on for(std::size_t i = 0; i < code_string.size() && i < reference_code.size(); diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index c0145b1f01c..b22dafa554e 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -122,6 +122,7 @@ static std::string architecture_string(T value, const char *s) void ansi_c_internal_additions(std::string &code) { + // clang-format off // do the built-in types and variables code+= "# 1 \"\"\n" @@ -179,6 +180,7 @@ void ansi_c_internal_additions(std::string &code) // by the entry-point construction. "void " INITIALIZE_FUNCTION "(void);\n" "\n"; + // clang-format on // GCC junk stuff, also for CLANG and ARM if( diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 620bf932447..d4b07f67ed4 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -164,17 +164,20 @@ SCENARIO("path strategies") opts.set_option("unwind", 2U); }; + // clang-format off c = - "/* 1 */ int main() \n" - "/* 2 */ { \n" - "/* 3 */ int x; \n" - "/* 4 */ " CPROVER_PREFIX "assume(x == 1);\n" - "/* 5 */ \n" - "/* 6 */ while(x) \n" - "/* 7 */ --x; \n" - "/* 8 */ \n" - "/* 9 */ assert(x); \n" - "/* 10 */ } \n"; + "/* 1 */ int main() \n" + "/* 2 */ { \n" + "/* 3 */ int x; \n" + "/* 4 */ " CPROVER_PREFIX + "assume(x == 1); \n" + "/* 5 */ \n" + "/* 6 */ while(x) \n" + "/* 7 */ --x; \n" + "/* 8 */ \n" + "/* 9 */ assert(x); \n" + "/* 10 */ } \n"; + // clang-format on check_with_strategy( "lifo", From 3a67fb64aaa74144d4469fbbcc8fb750ba85333c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Oct 2018 10:38:54 +0000 Subject: [PATCH 3/3] Check for uses of __CPROVER_ in the linter This should help avoid future code introducing literal uses of __CPROVER_ back into the code base. --- scripts/cpplint.py | 18 ++++++++++++++++++ src/util/cprover_prefix.h | 3 +++ 2 files changed, 21 insertions(+) diff --git a/scripts/cpplint.py b/scripts/cpplint.py index 9557c8f1fae..2a46dc8ce4b 100755 --- a/scripts/cpplint.py +++ b/scripts/cpplint.py @@ -4653,6 +4653,23 @@ def CheckAssert(filename, clean_lines, linenum, error): +def Check__CPROVER_(filename, clean_lines, linenum, error): + """Check for uses of __CPROVER_. + + Args: + filename: The name of the current file. + clean_lines: A CleansedLines instance containing the file. + linenum: The number of the line to check. + error: The function to call with any errors found. + """ + line = clean_lines.lines[linenum] + match = Match(r'.*__CPROVER_.*', line) + if match: + error(filename, linenum, 'build/deprecated', 4, + 'use CPROVER_PREFIX instead of __CPROVER_') + + + def GetLineWidth(line): """Determines the width of the line in column positions. @@ -4880,6 +4897,7 @@ def CheckStyle(filename, clean_lines, linenum, file_extension, nesting_state, #CheckCheck(filename, clean_lines, linenum, error) CheckAltTokens(filename, clean_lines, linenum, error) CheckAssert(filename, clean_lines, linenum, error) + Check__CPROVER_(filename, clean_lines, linenum, error) classinfo = nesting_state.InnermostClass() if classinfo: CheckSectionSpacing(filename, clean_lines, classinfo, linenum, error) diff --git a/src/util/cprover_prefix.h b/src/util/cprover_prefix.h index 5d6fe6b84e0..f26937e20cf 100644 --- a/src/util/cprover_prefix.h +++ b/src/util/cprover_prefix.h @@ -10,8 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_CPROVER_PREFIX_H #define CPROVER_UTIL_CPROVER_PREFIX_H +// NOLINTNEXTLINE(build/deprecated) #define CPROVER_PREFIX "__CPROVER_" +// NOLINTNEXTLINE(build/deprecated) #define CPROVER_FKT_PREFIX "__CPROVER_fkt_" +// NOLINTNEXTLINE(build/deprecated) #define CPROVER_MACRO_PREFIX "__CPROVER_macro_" #endif // CPROVER_UTIL_CPROVER_PREFIX_H