diff --git a/jbmc/regression/jbmc-strings/long_string/test_abort.desc b/jbmc/regression/jbmc-strings/long_string/test_abort.desc
index 16e6b93c80d..1bc612712b3 100644
--- a/jbmc/regression/jbmc-strings/long_string/test_abort.desc
+++ b/jbmc/regression/jbmc-strings/long_string/test_abort.desc
@@ -3,7 +3,7 @@ Test.class
--function Test.checkAbort --trace
^EXIT=10$
^SIGNAL=0$
-dynamic_object[0-9]*=\(assignment removed\)
+dynamic_object[0-9]*=.*\?.*
--
--
This tests that the object does not appear in the trace, because concretizing
diff --git a/regression/cbmc/Initialization7/test.desc b/regression/cbmc/Initialization7/test.desc
index fb5fd7bb84f..33900ad2b78 100644
--- a/regression/cbmc/Initialization7/test.desc
+++ b/regression/cbmc/Initialization7/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
main.c
^EXIT=10$
diff --git a/regression/cbmc/constant_folding2/test.desc b/regression/cbmc/constant_folding2/test.desc
index 52168c7eba4..9efefbc7362 100644
--- a/regression/cbmc/constant_folding2/test.desc
+++ b/regression/cbmc/constant_folding2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
main.c
^EXIT=0$
diff --git a/regression/cbmc/constant_folding3/main.c b/regression/cbmc/constant_folding3/main.c
new file mode 100644
index 00000000000..b8053ef508a
--- /dev/null
+++ b/regression/cbmc/constant_folding3/main.c
@@ -0,0 +1,18 @@
+typedef struct _pair
+{
+ int x;
+ int y;
+} pair;
+
+int __VERIFIER_nondet_int();
+
+int main (void)
+{
+ pair p1 = { .x = 0, .y = __VERIFIER_nondet_int() };
+ pair p2 = {};
+ p2.x = __VERIFIER_nondet_int();
+
+ __CPROVER_assert(p1.x == p2.y, "true by constant propagation");
+
+ return 0;
+}
diff --git a/regression/cbmc/constant_folding3/test.desc b/regression/cbmc/constant_folding3/test.desc
new file mode 100644
index 00000000000..201dc9bdb6e
--- /dev/null
+++ b/regression/cbmc/constant_folding3/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+--
+^warning: ignoring
diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
index cb22eaba5d0..f287ab66edd 100644
--- a/regression/cbmc/graphml_witness1/test.desc
+++ b/regression/cbmc/graphml_witness1/test.desc
@@ -54,12 +54,6 @@ main.c
21
-
- main.c
- 29
- main
-
-
main.c
15
diff --git a/regression/cbmc/struct10/main.c b/regression/cbmc/struct10/main.c
index a288fafb08f..9338d850347 100644
--- a/regression/cbmc/struct10/main.c
+++ b/regression/cbmc/struct10/main.c
@@ -1,3 +1,4 @@
+<<<<<<< HEAD
#include
struct S
@@ -8,12 +9,25 @@ struct S
struct T
{
struct S a[2];
+=======
+struct test_struct
+{
+ int a[2];
+ int b;
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
};
int main()
{
+<<<<<<< HEAD
struct T t;
t.a[1].x = 42;
assert(t.a[1].x == 42);
return 0;
+=======
+ struct test_struct test;
+ test.a[1] = 1;
+ test.b = 1;
+ __CPROVER_assert(test.a[1] == 0, "");
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
}
diff --git a/regression/cbmc/struct10/test.desc b/regression/cbmc/struct10/test.desc
index 9efefbc7362..f3132a9c5cd 100644
--- a/regression/cbmc/struct10/test.desc
+++ b/regression/cbmc/struct10/test.desc
@@ -1,8 +1,24 @@
CORE
main.c
+<<<<<<< HEAD
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
+=======
+--trace
+test.a\[1ll?\]=1 \(00000000000000000000000000000001\)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+\(\?\)
+--
+Earlier versions of non-deterministic initialisation would cause trace output
+including
+
+test.a[1l]={ .a={ 0, 1 }, .b=0 }.a[1l] (?)
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
diff --git a/regression/goto-instrument/print_global_state_size1/main.c b/regression/goto-instrument/print_global_state_size1/main.c
index 68f16e02519..08f28f20724 100644
--- a/regression/goto-instrument/print_global_state_size1/main.c
+++ b/regression/goto-instrument/print_global_state_size1/main.c
@@ -3,7 +3,7 @@
uint32_t some_global_var;
int8_t other_global_var;
-int main(int argc, char *argv[])
+int main()
{
return 0;
}
diff --git a/src/ansi-c/c_typecheck_argc_argv.cpp b/src/ansi-c/c_typecheck_argc_argv.cpp
index dfc752c8e19..7ff32a4810d 100644
--- a/src/ansi-c/c_typecheck_argc_argv.cpp
+++ b/src/ansi-c/c_typecheck_argc_argv.cpp
@@ -42,6 +42,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
argc_symbol.type=op0.type();
argc_symbol.is_static_lifetime=true;
argc_symbol.is_lvalue=true;
+ argc_symbol.value = side_effect_expr_nondett(op0.type());
if(argc_symbol.type.id()!=ID_signedbv &&
argc_symbol.type.id()!=ID_unsignedbv)
@@ -81,6 +82,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
argv_symbol.type=argv_type;
argv_symbol.is_static_lifetime=true;
argv_symbol.is_lvalue=true;
+ argv_symbol.value = side_effect_expr_nondett(argv_type);
symbolt *argv_new_symbol;
move_symbol(argv_symbol, argv_new_symbol);
@@ -99,6 +101,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
envp_size_symbol.name="envp_size'";
envp_size_symbol.type=op0.type(); // same type as argc!
envp_size_symbol.is_static_lifetime=true;
+ envp_size_symbol.value = side_effect_expr_nondett(op0.type());
move_symbol(envp_size_symbol, envp_new_size_symbol);
if(envp_symbol.type.id()!=ID_pointer)
@@ -113,6 +116,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
envp_symbol.type.id(ID_array);
envp_symbol.type.add(ID_size).swap(size_expr);
+ envp_symbol.value = side_effect_expr_nondett(envp_symbol.type);
symbolt *envp_new_symbol;
move_symbol(envp_symbol, envp_new_symbol);
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 9b362b00ff9..dffaa901bb1 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -145,13 +145,15 @@ static bool filter_out(
const goto_tracet::stepst::const_iterator &prev_it,
goto_tracet::stepst::const_iterator &it)
{
+ // use the goto program's assignment type as declarations may be
+ // recorded as (non-deterministic) assignments in the trace
if(it->hidden &&
(!it->pc->is_assign() ||
to_code_assign(it->pc->code).rhs().id()!=ID_side_effect ||
to_code_assign(it->pc->code).rhs().get(ID_statement)!=ID_nondet))
return true;
- if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
+ if(!it->pc->is_assign() && !it->is_goto() && !it->is_assert())
return true;
// we filter out steps with the same source location
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index fef369b07e8..593a8530330 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include "goto_symex.h"
#include
+#include
unsigned goto_symext::dynamic_counter=0;
@@ -27,3 +28,31 @@ nondet_symbol_exprt symex_nondet_generatort::operator()(typet &type)
nondet_symbol_exprt new_expr(identifier, type);
return new_expr;
}
+<<<<<<< HEAD
+=======
+
+void goto_symext::replace_nondet(exprt &expr)
+{
+ if(expr.id()==ID_side_effect &&
+ expr.get(ID_statement)==ID_nondet)
+ {
+ exprt nondet = nondet_initializer(
+ expr.type(), expr.source_location(), ns, log.get_message_handler());
+
+ // recursively replace nondet fields in structs or arrays
+ if(nondet.id() != ID_side_effect)
+ {
+ replace_nondet(nondet);
+ expr.swap(nondet);
+ return;
+ }
+
+ nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
+ new_expr.add_source_location()=expr.source_location();
+ expr.swap(new_expr);
+ }
+ else
+ Forall_operands(it, expr)
+ replace_nondet(*it);
+}
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 0921be1c5d5..805ea12acc8 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -250,7 +250,26 @@ class goto_symext
// guards
+<<<<<<< HEAD
const irep_idt guard_identifier;
+=======
+ irep_idt guard_identifier;
+
+ // symex
+ irep_idt init_l1;
+
+ virtual void symex_transition(
+ statet &,
+ goto_programt::const_targett to,
+ bool is_backwards_goto=false);
+
+ virtual void symex_transition(statet &state)
+ {
+ goto_programt::const_targett next=state.source.pc;
+ ++next;
+ symex_transition(state, next);
+ }
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
virtual void symex_goto(statet &);
virtual void symex_start_thread(statet &);
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 7a1bae4a163..b9737fe00d8 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -155,6 +155,8 @@ class goto_symex_is_constantt : public is_constantt
*/
return false;
}
+ else if(expr.id() == ID_nondet_symbol)
+ return true;
return is_constantt::is_constant(expr);
}
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index b9bdf010261..0f97809b422 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -178,9 +178,23 @@ void goto_symext::symex_allocate(
}
else
{
+<<<<<<< HEAD
const exprt nondet = build_symex_nondet(object_type);
const code_assignt assignment(value_symbol.symbol_expr(), nondet);
symex_assign(state, assignment);
+=======
+ side_effect_expr_nondett init(object_type);
+ replace_nondet(init);
+
+ guardt guard;
+ symex_assign_symbol(
+ state,
+ ssa_exprt(value_symbol.symbol_expr()),
+ nil_exprt(),
+ init,
+ guard,
+ symex_targett::assignment_typet::HIDDEN);
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
}
exprt rhs;
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index a0f964feb48..055dfe8f5e9 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include
-#include
-
#include
void goto_symext::symex_decl(statet &state)
@@ -45,6 +43,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
state.rename(ssa.type(), l1_identifier, ns);
ssa.update_type();
+<<<<<<< HEAD
// in case of pointers, put something into the value set
if(ns.follow(expr.type()).id()==ID_pointer)
{
@@ -76,6 +75,25 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
state.record_events=false;
state.rename(ssa, ns);
state.record_events=record_events;
+=======
+ // L2 renaming
+ // inlining may yield multiple declarations of the same identifier
+ // within the same L1 context
+ if(state.level2.current_names.find(l1_identifier)==
+ state.level2.current_names.end())
+ state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
+ init_l1 = l1_identifier;
+
+ // optimisation: skip non-deterministic initialisation if the next instruction
+ // will take care of initialisation (but ensure int x=x; is handled properly)
+ goto_programt::const_targett next = std::next(state.source.pc);
+ if(
+ next->is_assign() && to_code_assign(next->code).lhs() == expr &&
+ to_code_assign(next->code).rhs().is_constant())
+ {
+ return;
+ }
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
// we hide the declaration of auxiliary variables
// and if the statement itself is hidden
@@ -84,10 +102,16 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
state.top().hidden_function ||
state.source.pc->source_location.get_hide();
- target.decl(
- state.guard.as_expr(),
+ side_effect_expr_nondett init(ssa.type());
+ replace_nondet(init);
+
+ guardt guard;
+ symex_assign_symbol(
+ state,
ssa,
- state.source,
+ nil_exprt(),
+ init,
+ guard,
hidden?
symex_targett::assignment_typet::HIDDEN:
symex_targett::assignment_typet::STATE);
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index b9bb0828e64..5120dfafd0e 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -63,16 +63,13 @@ void static_lifetime_init(
continue;
// special values
- if(identifier==CPROVER_PREFIX "constant_infinity_uint" ||
- identifier==CPROVER_PREFIX "memory" ||
- identifier=="__func__" ||
- identifier=="__FUNCTION__" ||
- identifier=="__PRETTY_FUNCTION__" ||
- identifier=="argc'" ||
- identifier=="argv'" ||
- identifier=="envp'" ||
- identifier=="envp_size'")
+ if(
+ identifier == CPROVER_PREFIX "constant_infinity_uint" ||
+ identifier == CPROVER_PREFIX "memory" || identifier == "__func__" ||
+ identifier == "__FUNCTION__" || identifier == "__PRETTY_FUNCTION__")
+ {
continue;
+ }
// just for linking
if(has_prefix(id, CPROVER_PREFIX "architecture_"))
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index bfad48312d8..62d30444d28 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -389,7 +389,9 @@ void value_sett::get_value_set_rec(
const typet &expr_type=ns.follow(expr.type());
- if(expr.id()==ID_unknown || expr.id()==ID_invalid)
+ if(
+ expr.id() == ID_unknown || expr.id() == ID_invalid ||
+ expr.id() == ID_nondet_symbol)
{
insert(dest, exprt(ID_unknown, original_type));
}
@@ -1195,9 +1197,9 @@ void value_sett::assign(
"type:\n"+type.pretty();
rhs_member=make_member(rhs, name, ns);
-
- assign(lhs_member, rhs_member, ns, false, add_to_sets);
}
+
+ assign(lhs_member, rhs_member, ns, false, add_to_sets);
}
}
else if(type.id()==ID_array)
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index cd3b17f23f1..f572a9df18b 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -182,7 +182,8 @@ void arrayst::collect_arrays(const exprt &a)
else if(a.id()==ID_member)
{
DATA_INVARIANT(
- to_member_expr(a).struct_op().id()==ID_symbol,
+ to_member_expr(a).struct_op().id() == ID_symbol ||
+ to_member_expr(a).struct_op().id() == ID_nondet_symbol,
("unexpected array expression: member with `"+
a.op0().id_string()+"'").c_str());
}
@@ -458,8 +459,10 @@ void arrayst::add_array_constraints(
expr.id()==ID_string_constant)
{
}
- else if(expr.id()==ID_member &&
- to_member_expr(expr).struct_op().id()==ID_symbol)
+ else if(
+ expr.id() == ID_member &&
+ (to_member_expr(expr).struct_op().id() == ID_symbol ||
+ to_member_expr(expr).struct_op().id() == ID_nondet_symbol))
{
}
else if(expr.id()==ID_byte_update_little_endian ||
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index d67e65c1993..0e551b72b95 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -51,9 +51,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)
// record type if array is a symbol
- if(array.id()==ID_symbol)
- map.get_map_entry(
- to_symbol_expr(array).get_identifier(), array_type);
+ if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
+ map.get_map_entry(array.get(ID_identifier), array_type);
// make sure we have the index in the cache
convert_bv(index);
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 1b4b61ac8b6..2d975465b57 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1120,7 +1120,7 @@ static exprt substitute_array_access(
*if_expr, index_expr.index(), symbol_generator, left_propagate);
INVARIANT(
- array.is_nil() || array.id() == ID_symbol,
+ array.is_nil() || array.id() == ID_symbol || array.id() == ID_nondet_symbol,
std::string(
"in case the array is unknown, it should be a symbol or nil, id: ")
+ id2string(array.id()));
@@ -1693,7 +1693,9 @@ static void initial_index_set(
const exprt &s,
const exprt &i)
{
- PRECONDITION(s.id() == ID_symbol || s.id() == ID_array || s.id() == ID_if);
+ PRECONDITION(
+ s.id() == ID_symbol || s.id() == ID_nondet_symbol || s.id() == ID_array ||
+ s.id() == ID_if);
if(s.id() == ID_array)
{
for(std::size_t j = 0; j < s.operands().size(); ++j)
@@ -1995,7 +1997,8 @@ exprt string_refinementt::get(const exprt &expr) const
}
INVARIANT(
- array.is_nil() || array.id() == ID_symbol,
+ array.is_nil() || array.id() == ID_symbol ||
+ array.id() == ID_nondet_symbol,
std::string(
"apart from symbols, array valuations can be interpreted as "
"sparse arrays, id: ") +
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index b94d1ae2e8a..36c257ce091 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -276,8 +276,12 @@ bool is_constantt::is_constant_address_of(const exprt &expr) const
return is_constant(deref.pointer());
}
- else if(expr.id() == ID_string_constant)
+ else if(
+ expr.id() == ID_string_constant || expr.id() == ID_array ||
+ expr.id() == ID_struct || expr.id() == ID_union)
+ {
return true;
+ }
return false;
}