From f585e6087f8aa2115ea23539e6fc25f99867673f Mon Sep 17 00:00:00 2001 From: xbauch Date: Mon, 22 Jul 2019 10:39:15 +0100 Subject: [PATCH 1/2] Stop asserting positive array size when generating non-deterministic arrays. Zero-sized arrays are (unfortunately) legal C construct (as for example the regression test shows). --- regression/cbmc/Struct_Hack_Initialization/main.c | 13 +++++++++++++ .../cbmc/Struct_Hack_Initialization/test.desc | 13 +++++++++++++ src/ansi-c/c_nondet_symbol_factory.cpp | 1 - 3 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc/Struct_Hack_Initialization/main.c create mode 100644 regression/cbmc/Struct_Hack_Initialization/test.desc diff --git a/regression/cbmc/Struct_Hack_Initialization/main.c b/regression/cbmc/Struct_Hack_Initialization/main.c new file mode 100644 index 00000000000..f1a9c874834 --- /dev/null +++ b/regression/cbmc/Struct_Hack_Initialization/main.c @@ -0,0 +1,13 @@ +#include + +typedef struct stritem +{ + unsigned nkey; + unsigned cas[]; +} item; + +int foo(item *it) +{ + assert(it->cas[0] == 0); + return 0; +} diff --git a/regression/cbmc/Struct_Hack_Initialization/test.desc b/regression/cbmc/Struct_Hack_Initialization/test.desc new file mode 100644 index 00000000000..5ec6fe729da --- /dev/null +++ b/regression/cbmc/Struct_Hack_Initialization/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--function foo --bounds-check --pointer-check +^\[foo.assertion.1\] line \d+ assertion it->cas\[0\] == 0: FAILURE$ +^\[foo.array_bounds.3\] line \d+ array.cas upper bound in it->cas\[\(.*\)0\]: FAILURE$ +^\[foo.array_bounds.2\] line \d+ array.cas dynamic object upper bound in it->cas\[\(.*\)0\]: FAILURE$ +^\[foo.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in it->cas: SUCCESS$ +^\[foo.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in it->cas: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 5e91a9a2a73..5047a756425 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -163,7 +163,6 @@ void symbol_factoryt::gen_nondet_array_init( const auto &size = array_type.size(); PRECONDITION(size.id() == ID_constant); auto const array_size = numeric_cast_v(to_constant_expr(size)); - DATA_INVARIANT(array_size > 0, "Arrays should have positive size"); for(size_t index = 0; index < array_size; ++index) { gen_nondet_init( From 30923ab6a23ef7f7f0f9e9e6c099e167058daf11 Mon Sep 17 00:00:00 2001 From: xbauch Date: Tue, 30 Jul 2019 09:58:40 +0100 Subject: [PATCH 2/2] Also skip flattening zero-sized arrays when converting to SMT2 queries. --- src/solvers/smt2/smt2_conv.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 1868627547a..184cc479bc6 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2672,7 +2672,14 @@ void smt2_convt::convert_struct(const struct_exprt &expr) // may need to flatten array-theory arrays in there if(op.type().id() == ID_array) - flatten_array(op); + { + const array_typet &array_type = to_array_type(op.type()); + const auto &size_expr = array_type.size(); + CHECK_RETURN(size_expr.id() == ID_constant); + + if(numeric_cast_v(to_constant_expr(size_expr)) != 0) + flatten_array(op); + } else convert_expr(op); @@ -4526,7 +4533,11 @@ void smt2_convt::convert_type(const typet &type) { if(use_datatypes) { - out << datatype_map.at(type); + const typet &struct_type = type.id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(type)) + : type; + CHECK_RETURN(datatype_map.count(struct_type) > 0); + out << datatype_map.at(struct_type); } else {