Skip to content

Commit 64a3320

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #149 from FrNecas/frnecas-cbmc-5.8
Update to CBMC 5.8
2 parents ac8efba + 2411949 commit 64a3320

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+208
-182
lines changed

‎lib/cbmc

Submodule cbmc updated 3142 files

‎regression/instrumentation/pointers/main.c

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
1-
typedef struct data {
1+
struct data {
22
struct data *next;
33
int content;
4-
} Data;
4+
};
55

66
void main() {
7-
Data x1 = {0,};
8-
Data x2 = {&x1,};
9-
Data x3 = {&x2,};
10-
Data *curr = &x3;
7+
struct data x1 = {0,};
8+
struct data x2 = {&x1,};
9+
struct data x3 = {&x2,};
10+
struct data *curr = &x3;
1111
while (curr) {
1212
assert(curr->content == 0);
1313
curr = curr->next;

‎regression/preconditions/precond_contextsensitive2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ main.c
33
--context-sensitive --preconditions
44
^EXIT=5$
55
^SIGNAL=0$
6-
^\[_start\]: argc' <= 268435456 && -\(\(signed __CPROVER_bitvector\[33\]\)argc'\) <= -2$
6+
^\[__CPROVER__start\]: argc' <= 268435456 && -\(\(signed __CPROVER_bitvector\[33\]\)argc'\) <= -2$

‎regression/termination/precond_term1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ main.c
33
--preconditions
44
^EXIT=5$
55
^SIGNAL=0$
6-
\[_start\]: !\(argc' <= 1 && -\(\(signed __CPROVER_bitvector\[33\]\)argc'\) <= -1\)
6+
\[__CPROVER__start\]: !\(argc' <= 1 && -\(\(signed __CPROVER_bitvector\[33\]\)argc'\) <= -1\)

‎src/2ls/2ls_parse_options.cpp

Lines changed: 25 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -151,10 +151,10 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
151151
else
152152
options.set_option("std-invariants", false);
153153

154-
if(cmdline.isset("no-propagation"))
155-
options.set_option("constant-propagation", false);
156-
else
154+
if(cmdline.isset("constant-propagation"))
157155
options.set_option("constant-propagation", true);
156+
else
157+
options.set_option("constant-propagation", false);
158158

