Skip to content

Commit 11dec6c

Browse files
tautschnigPetr Bauch
tautschnig
authored and
Petr Bauch
committed
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: diffblue#735
1 parent fe196d3 commit 11dec6c

28 files changed

+181
-160
lines changed

‎jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ void java_internal_additions(symbol_table_baset &dest)
2121

2222
{
2323
symbolt symbol;
24-
symbol.base_name="__CPROVER_rounding_mode";
24+
symbol.base_name = CPROVER_PREFIX "rounding_mode";
2525
symbol.name=CPROVER_PREFIX "rounding_mode";
2626
symbol.type=signed_int_type();
2727
symbol.mode=ID_C;
@@ -35,7 +35,7 @@ void java_internal_additions(symbol_table_baset &dest)
3535

3636
{
3737
symbolt symbol;
38-
symbol.base_name="__CPROVER_malloc_object";
38+
symbol.base_name = CPROVER_PREFIX "malloc_object";
3939
symbol.name=CPROVER_PREFIX "malloc_object";
4040
symbol.type=pointer_type(empty_typet());
4141
symbol.mode=ID_C;

‎jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,8 +80,8 @@ SCENARIO(
8080
const std::vector<std::string> reference_code = { // NOLINT
8181
"int tmp_object_factory;",
8282
"tmp_object_factory = NONDET(int);",
83-
"__CPROVER_assume(tmp_object_factory >= 0);",
84-
"__CPROVER_assume(tmp_object_factory <= 20);",
83+
CPROVER_PREFIX "assume(tmp_object_factory >= 0);",
84+
CPROVER_PREFIX "assume(tmp_object_factory <= 20);",
8585
"char (*string_data_pointer)[INFINITY()];",
8686
"string_data_pointer = "
8787
"ALLOCATE(char [INFINITY()], INFINITY(), false);",

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -320,10 +320,11 @@ void custom_bitvector_domaint::transform(
320320
{
321321
const irep_idt &identifier=to_symbol_expr(function).get_identifier();
322322

323-
if(identifier=="__CPROVER_set_must" ||
324-
identifier=="__CPROVER_clear_must" ||
325-
identifier=="__CPROVER_set_may" ||
326-
identifier=="__CPROVER_clear_may")
323+
if(
324+
identifier == CPROVER_PREFIX "set_must" ||
325+
identifier == CPROVER_PREFIX "clear_must" ||
326+
identifier == CPROVER_PREFIX "set_may" ||
327+
identifier == CPROVER_PREFIX "clear_may")
327328
{
328329
if(code_function_call.arguments().size()==2)
329330
{
@@ -333,13 +334,13 @@ void custom_bitvector_domaint::transform(
333334
// initialize to make Visual Studio happy
334335
modet mode = modet::SET_MUST;
335336

336-
if(identifier=="__CPROVER_set_must")
337+
if(identifier == CPROVER_PREFIX "set_must")
337338
mode=modet::SET_MUST;
338-
else if(identifier=="__CPROVER_clear_must")
339+
else if(identifier == CPROVER_PREFIX "clear_must")
339340
mode=modet::CLEAR_MUST;
340-
else if(identifier=="__CPROVER_set_may")
341+
else if(identifier == CPROVER_PREFIX "set_may")
341342
mode=modet::SET_MAY;
342-
else if(identifier=="__CPROVER_clear_may")
343+
else if(identifier == CPROVER_PREFIX "clear_may")
343344
mode=modet::CLEAR_MAY;
344345
else
345346
UNREACHABLE;

‎src/analyses/escape_analysis.cpp

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,16 +11,20 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "escape_analysis.h"
1313

14+
#include <util/cprover_prefix.h>
1415
#include <util/simplify_expr.h>
1516

1617
bool escape_domaint::is_tracked(const symbol_exprt &symbol)
1718
{
1819
const irep_idt &identifier=symbol.get_identifier();
19-
if(identifier=="__CPROVER_memory_leak" ||
20-
identifier=="__CPROVER_malloc_object" ||
21-
identifier=="__CPROVER_dead_object" ||
22-
identifier=="__CPROVER_deallocated")
20+
if(
21+
identifier == CPROVER_PREFIX "memory_leak" ||
22+
identifier == CPROVER_PREFIX "malloc_object" ||
23+
identifier == CPROVER_PREFIX "dead_object" ||
24+
identifier == CPROVER_PREFIX "deallocated")
25+
{
2326
return false;
27+
}
2428

2529
return true;
2630
}
@@ -217,7 +221,7 @@ void escape_domaint::transform(
217221
if(function.id()==ID_symbol)
218222
{
219223
const irep_idt &identifier=to_symbol_expr(function).get_identifier();
220-
if(identifier=="__CPROVER_cleanup")
224+
if(identifier == CPROVER_PREFIX "cleanup")
221225
{
222226
if(code_function_call.arguments().size()==2)
223227
{

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 38 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -109,72 +109,71 @@ const char windows_builtin_headers[]=
109109

110110
static std::string architecture_string(const std::string &value, const char *s)
111111
{
112-
return std::string("const char *__CPROVER_architecture_")+
113-
std::string(s)+
114-
"=\""+value+"\";\n";
112+
return std::string("const char *" CPROVER_PREFIX "architecture_") +
113+
std::string(s) + "=\"" + value + "\";\n";
115114
}
116115

117116
template <typename T>
118117
static std::string architecture_string(T value, const char *s)
119118
{
120-
return std::string("const int __CPROVER_architecture_")+
121-
std::string(s)+
122-
"="+std::to_string(value)+";\n";
119+
return std::string("const int " CPROVER_PREFIX "architecture_") +
120+
std::string(s) + "=" + std::to_string(value) + ";\n";
123121
}
124122

125123
void ansi_c_internal_additions(std::string &code)
126124
{
127125
// do the built-in types and variables
128126
code+=
129127
"# 1 \"<built-in-additions>\"\n"
130-
"typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
128+
"typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
131129
"typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
132-
" __CPROVER_ssize_t;\n"
133-
"const unsigned __CPROVER_constant_infinity_uint;\n"
134-
"typedef void __CPROVER_integer;\n"
135-
"typedef void __CPROVER_rational;\n"
136-
"__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
137-
// NOLINTNEXTLINE(whitespace/line_length)
138-
"__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
139-
"unsigned long __CPROVER_next_thread_id=0;\n"
140-
// NOLINTNEXTLINE(whitespace/line_length)
141-
"extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
130+
" " CPROVER_PREFIX "ssize_t;\n"
131+
"const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
132+
"typedef void " CPROVER_PREFIX "integer;\n"
133+
"typedef void " CPROVER_PREFIX "rational;\n"
134+
CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n"
135+
CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
136+
CPROVER_PREFIX "constant_infinity_uint];\n"
137+
"unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
138+
"extern unsigned char " CPROVER_PREFIX "memory["
139+
CPROVER_PREFIX "constant_infinity_uint];\n"
142140

143141
// malloc
144-
"const void *__CPROVER_deallocated=0;\n"
145-
"const void *__CPROVER_dead_object=0;\n"
146-
"const void *__CPROVER_malloc_object=0;\n"
147-
"__CPROVER_size_t __CPROVER_malloc_size;\n"
148-
"__CPROVER_bool __CPROVER_malloc_is_new_array=0;\n" // for C++
149-
"const void *__CPROVER_memory_leak=0;\n"
150-
"void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
142+
"const void *" CPROVER_PREFIX "deallocated=0;\n"
143+
"const void *" CPROVER_PREFIX "dead_object=0;\n"
144+
"const void *" CPROVER_PREFIX "malloc_object=0;\n"
145+
CPROVER_PREFIX "size_t " CPROVER_PREFIX "malloc_size;\n"
146+
CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
147+
"const void *" CPROVER_PREFIX "memory_leak=0;\n"
148+
"void *" CPROVER_PREFIX "allocate("
149+
CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
151150

152151
// this is ANSI-C
153-
// NOLINTNEXTLINE(whitespace/line_length)
154-
"extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
152+
"extern " CPROVER_PREFIX "thread_local const char __func__["
153+
CPROVER_PREFIX "constant_infinity_uint];\n"
155154

156155
// this is GCC
157-
// NOLINTNEXTLINE(whitespace/line_length)
158-
"extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
159-
// NOLINTNEXTLINE(whitespace/line_length)
160-
"extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
156+
"extern " CPROVER_PREFIX "thread_local const char __FUNCTION__["
157+
CPROVER_PREFIX "constant_infinity_uint];\n"
158+
"extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
159+
CPROVER_PREFIX "constant_infinity_uint];\n"
161160

162161
// float stuff
163-
"int __CPROVER_thread_local __CPROVER_rounding_mode="+
162+
"int " CPROVER_PREFIX "thread_local " CPROVER_PREFIX "rounding_mode="+
164163
std::to_string(config.ansi_c.rounding_mode)+";\n"
165164

166165
// pipes, write, read, close
167-
"struct __CPROVER_pipet {\n"
166+
"struct " CPROVER_PREFIX "pipet {\n"
168167
" _Bool widowed;\n"
169168
" char data[4];\n"
170169
" short next_avail;\n"
171170
" short next_unread;\n"
172171
"};\n"
173-
// NOLINTNEXTLINE(whitespace/line_length)
174-
"extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
172+
"extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes["
173+
CPROVER_PREFIX "constant_infinity_uint];\n"
175174
// offset to make sure we don't collide with other fds
176-
"extern const int __CPROVER_pipe_offset;\n"
177-
"unsigned __CPROVER_pipe_count=0;\n"
175+
"extern const int " CPROVER_PREFIX "pipe_offset;\n"
176+
"unsigned " CPROVER_PREFIX "pipe_count=0;\n"
178177
"\n"
179178
// This function needs to be declared, or otherwise can't be called
180179
// by the entry-point construction.
@@ -201,13 +200,13 @@ void ansi_c_internal_additions(std::string &code)
201200
// For clang, __float128 is a keyword.
202201
// For gcc, this is a typedef and not a keyword.
203202
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
204-
code += "typedef __CPROVER_Float128 __float128;\n";
203+
code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
205204
}
206205
else if(config.ansi_c.arch == "ppc64le")
207206
{
208207
// https://patchwork.ozlabs.org/patch/792295/
209208
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
210-
code += "typedef __CPROVER_Float128 __ieee128;\n";
209+
code += "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
211210
}
212211
else if(config.ansi_c.arch == "hppa")
213212
{
@@ -225,7 +224,7 @@ void ansi_c_internal_additions(std::string &code)
225224
// clang doesn't do __float80
226225
// Note that __float80 is a typedef, and not a keyword.
227226
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
228-
code += "typedef __CPROVER_Float64x __float80;\n";
227+
code += "typedef " CPROVER_PREFIX "Float64x __float80;\n";
229228
}
230229

231230
// On 64-bit systems, gcc has typedefs

‎src/ansi-c/c_typecheck_base.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -771,7 +771,7 @@ void c_typecheck_baset::typecheck_declaration(
771771
ret_type=to_code_type(new_symbol.type).return_type();
772772
assert(parameter_map.empty());
773773
if(ret_type.id()!=ID_empty)
774-
parameter_map["__CPROVER_return_value"]=ret_type;
774+
parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
775775
typecheck_spec_expr(contract, ID_C_spec_ensures);
776776
parameter_map.clear();
777777

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1508,11 +1508,11 @@ void c_typecheck_baset::typecheck_typedef_type(typet &type)
15081508
type.set(ID_C_alignment, alignment);
15091509

15101510
// CPROVER extensions
1511-
if(symbol.base_name=="__CPROVER_rational")
1511+
if(symbol.base_name == CPROVER_PREFIX "rational")
15121512
{
15131513
type=rational_typet();
15141514
}
1515-
else if(symbol.base_name=="__CPROVER_integer")
1515+
else if(symbol.base_name == CPROVER_PREFIX "integer")
15161516
{
15171517
type=integer_typet();
15181518
}

‎src/ansi-c/cprover_library.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ static std::string get_cprover_library_text(
2525
"#undef inline\n";
2626

2727
if(config.ansi_c.string_abstraction)
28-
library_text << "#define __CPROVER_STRING_ABSTRACTION\n";
28+
library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
2929

3030
// cprover_library.inc may not have been generated when running Doxygen, thus
3131
// make Doxygen skip this part

‎src/ansi-c/expr2c.cpp

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/arith_tools.h>
1818
#include <util/c_types.h>
1919
#include <util/config.h>
20+
#include <util/cprover_prefix.h>
2021
#include <util/find_symbols.h>
2122
#include <util/fixedbv.h>
2223
#include <util/lispexpr.h>
@@ -213,7 +214,7 @@ std::string expr2ct::convert_rec(
213214
}
214215
else if(src.id()==ID_string)
215216
{
216-
return q+"__CPROVER_string"+d;
217+
return q + CPROVER_PREFIX + "string" + d;
217218
}
218219
else if(src.id()==ID_natural ||
219220
src.id()==ID_integer ||
@@ -244,17 +245,16 @@ std::string expr2ct::convert_rec(
244245
{
245246
std::string swidth=src.get_string(ID_width);
246247
std::string fwidth=src.get_string(ID_f);
247-
return q+"__CPROVER_floatbv["+swidth+"]["+fwidth+"]";
248+
return q + CPROVER_PREFIX + "floatbv[" + swidth + "][" + fwidth + "]";
248249
}
249250
}
250251
else if(src.id()==ID_fixedbv)
251252
{
252253
const std::size_t width=to_fixedbv_type(src).get_width();
253254

254255
const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();
255-
return
256-
q+"__CPROVER_fixedbv["+std::to_string(width)+"]["+
257-
std::to_string(fraction_bits)+"]"+d;
256+
return q + CPROVER_PREFIX + "fixedbv[" + std::to_string(width) + "][" +
257+
std::to_string(fraction_bits) + "]" + d;
258258
}
259259
else if(src.id()==ID_c_bit_field)
260260
{
@@ -323,8 +323,8 @@ std::string expr2ct::convert_rec(
323323
}
324324
else
325325
{
326-
return q+sign_str+
327-
"__CPROVER_bitvector["+integer2string(width)+"]"+d;
326+
return q + sign_str + CPROVER_PREFIX + "bitvector[" +
327+
integer2string(width) + "]" + d;
328328
}
329329
}
330330
else if(src.id()==ID_struct)
@@ -2982,10 +2982,10 @@ std::string expr2ct::convert_code(
29822982
return convert_code_unlock(src, indent);
29832983

29842984
if(statement==ID_atomic_begin)
2985-
return indent_str(indent)+"__CPROVER_atomic_begin();";
2985+
return indent_str(indent) + CPROVER_PREFIX + "atomic_begin();";
29862986

29872987
if(statement==ID_atomic_end)
2988-
return indent_str(indent)+"__CPROVER_atomic_end();";
2988+
return indent_str(indent) + CPROVER_PREFIX + "atomic_end();";
29892989

29902990
if(statement==ID_function_call)
29912991
return convert_code_function_call(to_code_function_call(src), indent);
@@ -3282,7 +3282,8 @@ std::string expr2ct::convert_code_assume(
32823282
return convert_norep(src, precedence);
32833283
}
32843284

3285-
return indent_str(indent)+"__CPROVER_assume("+convert(src.op0())+");";
3285+
return indent_str(indent) + CPROVER_PREFIX + "assume(" + convert(src.op0()) +
3286+
");";
32863287
}
32873288

32883289
std::string expr2ct::convert_code_label(
@@ -3551,10 +3552,10 @@ std::string expr2ct::convert_with_precedence(
35513552
return convert_function(src, "POINTER_OBJECT", precedence=16);
35523553

35533554
else if(src.id()=="get_must")
3554-
return convert_function(src, "__CPROVER_get_must", precedence=16);
3555+
return convert_function(src, CPROVER_PREFIX "get_must", precedence = 16);
35553556

35563557
else if(src.id()=="get_may")
3557-
return convert_function(src, "__CPROVER_get_may", precedence=16);
3558+
return convert_function(src, CPROVER_PREFIX "get_may", precedence = 16);
35583559

35593560
else if(src.id()=="object_value")
35603561
return convert_function(src, "OBJECT_VALUE", precedence=16);
@@ -3572,7 +3573,8 @@ std::string expr2ct::convert_with_precedence(
35723573
return convert_function(src, "POINTER_CONS", precedence=16);
35733574

35743575
else if(src.id()==ID_invalid_pointer)
3575-
return convert_function(src, "__CPROVER_invalid_pointer", precedence=16);
3576+
return convert_function(
3577+
src, CPROVER_PREFIX "invalid_pointer", precedence = 16);
35763578

35773579
else if(src.id()==ID_dynamic_object)
35783580
return convert_function(src, "DYNAMIC_OBJECT", precedence=16);

0 commit comments

Comments
 (0)