Skip to content

Commit 703a04c

Browse files
FrNecasFrNecas
committed
Update CBMC to 5.7
Replace i2string with std::to_string. Adjust abstract domains: - In CBMC 5.7, abstract domains work slightly differently than they used to. Methods for creating top, bottom and entry must be implemented. Moreover, the first merge could have no effect resulting in the function not being entered due to changes in abstract interpretation implementation in CBMC. Replace dstring with dstringt. Replace deprecated gen_zero. Fix GOTO check options. Change graph to grapht. Add missing argument to goto_inlinet constructor call. Recompute locations after inlining. Adjust memsafety tests to new checks. Signed-off-by: František Nečas <[email protected]>
1 parent 0e367f8 commit 703a04c

33 files changed

+143
-69
lines changed

‎lib/cbmc

Submodule cbmc updated 2399 files

‎regression/memsafety/built_from_end_false/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
\[main.pointer_dereference.11\] dereference failure: deallocated dynamic object in \*p: FAILURE
7+
\[main.pointer_dereference.15\] dereference failure: deallocated dynamic object in \*p: FAILURE

‎regression/memsafety/simple_false/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
\[main.pointer_dereference.23\] dereference failure: deallocated dynamic object in \*p: FAILURE
7+
\[main.pointer_dereference.33\] dereference failure: deallocated dynamic object in \*p: FAILURE

‎src/2ls/2ls_parse_options.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,7 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
125125
options.set_option("slice", false);
126126

127127
// all checks supported by goto_check
128-
GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
128+
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
129129

130130
// check assertions
131131
if(cmdline.isset("no-assertions"))
@@ -1087,10 +1087,14 @@ bool twols_parse_optionst::process_goto_program(
10871087
goto_inlinet goto_inline(
10881088
goto_model.goto_functions,
10891089
ns,
1090-
ui_message_handler);
1090+
ui_message_handler,
1091+
false);
10911092
goto_inline();
10921093
#if IGNORE_RECURSION
10931094
recursion_detected=goto_inline.recursion_detected();
1095+
// since CBMC 5.7, inlining doesn't update location and loop numbers
1096+
goto_model.goto_functions.update();
1097+
goto_model.goto_functions.compute_loop_numbers();
10941098
#endif
10951099
}
10961100

@@ -1559,7 +1563,7 @@ void twols_parse_optionst::help()
15591563
" --round-to-zero IEEE floating point rounding mode\n"
15601564
"\n"
15611565
"Program instrumentation options:\n"
1562-
GOTO_CHECK_HELP
1566+
HELP_GOTO_CHECK
15631567
" --error-label label check that label is unreachable\n"
15641568
" --show-properties show the properties\n"
15651569
" --no-assertions ignore user assertions\n"

‎src/2ls/2ls_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ class optionst;
3131
"(function):" \
3232
"D:I:" \
3333
"(depth):(context-bound):(unwind):" \
34-
GOTO_CHECK_OPTIONS \
34+
OPT_GOTO_CHECK \
3535
"(non-incremental)" \
3636
"(no-assertions)(no-assumptions)" \
3737
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \

‎src/2ls/dynamic_cfg.h

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Peter Schrammel
1414

1515
#include <util/std_expr.h>
1616
#include <util/graph.h>
17-
#include <util/i2string.h>
1817
#include <goto-programs/goto_program.h>
1918

2019
#include <ssa/ssa_unwinder.h>
@@ -35,9 +34,9 @@ struct dynamic_cfg_idt
3534
std::string to_string() const
3635
{
3736
std::ostringstream sid;
38-
sid << i2string(pc->location_number);
37+
sid << std::to_string(pc->location_number);
3938
for(const auto &i : iteration_stack)
40-
sid << "." <<i2string(i);
39+
sid << "." <<std::to_string(i);
4140
return sid.str();
4241
}
4342
};
@@ -51,7 +50,7 @@ struct dynamic_cfg_nodet:public graph_nodet<dynamic_cfg_edget>
5150
exprt assumption;
5251
};
5352

