Skip to content

Commit 16c8bc8

Browse files
marek-trtikmarek-trtik
committed
Fixing CPPLINTer/cnang-formater issues.
1 parent 0624b69 commit 16c8bc8

28 files changed

+194
-178
lines changed

‎regression/cbmc-with-incr/Malloc17/main.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ unsigned char* init1()
44
if (size!=1) return 0;
55

66
assert(sizeof(unsigned char)==1);
7-
unsigned char* buffer=__CPROVER_allocate(1, 0);
7+
unsigned char *buffer = __CPROVER_allocate(1, 0);
88
assert(buffer!=0);
99

1010
buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
1818
if (size!=1) return 0;
1919

2020
assert(sizeof(unsigned char)==1);
21-
unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
21+
unsigned char *buffer = __CPROVER_allocate(1 * sizeof(unsigned char), 0);
2222
assert(buffer!=0);
2323

2424
buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
3232
if (size!=1) return 0;
3333

3434
assert(sizeof(unsigned char)==1);
35-
unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
35+
unsigned char *buffer = __CPROVER_allocate(sizeof(unsigned char) * 1, 0);
3636
assert(buffer!=0);
3737

3838
buffer[0]=0;

‎regression/cbmc-with-incr/Malloc18/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ unsigned char* init()
44
if (size!=1) return 0;
55

66
assert(sizeof(unsigned char)==1);
7-
unsigned char* buffer=__CPROVER_allocate(size, 0);
7+
unsigned char *buffer = __CPROVER_allocate(size, 0);
88
assert(buffer!=0);
99

1010
buffer[0]=0;

‎regression/cbmc/Calloc1/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
int main()
55
{
6-
int *x=calloc(sizeof(int), 1);
7-
assert(*x==0);
6+
int *x = calloc(sizeof(int), 1);
7+
assert(*x == 0);
88
return 0;
99
}

‎regression/cbmc/Malloc17/main.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ unsigned char* init1()
44
if (size!=1) return 0;
55

66
assert(sizeof(unsigned char)==1);
7-
unsigned char* buffer=__CPROVER_allocate(1, 0);
7+
unsigned char *buffer = __CPROVER_allocate(1, 0);
88
assert(buffer!=0);
99

1010
buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
1818
if (size!=1) return 0;
1919

2020
assert(sizeof(unsigned char)==1);
21-
unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
21+
unsigned char *buffer = __CPROVER_allocate(1 * sizeof(unsigned char), 0);
2222
assert(buffer!=0);
2323

2424
buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
3232
if (size!=1) return 0;
3333

3434
assert(sizeof(unsigned char)==1);
35-
unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
35+
unsigned char *buffer = __CPROVER_allocate(sizeof(unsigned char) * 1, 0);
3636
assert(buffer!=0);
3737

3838
buffer[0]=0;

‎regression/cbmc/Malloc18/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ unsigned char* init()
33
unsigned long buffer_size;
44
if(buffer_size!=1) return 0;
55

6-
unsigned char* buffer=__CPROVER_allocate(buffer_size, 0);
6+
unsigned char *buffer = __CPROVER_allocate(buffer_size, 0);
77
__CPROVER_assert(buffer!=0, "malloc did not return NULL");
88

99
buffer[0]=10;

‎regression/cbmc/Malloc24/main.c

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22

33
struct node
44
{
5-
int value;
6-
struct node *next;
5+
int value;
6+
struct node *next;
77
};
88

99
struct list
@@ -12,7 +12,7 @@ struct list
1212
struct node *head;
1313
};
1414

15-
void removeLast(struct list * l)
15+
void removeLast(struct list *l)
1616
{
1717
int index = l->size - 1;
1818
struct node **current;
@@ -22,16 +22,17 @@ void removeLast(struct list * l)
2222
l->size--;
2323
}
2424

