Skip to content

Commit 3ab73ea

Browse files
tautschnigtautschnig
authored
Merge pull request #3171 from tautschnig/use_cprover_prefix
Use CPROVER_PREFIX macro instead of hardcoded __CPROVER_ string
2 parents 3039114 + 3a67fb6 commit 3ab73ea

30 files changed

+220
-170
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: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,11 +77,13 @@ SCENARIO(
7777
std::regex_replace(line, spaces, " "), numbers, ""));
7878
}
7979

80-
const std::vector<std::string> reference_code = { // NOLINT
80+
// clang-format off
81+
// NOLINTNEXTLINE
82+
const std::vector<std::string> reference_code = {
8183
"int tmp_object_factory;",
8284
"tmp_object_factory = NONDET(int);",
83-
"__CPROVER_assume(tmp_object_factory >= 0);",
84-
"__CPROVER_assume(tmp_object_factory <= 20);",
85+
CPROVER_PREFIX "assume(tmp_object_factory >= 0);",
86+
CPROVER_PREFIX "assume(tmp_object_factory <= 20);",
8587
"char (*string_data_pointer)[INFINITY()];",
8688
"string_data_pointer = "
8789
"ALLOCATE(char [INFINITY()], INFINITY(), false);",
@@ -98,6 +100,7 @@ SCENARIO(
98100
"=\"java::java.lang.String\" },"
99101
" .length=tmp_object_factory, "
100102
".data=*string_data_pointer };"};
103+
// clang-format on
101104

102105
for(std::size_t i = 0;
103106
i < code_string.size() && i < reference_code.size();

‎scripts/cpplint.py

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4653,6 +4653,23 @@ def CheckAssert(filename, clean_lines, linenum, error):
46534653

46544654

46554655

4656+
def Check__CPROVER_(filename, clean_lines, linenum, error):
4657+
"""Check for uses of __CPROVER_.
4658+
4659+
Args:
4660+
filename: The name of the current file.
4661+
clean_lines: A CleansedLines instance containing the file.
4662+
linenum: The number of the line to check.
4663+
error: The function to call with any errors found.
4664+
"""
4665+
line = clean_lines.lines[linenum]
4666+
match = Match(r'.*__CPROVER_.*', line)
4667+
if match:
4668+
error(filename, linenum, 'build/deprecated', 4,
4669+
'use CPROVER_PREFIX instead of __CPROVER_')
4670+
4671+
4672+
46564673
def GetLineWidth(line):
46574674
"""Determines the width of the line in column positions.
46584675
@@ -4880,6 +4897,7 @@ def CheckStyle(filename, clean_lines, linenum, file_extension, nesting_state,
48804897
#CheckCheck(filename, clean_lines, linenum, error)
48814898
CheckAltTokens(filename, clean_lines, linenum, error)
48824899
CheckAssert(filename, clean_lines, linenum, error)
4900+
Check__CPROVER_(filename, clean_lines, linenum, error)
48834901
classinfo = nesting_state.InnermostClass()
48844902
if classinfo:
48854903
CheckSectionSpacing(filename, clean_lines, classinfo, linenum, error)

‎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: 40 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -109,77 +109,78 @@ 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
{
125+
// clang-format off
127126
// do the built-in types and variables
128127
code+=
129128
"# 1 \"<built-in-additions>\"\n"
130-
"typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
129+
"typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
131130
"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"
131+
" " CPROVER_PREFIX "ssize_t;\n"
132+
"const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
133+
"typedef void " CPROVER_PREFIX "integer;\n"
134+
"typedef void " CPROVER_PREFIX "rational;\n"
135+
CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n"
136+
CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
137+
CPROVER_PREFIX "constant_infinity_uint];\n"
138+
"unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
139+
"extern unsigned char " CPROVER_PREFIX "memory["
140+
CPROVER_PREFIX "constant_infinity_uint];\n"
142141

143142
// 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"
143+
"const void *" CPROVER_PREFIX "deallocated=0;\n"
144+
"const void *" CPROVER_PREFIX "dead_object=0;\n"
145+
"const void *" CPROVER_PREFIX "malloc_object=0;\n"
146+
CPROVER_PREFIX "size_t " CPROVER_PREFIX "malloc_size;\n"
147+
CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
148+
"const void *" CPROVER_PREFIX "memory_leak=0;\n"
149+
"void *" CPROVER_PREFIX "allocate("
150+
CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
151151

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

156156
// 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"
157+
"extern " CPROVER_PREFIX "thread_local const char __FUNCTION__["
158+
CPROVER_PREFIX "constant_infinity_uint];\n"
159+
"extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
160+
CPROVER_PREFIX "constant_infinity_uint];\n"
161161

162162
// float stuff
163-
"int __CPROVER_thread_local __CPROVER_rounding_mode="+
163+
"int " CPROVER_PREFIX "thread_local " CPROVER_PREFIX "rounding_mode="+
164164
std::to_string(config.ansi_c.rounding_mode)+";\n"
165165

166166
// pipes, write, read, close
167-
"struct __CPROVER_pipet {\n"
167+
"struct " CPROVER_PREFIX "pipet {\n"
168168
" _Bool widowed;\n"
169169
" char data[4];\n"
170170
" short next_avail;\n"
171171
" short next_unread;\n"
172172
"};\n"
173-
// NOLINTNEXTLINE(whitespace/line_length)
174-
"extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
173+
"extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes["
174+
CPROVER_PREFIX "constant_infinity_uint];\n"
175175
// 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"
176+
"extern const int " CPROVER_PREFIX "pipe_offset;\n"
177+
"unsigned " CPROVER_PREFIX "pipe_count=0;\n"
178178
"\n"
179179
// This function needs to be declared, or otherwise can't be called
180180
// by the entry-point construction.
181181
"void " INITIALIZE_FUNCTION "(void);\n"
182182
"\n";
183+
// clang-format on
183184

184185
// GCC junk stuff, also for CLANG and ARM
185186
if(
@@ -201,13 +202,13 @@ void ansi_c_internal_additions(std::string &code)
201202
// For clang, __float128 is a keyword.
202203
// For gcc, this is a typedef and not a keyword.
203204
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
204-
code += "typedef __CPROVER_Float128 __float128;\n";
205+
code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
205206
}
206207
else if(config.ansi_c.arch == "ppc64le")
207208
{
208209
// https://patchwork.ozlabs.org/patch/792295/
209210
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
210-
code += "typedef __CPROVER_Float128 __ieee128;\n";
211+
code += "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
211212
}
212213
else if(config.ansi_c.arch == "hppa")
213214
{
@@ -225,7 +226,7 @@ void ansi_c_internal_additions(std::string &code)
225226
// clang doesn't do __float80
226227
// Note that __float80 is a typedef, and not a keyword.
227228
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
228-
code += "typedef __CPROVER_Float64x __float80;\n";
229+
code += "typedef " CPROVER_PREFIX "Float64x __float80;\n";
229230
}
230231

231232
// 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

0 commit comments

Comments
 (0)