159159
// magic error label
160160
if(cmdline.isset("error-label"))
@@ -633,7 +633,7 @@ int twols_parse_optionst::doit()
633633
// do actual analysis
634634
switch((*checker)(goto_model))
635635
{
636-
case property_checkert::PASS:
636+
case property_checkert::resultt::PASS:
637637
if(report_assertions)
638638
report_properties(options, goto_model, checker->property_map);
639639
report_success();
@@ -642,7 +642,7 @@ int twols_parse_optionst::doit()
642642
retval=0;
643643
break;
644644

645-
case property_checkert::FAIL:
645+
case property_checkert::resultt::FAIL:
646646
{
647647
if(report_assertions)
648648
report_properties(options, goto_model, checker->property_map);
@@ -651,7 +651,7 @@ int twols_parse_optionst::doit()
651651
bool trace_valid=false;
652652
for(const auto &p : checker->property_map)
653653
{
654-
if(p.second.result!=property_checkert::FAIL)
654+
if(p.second.result!=property_checkert::resultt::FAIL)
655655
continue;
656656

657657
if(options.get_bool_option("trace"))
@@ -681,7 +681,7 @@ int twols_parse_optionst::doit()
681681
retval=10;
682682
break;
683683
}
684-
case property_checkert::UNKNOWN:
684+
case property_checkert::resultt::UNKNOWN:
685685
if(report_assertions)
686686
report_properties(options, goto_model, checker->property_map);
687687
retval=5;
@@ -963,7 +963,7 @@ bool twols_parse_optionst::get_goto_program(
963963

964964
language->set_message_handler(get_message_handler());
965965

966-
status("Parsing", filename);
966+
status() << "Parsing" << filename << eom;
967967

968968
if(language->parse(infile, filename))
969969
{
@@ -1049,6 +1049,7 @@ bool twols_parse_optionst::process_goto_program(
10491049
{
10501050
status() << "Function Pointer Removal" << eom;
10511051
remove_function_pointers(
1052+
get_message_handler(),
10521053
goto_model,
10531054
cmdline.isset("pointer-check"));
10541055

@@ -1062,7 +1063,7 @@ bool twols_parse_optionst::process_goto_program(
10621063

10631064
// remove inlined functions
10641065
Forall_goto_functions(f_it, goto_model.goto_functions)
1065-
if(f_it->first!=ID__start &&
1066+
if(f_it->first!=goto_functionst::entry_point() &&
10661067
f_it->second.body.instructions.size()<=2*(limit/2))
10671068
{
10681069
f_it->second.body.clear();
@@ -1285,10 +1286,10 @@ void twols_parse_optionst::report_properties(
12851286
#endif
12861287

12871288
if(!options.get_bool_option("all-properties") &&
1288-
it->second.result!=property_checkert::FAIL)
1289+
it->second.result!=property_checkert::resultt::FAIL)
12891290
continue;
12901291

1291-
if(get_ui()==ui_message_handlert::XML_UI)
1292+
if(get_ui()==ui_message_handlert::uit::XML_UI)
12921293
{
12931294
xmlt xml_result("result");
12941295
xml_result.set_attribute("property", id2string(it->first));
@@ -1307,10 +1308,10 @@ void twols_parse_optionst::report_properties(
13071308
}
13081309

13091310
if(options.get_bool_option("trace") &&
1310-
it->second.result==property_checkert::FAIL)
1311+
it->second.result==property_checkert::resultt::FAIL)
13111312
show_counterexample(goto_model, it->second.error_trace);
13121313
if(cmdline.isset("json-cex") &&
1313-
it->second.result==property_checkert::FAIL)
1314+
it->second.result==property_checkert::resultt::FAIL)
13141315
output_json_cex(
13151316
options,
13161317
goto_model,
@@ -1330,9 +1331,9 @@ void twols_parse_optionst::report_properties(
13301331
it!=property_map.end();
13311332
it++)
13321333
{
1333-
if(it->second.result==property_checkert::UNKNOWN)
1334+
if(it->second.result==property_checkert::resultt::UNKNOWN)
13341335
unknown++;
1335-
if(it->second.result==property_checkert::FAIL)
1336+
if(it->second.result==property_checkert::resultt::FAIL)
13361337
failed++;
13371338
}
13381339

@@ -1351,10 +1352,10 @@ void twols_parse_optionst::report_success()
13511352

13521353
switch(get_ui())
13531354
{
1354-
case ui_message_handlert::PLAIN:
1355+
case ui_message_handlert::uit::PLAIN:
13551356
break;
13561357

1357-
case ui_message_handlert::XML_UI:
1358+
case ui_message_handlert::uit::XML_UI:
13581359
{
13591360
xmlt xml("cprover-status");
13601361
xml.data="SUCCESS";
@@ -1376,12 +1377,12 @@ void twols_parse_optionst::show_counterexample(
13761377

13771378
switch(get_ui())
13781379
{
1379-
case ui_message_handlert::PLAIN:
1380+
case ui_message_handlert::uit::PLAIN:
13801381
std::cout << std::endl << "Counterexample:" << std::endl;
13811382
show_goto_trace(std::cout, ns, error_trace);
13821383
break;
13831384

1384-
case ui_message_handlert::XML_UI:
1385+
case ui_message_handlert::uit::XML_UI:
13851386
{
13861387
xmlt xml;
13871388
convert(ns, error_trace, xml);
@@ -1401,7 +1402,7 @@ void twols_parse_optionst::output_graphml_cex(
14011402
{
14021403
for(const auto &p : summary_checker.property_map)
14031404
{
1404-
if(p.second.result!=property_checkert::FAIL)
1405+
if(p.second.result!=property_checkert::resultt::FAIL)
14051406
continue;
14061407

14071408
const namespacet ns(goto_model.symbol_table);
@@ -1475,10 +1476,10 @@ void twols_parse_optionst::report_failure()
14751476

14761477
switch(get_ui())
14771478
{
1478-
case ui_message_handlert::PLAIN:
1479+
case ui_message_handlert::uit::PLAIN:
14791480
break;
14801481

1481-
case ui_message_handlert::XML_UI:
1482+
case ui_message_handlert::uit::XML_UI:
14821483
{
14831484
xmlt xml("cprover-status");
14841485
xml.data="FAILURE";
@@ -1498,10 +1499,10 @@ void twols_parse_optionst::report_unknown()
14981499

14991500
switch(get_ui())
15001501
{
1501-
case ui_message_handlert::PLAIN:
1502+
case ui_message_handlert::uit::PLAIN:
15021503
break;
15031504

1504-
case ui_message_handlert::XML_UI:
1505+
case ui_message_handlert::uit::XML_UI:
15051506
{
15061507
xmlt xml("cprover-status");
15071508
xml.data="UNKNOWN";

‎src/2ls/2ls_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ class optionst;
6666
"(graphml-witness):(json-cex):" \
6767
"(no-spurious-check)(stop-on-fail)" \
6868
"(competition-mode)(slice)(no-propagation)(independent-properties)" \
69+
"(constant-propagation)" \
6970
"(no-unwinding-assertions)"
7071
// the last line is for CBMC-regression testing only
7172

‎src/2ls/cover_goals_ext.cpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -84,10 +84,10 @@ void cover_goals_extt::operator()()
8484

8585
switch(dec_result)
8686
{
87-
case decision_proceduret::D_UNSATISFIABLE: // DONE
87+
case decision_proceduret::resultt::D_UNSATISFIABLE: // DONE
8888
break;
8989

90-
case decision_proceduret::D_SATISFIABLE:
90+
case decision_proceduret::resultt::D_SATISFIABLE:
9191
// mark the goals we got
9292
mark();
9393

@@ -103,7 +103,7 @@ void cover_goals_extt::operator()()
103103
return;
104104
}
105105
}
106-
while(dec_result==decision_proceduret::D_SATISFIABLE &&
106+
while(dec_result==decision_proceduret::resultt::D_SATISFIABLE &&
107107
number_covered()<size());
108108
}
109109

@@ -130,10 +130,10 @@ void cover_goals_extt::assignment()
130130
for(goal_mapt::const_iterator it=goal_map.begin();
131131
it!=goal_map.end(); it++, g_it++)
132132
{
133-
if(property_map[it->first].result==property_checkert::UNKNOWN &&
133+
if(property_map[it->first].result==property_checkert::resultt::UNKNOWN &&
134134
solver.l_get(g_it->condition).is_true())
135135
{
136-
property_map[it->first].result=property_checkert::FAIL;
136+
property_map[it->first].result=property_checkert::resultt::FAIL;
137137
if(build_error_trace)
138138
{
139139
ssa_build_goto_tracet build_goto_trace(SSA, solver.get_solver());
@@ -153,16 +153,16 @@ void cover_goals_extt::assignment()
153153

154154
switch(solver())
155155
{
156-
case decision_proceduret::D_SATISFIABLE:
156+
case decision_proceduret::resultt::D_SATISFIABLE:
157157
{
158158
std::list<cover_goals_extt::cover_goalt>::const_iterator g_it=goals.begin();
159159
for(goal_mapt::const_iterator it=goal_map.begin();
160160
it!=goal_map.end(); it++, g_it++)
161161
{
162-
if(property_map[it->first].result==property_checkert::UNKNOWN &&
162+
if(property_map[it->first].result==property_checkert::resultt::UNKNOWN &&
163163
solver.l_get(g_it->condition).is_true())
164164
{
165-
property_map[it->first].result=property_checkert::FAIL;
165+
property_map[it->first].result=property_checkert::resultt::FAIL;
166166
if(build_error_trace)
167167
{
168168
ssa_build_goto_tracet build_goto_trace(SSA, solver.get_solver());
@@ -179,10 +179,10 @@ void cover_goals_extt::assignment()
179179
}
180180
break;
181181
}
182-
case decision_proceduret::D_UNSATISFIABLE:
182+
case decision_proceduret::resultt::D_UNSATISFIABLE:
183183
break;
184184

185-
case decision_proceduret::D_ERROR:
185+
case decision_proceduret::resultt::D_ERROR:
186186
default:
187187
throw "error from decision procedure";
188188
}

‎src/2ls/graphml_witness_ext.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Author: Peter Schrammel
1515
void graphml_witness_extt::operator()(
1616
const summary_checker_baset &summary_checker)
1717
{
18-
irep_idt function_name=ID__start;
18+
irep_idt function_name=goto_functionst::entry_point();
1919
const unwindable_local_SSAt &ssa=
2020
static_cast<const unwindable_local_SSAt &>(
2121
summary_checker.ssa_db.get(function_name));

‎src/2ls/horn_encoding.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ class horn_encodingt
2929
ns(_goto_model.symbol_table),
3030
options(_options),
3131
out(_out),
32-
smt2_conv(ns, "", "Horn-clause encoding", "", smt2_convt::Z3, _out)
32+
smt2_conv(ns, "", "Horn-clause encoding", "", smt2_convt::solvert::Z3, _out)
3333
{
3434
}
3535

‎src/2ls/preprocessing_util.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,8 @@ Author: Peter Schrammel
2222

2323
void twols_parse_optionst::inline_main(goto_modelt &goto_model)
2424
{
25-
goto_programt &main=goto_model.goto_functions.function_map[ID__start].body;
25+
irep_idt start=goto_functionst::entry_point();
26+
goto_programt &main=goto_model.goto_functions.function_map[start].body;
2627
goto_programt::targett target=main.instructions.begin();
2728
while(target!=main.instructions.end())
2829
{
@@ -155,7 +156,7 @@ bool twols_parse_optionst::unwind_goto_into_loop(
155156
l_it->second,
156157
l_it->first,
157158
k,
158-
goto_unwindt::PARTIAL, iteration_points);
159+
goto_unwindt::unwind_strategyt::PARTIAL, iteration_points);
159160

160161
assert(iteration_points.size()==2);
161162
goto_programt::targett t=body.insert_before(l_it->first);
@@ -798,7 +799,8 @@ void twols_parse_optionst::assert_no_builtin_functions(goto_modelt &goto_model)
798799
{
799800
forall_goto_program_instructions(
800801
i_it,
801-
goto_model.goto_functions.function_map.find("_start")->second.body)
802+
goto_model.goto_functions.function_map.find(
803+
goto_model.goto_functions.entry_point())->second.body)
802804
{
803805
std::string name=id2string(i_it->source_location.get_function());
804806
assert(

‎src/2ls/summary_checker_ai.cpp

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ property_checkert::resultt summary_checker_ait::operator()(
3232
// properties
3333
initialize_property_map(goto_model.goto_functions);
3434

35-
property_checkert::resultt result=property_checkert::UNKNOWN;
35+
property_checkert::resultt result=property_checkert::resultt::UNKNOWN;
3636
bool finished=false;
3737
while(!finished)
3838
{
@@ -54,7 +54,7 @@ property_checkert::resultt summary_checker_ait::operator()(
5454
{
5555
report_statistics();
5656
report_preconditions();
57-
return property_checkert::UNKNOWN;
57+
return property_checkert::resultt::UNKNOWN;
5858
}
5959

6060
if(termination)
@@ -65,13 +65,13 @@ property_checkert::resultt summary_checker_ait::operator()(
6565

6666
#ifdef SHOW_CALLINGCONTEXTS
6767
if(options.get_bool_option("show-calling-contexts"))
68-
return property_checkert::UNKNOWN;
68+
return property_checkert::resultt::UNKNOWN;
6969
#endif
7070

7171
result=check_properties();
7272
report_statistics();
7373

74-
if(result==property_checkert::UNKNOWN &&
74+
if(result==property_checkert::resultt::UNKNOWN &&
7575
options.get_bool_option("values-refine") &&
7676
options.get_bool_option("intervals"))
7777
{
@@ -134,17 +134,17 @@ property_checkert::resultt summary_checker_ait::report_termination()
134134
<< (!computed ? "not computed" : threeval2string(terminates)) << eom;
135135
}
136136
if(not_computed)
137-
return property_checkert::UNKNOWN;
137+
return property_checkert::resultt::UNKNOWN;
138138
if(all_terminate)
139-
return property_checkert::PASS;
139+
return property_checkert::resultt::PASS;
140140
if(one_nonterminate)
141141
{
142142
#if 0
143-
return property_checkert::FAIL;
143+
return property_checkert::resultt::FAIL;
144144
#else
145145
// rely on nontermination checker to find counterexample
146-
return property_checkert::UNKNOWN;
146+
return property_checkert::resultt::UNKNOWN;
147147
#endif
148148
}
149-
return property_checkert::UNKNOWN;
149+
return property_checkert::resultt::UNKNOWN;
150150
}

0 commit comments

Comments
 (0)