25-
int main () {
25+
int main()
26+
{
2627
//build a 2-nodes list
2728
struct node *n0 = malloc(sizeof(struct node));
2829
struct node *n1 = malloc(sizeof(struct node));
2930
struct list *l = malloc(sizeof(struct list));
3031
l->size = 2;
3132
l->head = n0;
3233

33-
n0->next=n1;
34-
n1->next=NULL;
34+
n0->next = n1;
35+
n1->next = NULL;
3536

3637
//remove last node from list
3738

@@ -43,5 +44,5 @@ int main () {
4344
//this doesn't
4445
removeLast(l);
4546

46-
__CPROVER_assert(n0->next == NULL , "not NULL");
47+
__CPROVER_assert(n0->next == NULL, "not NULL");
4748
}

‎src/analyses/constant_propagator.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -276,9 +276,12 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
276276
to_side_effect_expr(expr).get_statement()==ID_nondet)
277277
return false;
278278

279-
if(expr.id()==ID_side_effect &&
280-
to_side_effect_expr(expr).get_statement()==ID_allocate)
279+
if(
280+
expr.id() == ID_side_effect &&
281+
to_side_effect_expr(expr).get_statement() == ID_allocate)
282+
{
281283
return false;
284+
}
282285

283286
if(expr.id()==ID_symbol)
284287
if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())==

‎src/analyses/goto_check.cpp

Lines changed: 21 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
2727
#include <util/pointer_predicates.h>
2828
#include <util/cprover_prefix.h>
2929
#include <util/options.h>
30+
#include <util/invariant.h>
3031

3132
#include "local_bitvector_analysis.h"
3233