54-
class dynamic_cfgt:public graph<dynamic_cfg_nodet>
53+
class dynamic_cfgt:public grapht<dynamic_cfg_nodet>
5554
{
5655
public:
5756
inline dynamic_cfg_nodet& operator[](const dynamic_cfg_idt &id)

‎src/2ls/preprocessing_util.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -190,7 +190,7 @@ void twols_parse_optionst::remove_multiple_dereferences(
190190
{
191191
symbolt new_symbol;
192192
new_symbol.type=member_expr.type();
193-
new_symbol.name="$deref"+i2string(var_counter++);
193+
new_symbol.name="$deref"+std::to_string(var_counter++);
194194
new_symbol.base_name=new_symbol.name;
195195
new_symbol.pretty_name=new_symbol.name;
196196
goto_model.symbol_table.add(new_symbol);
@@ -465,7 +465,7 @@ void twols_parse_optionst::split_same_symbolic_object_assignments(
465465
{
466466
symbolt tmp_symbol;
467467
tmp_symbol.type=assign.lhs().type();
468-
tmp_symbol.name="$symderef_tmp"+i2string(counter++);
468+
tmp_symbol.name="$symderef_tmp"+std::to_string(counter++);
469469
tmp_symbol.base_name=tmp_symbol.name;
470470
tmp_symbol.pretty_name=tmp_symbol.name;
471471

‎src/2ls/show.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <util/options.h>
1313
#include <util/find_symbols.h>
14-
#include <util/i2string.h>
1514
#include <util/string2int.h>
1615

1716
#include <goto-programs/read_goto_binary.h>

‎src/2ls/summary_checker_base.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Author: Peter Schrammel
1212
#include <iostream>
1313

1414
#include <util/options.h>
15-
#include <util/i2string.h>
1615
#include <util/simplify_expr.h>
1716
#include <langapi/language_util.h>
1817
#include <util/prefix.h>

‎src/2ls/summary_checker_nonterm.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Stefan Marticek
1111

1212
#include "summary_checker_nonterm.h"
1313

14-
#include <util/i2string.h>
1514
#include <util/simplify_expr.h>
1615
#include <util/prefix.h>
1716

‎src/domains/domain.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ Author: Peter Schrammel
1616
#include <set>
1717

1818
#include <util/std_expr.h>
19-
#include <util/i2string.h>
2019
#include <langapi/language_util.h>
2120
#include <util/replace_expr.h>
2221
#include <util/namespace.h>

‎src/domains/incremental_solver.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ Author: Peter Schrammel
1616
#include <set>
1717

1818
#include <solvers/flattening/bv_pointers.h>
19-
#include <util/i2string.h>
2019

2120
#include "incremental_solver.h"
2221

@@ -35,7 +34,7 @@ void incremental_solvert::new_context()
3534
solver->convert(
3635
symbol_exprt(
3736
"goto_symex::\\act$"+
38-
i2string(activation_literal_counter++), bool_typet()));
37+
std::to_string(activation_literal_counter++), bool_typet()));
3938

4039
#ifdef DEBUG_OUTPUT
4140
debug() << "new context: " << activation_literal<< eom;

‎src/domains/lexlinrank_domain.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Peter Schrammel
1414
#endif
1515

1616
#include <util/find_symbols.h>
17-
#include <util/i2string.h>
1817
#include <util/simplify_expr.h>
1918
#include <langapi/languages.h>
2019
#include <goto-symex/adjust_float_expressions.h>
@@ -372,7 +371,7 @@ exprt lexlinrank_domaint::get_row_symb_constraint(
372371

373372
symb_values[elm].c[0]=symbol_exprt(
374373
SYMB_COEFF_VAR+std::string("c!")+
375-
i2string(row)+"$"+i2string(elm)+"$0",
374+
std::to_string(row)+"$"+std::to_string(elm)+"$0",
376375
signedbv_typet(COEFF_C_SIZE)); // coefficients are signed integers
377376

378377
#ifdef DIFFERENCE_ENCODING
@@ -388,7 +387,7 @@ exprt lexlinrank_domaint::get_row_symb_constraint(
388387
{
389388
symb_values[elm].c[i]=symbol_exprt(
390389
SYMB_COEFF_VAR+std::string("c!")+
391-
i2string(row)+"$"+i2string(elm)+"$"+i2string(i),
390+
std::to_string(row)+"$"+std::to_string(elm)+"$"+std::to_string(i),
392391
signedbv_typet(COEFF_C_SIZE));
393392
#ifdef DIFFERENCE_ENCODING
394393
sum=plus_exprt(

‎src/domains/linrank_domain.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Peter Schrammel
1414
#endif
1515

1616
#include <util/find_symbols.h>
17-
#include <util/i2string.h>
1817
#include <util/simplify_expr.h>
1918
#include <langapi/languages.h>
2019
#include <util/cprover_prefix.h>
@@ -231,7 +230,7 @@ exprt linrank_domaint::get_row_symb_constraint(
231230
symb_values.c.resize(smt_model_values.size()/2);
232231
assert(!symb_values.c.empty());
233232
symb_values.c[0]=symbol_exprt(
234-
SYMB_COEFF_VAR+std::string("c!")+i2string(row)+"$0",
233+
SYMB_COEFF_VAR+std::string("c!")+std::to_string(row)+"$0",
235234
signedbv_typet(COEFF_C_SIZE)); // coefficients are signed integers
236235

237236
#ifdef DIFFERENCE_ENCODING
@@ -245,7 +244,8 @@ exprt linrank_domaint::get_row_symb_constraint(
245244
for(unsigned i=1, vals_i=2; i<symb_values.c.size(); ++i, vals_i+=2)
246245
{
247246
symb_values.c[i]=symbol_exprt(
248-
SYMB_COEFF_VAR+std::string("c!")+i2string(row)+"$"+i2string(i),
247+
SYMB_COEFF_VAR+std::string("c!")+std::to_string(row)+"$"+
248+
std::to_string(i),
249249
signedbv_typet(COEFF_C_SIZE)); // coefficients are signed integers
250250
#ifdef DIFFERENCE_ENCODING
251251
sum=plus_exprt(

‎src/domains/predabs_domain.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Peter Schrammel
1515

1616
#include <util/find_symbols.h>
1717
#include <util/prefix.h>
18-
#include <util/i2string.h>
1918
#include <util/simplify_expr.h>
2019
#include <langapi/languages.h>
2120

‎src/domains/strategy_solver_binsearch2.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,6 @@ Author: Peter Schrammel
1717

1818
#include <cassert>
1919

20-
#include <util/i2string.h>
21-
2220
#include "strategy_solver_binsearch2.h"
2321
#include "ssa/local_ssa.h"
2422
#include "util.h"
@@ -163,7 +161,7 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv)
163161
assert(sum.type()==lower.type());
164162

165163
symbol_exprt sum_bound(
166-
SUM_BOUND_VAR+i2string(sum_bound_counter++),
164+
SUM_BOUND_VAR+std::to_string(sum_bound_counter++),
167165
sum.type());
168166
solver << equal_exprt(sum_bound, sum);
169167

‎src/domains/strategy_solver_binsearch3.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,6 @@ Author: Peter Schrammel
1515

1616
#include <cassert>
1717

18-
#include <util/i2string.h>
19-
2018
#include "strategy_solver_binsearch3.h"
2119
#include "util.h"
2220

@@ -164,7 +162,7 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv)
164162
assert(sum.type()==lower.type());
165163

166164
symbol_exprt sum_bound(
167-
SUM_BOUND_VAR+i2string(sum_bound_counter++),
165+
SUM_BOUND_VAR+std::to_string(sum_bound_counter++),
168166
sum.type());
169167
solver << equal_exprt(sum_bound, sum);
170168

‎src/domains/tpolyhedra_domain.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Peter Schrammel
1515
#endif
1616

1717
#include <util/find_symbols.h>
18-
#include <util/i2string.h>
1918
#include <util/simplify_expr.h>
2019

2120
#include "tpolyhedra_domain.h"
@@ -186,7 +185,7 @@ symbol_exprt tpolyhedra_domaint::get_row_symb_value(const rowt &row)
186185
assert(row<templ.size());
187186
auto &row_expr=dynamic_cast<template_row_exprt &>(*templ[row].expr);
188187
return symbol_exprt(
189-
SYMB_BOUND_VAR+i2string(domain_number)+"$"+i2string(row),
188+
SYMB_BOUND_VAR+std::to_string(domain_number)+"$"+std::to_string(row),
190189
row_expr.type());
191190
}
192191

@@ -358,7 +357,7 @@ void tpolyhedra_domaint::rename_for_row(exprt &expr, const rowt &row)
358357
const std::string &old_id=expr.get_string(ID_identifier);
359358
if(old_id.find(SYMB_BOUND_VAR)==std::string::npos)
360359
{
361-
irep_idt id=old_id+"_"+i2string(row);
360+
irep_idt id=old_id+"_"+std::to_string(row);
362361
expr.set(ID_identifier, id);
363362
}
364363
}

‎src/solver/summarizer_fw_contexts.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@ Author: Peter Schrammel
1919

2020
#include <util/xml.h>
2121
#include <util/xml_expr.h>
22-
#include <util/i2string.h>
2322

2423
#include "summarizer_fw_contexts.h"
2524
#include "summary_db.h"
@@ -86,7 +85,7 @@ void summarizer_fw_contextst::inline_summaries(
8685
xmlt xml_cc("calling-context");
8786
xml_cc.set_attribute("function", id2string(fname));
8887
xml_cc.set_attribute(
89-
"goto_location", i2string(n_it->location->location_number));
88+
"goto_location", std::to_string(n_it->location->location_number));
9089

9190
// location
9291
const source_locationt &source_location=

‎src/ssa/dynobj_instance_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ bool dynobj_instance_domaint::merge(
206206
ai_domain_baset::locationt from,
207207
ai_domain_baset::locationt to)
208208
{
209-
bool result=false;
209+
bool result=has_values.is_false() && !other.has_values.is_false();
210210
for(auto &obj : other.must_alias_relations)
211211
{
212212
if(must_alias_relations.find(obj.first)==must_alias_relations.end())

‎src/ssa/dynobj_instance_analysis.h

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Description: In some cases, multiple instances must be used so that the
2525
#include <analyses/ai.h>
2626
#include <util/union_find.h>
2727
#include <util/options.h>
28+
#include <util/threeval.h>
2829
#include "ssa_object.h"
2930
#include "ssa_value_set.h"
3031

@@ -159,6 +160,28 @@ class dynobj_instance_domaint:public ai_domain_baset
159160
locationt from,
160161
locationt to);
161162

163+
void make_bottom() override
164+
{
165+
must_alias_relations.clear();
166+
live_pointers.clear();
167+
has_values=tvt(false);
168+
}
169+
170+
void make_top() override
171+
{
172+
must_alias_relations.clear();
173+
live_pointers.clear();
174+
has_values=tvt(true);
175+
}
176+
177+
void make_entry() override
178+
{
179+
make_top();
180+
}
181+
182+
protected:
183+
tvt has_values;
184+
162185
private:
163186
void rhs_concretisation(
164187
const exprt &guard,

0 commit comments

Comments
 (0)