From 49c4b3ac06d62aaf74cd1bc6edc903fef3872ca2 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 30 Sep 2016 12:58:44 +0100 Subject: [PATCH 1/2] Fix address space limit test. Fixes #243 --- src/solvers/flattening/bv_pointers.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index b4d0382f27a..e23dccace5e 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -795,7 +795,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv) { std::size_t a=pointer_logic.add_object(expr); - if(a==(std::size_t(1)>>object_bits)) + if(a==(std::size_t(1)< Date: Wed, 25 Jan 2017 11:48:53 +0000 Subject: [PATCH 2/2] Add address space size limit regression test --- regression/cbmc/address_space_size_limit1/test.c | 16 ++++++++++++++++ .../cbmc/address_space_size_limit1/test.desc | 5 +++++ 2 files changed, 21 insertions(+) create mode 100644 regression/cbmc/address_space_size_limit1/test.c create mode 100644 regression/cbmc/address_space_size_limit1/test.desc diff --git a/regression/cbmc/address_space_size_limit1/test.c b/regression/cbmc/address_space_size_limit1/test.c new file mode 100644 index 00000000000..a4f9e047262 --- /dev/null +++ b/regression/cbmc/address_space_size_limit1/test.c @@ -0,0 +1,16 @@ + +#include +#include + +int main(int argc, char** argv) +{ + + int i; + char* c; + for(i=0; i<300; ++i) + { + c=(char*)malloc(1); + assert(c!=(char*)0); + } + +} diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc new file mode 100644 index 00000000000..9dcfb8970aa --- /dev/null +++ b/regression/cbmc/address_space_size_limit1/test.desc @@ -0,0 +1,5 @@ +CORE +test.c +--no-simplify --unwind 300 +too many variables +--