Skip to content

Commit ac8efba

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #148 from FrNecas/frnecas-cbmc-5.7
Update to CBMC 5.7
2 parents 0e367f8 + fbbd676 commit ac8efba

34 files changed

+144
-70
lines changed

‎lib/cbmc

Submodule cbmc updated 2399 files

‎regression/memsafety/built_from_end_false/test.desc

+1-1
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

+1-1
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

+7-3
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

+1-1
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

+3-4
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

+2-2
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

-1
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

-1
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

-1
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/2ls/version.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,6 @@ Author: Peter Schrammel
1212
#ifndef CPROVER_2LS_2LS_VERSION_H
1313
#define CPROVER_2LS_2LS_VERSION_H
1414

15-
#define TWOLS_VERSION "0.9.1"
15+
#define TWOLS_VERSION "0.9.2"
1616

1717
#endif

‎src/domains/domain.h

-1
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

+1-2
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

+2-3
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

+3-3
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

-1
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

+1-3
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

+1-3
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

+2-3
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

+1-2
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

+1-1
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

+23
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)