@@ -1658,24 +1659,23 @@ void goto_checkt::goto_check(
16581659
{
16591660
if(enable_pointer_check)
16601661
{
1661-
assert(i.code.operands().size()==1);
1662+
INVARIANT(i.code.operands().size() == 1, "The num-operands must be 1.");
16621663
const symbol_exprt &variable=to_symbol_expr(i.code.op0());
16631664

16641665
// is it dirty?
16651666
if(local_bitvector_analysis->dirty(variable))
16661667
{
16671668
// need to mark the dead variable as dead
16681669
goto_programt::targett t=new_code.add_instruction(ASSIGN);
1669-
exprt address_of_expr=address_of_exprt(variable);
1670+
exprt address_of_expr = address_of_exprt(variable);
16701671
exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
16711672
if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
16721673
address_of_expr.make_typecast(lhs.type());
1673-
exprt rhs=
1674-
if_exprt(
1675-
side_effect_expr_nondett(bool_typet()),
1676-
address_of_expr,
1677-
lhs,
1678-
lhs.type());
1674+
exprt rhs = if_exprt(
1675+
side_effect_expr_nondett(bool_typet()),
1676+
address_of_expr,
1677+
lhs,
1678+
lhs.type());
16791679
t->source_location=i.source_location;
16801680
t->code=code_assignt(lhs, rhs);
16811681
t->code.add_source_location()=i.source_location;
@@ -1686,27 +1686,26 @@ void goto_checkt::goto_check(
16861686
{
16871687
if(enable_pointer_check)
16881688
{
1689-
assert(i.code.operands().size()==1);
1690-
const symbol_exprt &variable=to_symbol_expr(i.code.op0());
1689+
INVARIANT(i.code.operands().size() == 1, "There must be 1 operand.");
1690+
const symbol_exprt &variable = to_symbol_expr(i.code.op0());
16911691

16921692
// is it dirty?
16931693
if(local_bitvector_analysis->dirty(variable))
16941694
{
16951695
// reset the dead marker
1696-
goto_programt::targett t=new_code.add_instruction(ASSIGN);
1697-
exprt address_of_expr=address_of_exprt(variable);
1698-
exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
1696+
goto_programt::targett t = new_code.add_instruction(ASSIGN);
1697+
exprt address_of_expr = address_of_exprt(variable);
1698+
exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
16991699
if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
17001700
address_of_expr.make_typecast(lhs.type());
1701-
exprt rhs=
1702-
if_exprt(
1703-
equal_exprt(lhs, address_of_expr),
1704-
null_pointer_exprt(to_pointer_type(address_of_expr.type())),
1705-
lhs,
1706-
lhs.type());
1707-
t->source_location=i.source_location;
1708-
t->code=code_assignt(lhs, rhs);
1709-
t->code.add_source_location()=i.source_location;
1701+
exprt rhs = if_exprt(
1702+
equal_exprt(lhs, address_of_expr),
1703+
null_pointer_exprt(to_pointer_type(address_of_expr.type())),
1704+
lhs,
1705+
lhs.type());
1706+
t->source_location = i.source_location;
1707+
t->code = code_assignt(lhs, rhs);
1708+
t->code.add_source_location() = i.source_location;
17101709
}
17111710
}
17121711
}

‎src/analyses/local_bitvector_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
232232
const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
233233
const irep_idt &statement=side_effect_expr.get_statement();
234234

235-
if(statement==ID_allocate)
235+
if(statement == ID_allocate)
236236
return flagst::mk_dynamic_heap();
237237
else
238238
return flagst::mk_unknown();

‎src/analyses/local_may_alias.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -298,7 +298,7 @@ void local_may_aliast::get_rec(
298298
const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
299299
const irep_idt &statement=side_effect_expr.get_statement();
300300

301-
if(statement==ID_allocate)
301+
if(statement == ID_allocate)
302302
{
303303
dest.insert(objects.number(exprt(ID_dynamic_object)));
304304
}

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 23 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -105,15 +105,17 @@ static std::string architecture_string(int value, const char *s)
105105

106106
void ansi_c_internal_additions(std::string &code)
107107
{
108-
code+=
108+
code +=
109109
"# 1 \"<built-in-additions>\"\n"
110110
"typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
111111
"void __CPROVER_assume(__CPROVER_bool assumption);\n"
112112
"void __VERIFIER_assume(__CPROVER_bool assumption);\n"
113113
// NOLINTNEXTLINE(whitespace/line_length)
114-
"void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
114+
"void __CPROVER_assert(__CPROVER_bool assertion, const char "
115+
"*description);\n"
115116
// NOLINTNEXTLINE(whitespace/line_length)
116-
"void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);\n"
117+
"void __CPROVER_precondition(__CPROVER_bool precondition, const char "
118+
"*description);\n"
117119
"void __CPROVER_havoc_object(void *);\n"
118120
"__CPROVER_bool __CPROVER_equal();\n"
119121
"__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
@@ -145,7 +147,8 @@ void ansi_c_internal_additions(std::string &code)
145147
"void __CPROVER_fence(const char *kind, ...);\n"
146148
"__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
147149
// NOLINTNEXTLINE(whitespace/line_length)
148-
"__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
150+
"__CPROVER_bool "
151+
"__CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
149152
"unsigned long __CPROVER_next_thread_id=0;\n"
150153

151154
// traces
@@ -157,7 +160,8 @@ void ansi_c_internal_additions(std::string &code)
157160
"__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\n"
158161
"extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
159162
// NOLINTNEXTLINE(whitespace/line_length)
160-
"void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
163+
"void __CPROVER_allocated_memory(__CPROVER_size_t address, "
164+
"__CPROVER_size_t extent);\n"
161165

162166
// malloc
163167
"void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
@@ -170,13 +174,16 @@ void ansi_c_internal_additions(std::string &code)
170174

171175
// this is ANSI-C
172176
// NOLINTNEXTLINE(whitespace/line_length)
173-
"extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
177+
"extern __CPROVER_thread_local const char "
178+
"__func__[__CPROVER_constant_infinity_uint];\n"
174179

175180
// this is GCC
176181
// NOLINTNEXTLINE(whitespace/line_length)
177-
"extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
182+
"extern __CPROVER_thread_local const char "
183+
"__FUNCTION__[__CPROVER_constant_infinity_uint];\n"
178184
// NOLINTNEXTLINE(whitespace/line_length)
179-
"extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
185+
"extern __CPROVER_thread_local const char "
186+
"__PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
180187

181188
// float stuff
182189
"__CPROVER_bool __CPROVER_isnanf(float f);\n"
@@ -197,8 +204,9 @@ void ansi_c_internal_additions(std::string &code)
197204
"double __CPROVER_inf(void);\n"
198205
"float __CPROVER_inff(void);\n"
199206
"long double __CPROVER_infl(void);\n"
200-
"int __CPROVER_thread_local __CPROVER_rounding_mode="+
201-
std::to_string(config.ansi_c.rounding_mode)+";\n"
207+
"int __CPROVER_thread_local __CPROVER_rounding_mode=" +
208+
std::to_string(config.ansi_c.rounding_mode) +
209+
";\n"
202210
"int __CPROVER_isgreaterf(float f, float g);\n"
203211
"int __CPROVER_isgreaterd(double f, double g);\n"
204212
"int __CPROVER_isgreaterequalf(float f, float g);\n"
@@ -222,7 +230,8 @@ void ansi_c_internal_additions(std::string &code)
222230

223231
// arrays
224232
// NOLINTNEXTLINE(whitespace/line_length)
225-
"__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
233+
"__CPROVER_bool __CPROVER_array_equal(const void *array1, "
234+
"const void *array2);\n"
226235
// overwrite all of *dest (possibly using nondet values), even
227236
// if *src is smaller
228237
"void __CPROVER_array_copy(const void *dest, const void *src);\n"
@@ -232,7 +241,7 @@ void ansi_c_internal_additions(std::string &code)
232241

233242
// k-induction
234243
"void __CPROVER_k_induction_hint(unsigned min, unsigned max, "
235-
"unsigned step, unsigned loop_free);\n"
244+
"unsigned step, unsigned loop_free);\n"
236245

237246
// format string-related
238247
"int __CPROVER_scanf(const char *, ...);\n"
@@ -245,7 +254,8 @@ void ansi_c_internal_additions(std::string &code)
245254
" short next_unread;\n"
246255
"};\n"
247256
// NOLINTNEXTLINE(whitespace/line_length)
248-
"extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
257+
"extern struct __CPROVER_pipet "
258+
"__CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
249259
// offset to make sure we don't collide with other fds
250260
"extern const int __CPROVER_pipe_offset;\n"
251261
"unsigned __CPROVER_pipe_count=0;\n"

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2271,16 +2271,16 @@ exprt c_typecheck_baset::do_special_functions(
22712271

22722272
return abs_expr;
22732273
}
2274-
else if(identifier==CPROVER_PREFIX "allocate")
2274+
else if(identifier == CPROVER_PREFIX "allocate")
22752275
{
2276-
if(expr.arguments().size()!=2)
2276+
if(expr.arguments().size() != 2)
22772277
{
22782278
err_location(f_op);
22792279
error() << "allocate expects two operands" << eom;
22802280
throw 0;
22812281
}
22822282

2283-
exprt malloc_expr=side_effect_exprt(ID_allocate);
2283+
exprt malloc_expr = side_effect_exprt(ID_allocate);
22842284
malloc_expr.type()=expr.type();
22852285
malloc_expr.add_source_location()=source_location;
22862286
malloc_expr.operands()=expr.arguments();

‎src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -670,7 +670,7 @@ void goto_convertt::remove_side_effect(
670670
else if(statement==ID_cpp_delete ||
671671
statement==ID_cpp_delete_array)
672672
remove_cpp_delete(expr, dest, result_is_used);
673-
else if(statement==ID_allocate)
673+
else if(statement == ID_allocate)
674674
remove_malloc(expr, dest, result_is_used);
675675
else if(statement==ID_temporary_object)
676676
remove_temporary_object(expr, dest, result_is_used);

‎src/goto-symex/goto_symex.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -322,7 +322,9 @@ class goto_symext
322322
virtual void symex_gcc_builtin_va_arg_next(
323323
statet &state, const exprt &lhs, const side_effect_exprt &code);
324324
virtual void symex_allocate(
325-
statet &state, const exprt &lhs, const side_effect_exprt &code);
325+
statet &state,
326+
const exprt &lhs,
327+
const side_effect_exprt &code);
326328
virtual void symex_cpp_delete(statet &state, const codet &code);
327329
virtual void symex_cpp_new(
328330
statet &state, const exprt &lhs, const side_effect_exprt &code);

‎src/goto-symex/goto_symex_state.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -345,6 +345,9 @@ void goto_symex_statet::assignment(
345345
assert_l2_renaming(lhs);
346346
assert_l2_renaming(rhs);
347347

348+
if(is_shared && lhs.type().id() == ID_pointer)
349+
throw "pointer handling for concurrency is unsound";
350+
348351
// for value propagation -- the RHS is L2
349352

350353
if(!is_shared && record_value && constant_propagation(rhs))

0 commit comments

Comments
 (0)