From 531b856ace714d6f63c9d7971aafb07be7a97b06 Mon Sep 17 00:00:00 2001 From: xbauch Date: Tue, 25 Feb 2020 09:40:36 +0000 Subject: [PATCH 1/5] Malloc should fail on too large allocations 1: two new options to choose between fail by assert-then-assume and return null 2: `__CPROVER_max_malloc_size` is introduced 3: some tests for boundary conditions 4: user-level documentation --- doc/cprover-manual/properties.md | 16 ++++++ .../malloc-too-large/largest_representable.c | 10 ++++ .../largest_representable.desc | 9 ++++ regression/cbmc/malloc-too-large/max_size.c | 10 ++++ .../cbmc/malloc-too-large/max_size.desc | 9 ++++ .../malloc-too-large/one_byte_too_large.c | 12 +++++ .../malloc-too-large/one_byte_too_large.desc | 9 ++++ src/ansi-c/ansi_c_internal_additions.cpp | 9 ++++ src/ansi-c/library/cprover.h | 6 +++ src/ansi-c/library/stdlib.c | 50 ++++++++++++++----- src/cbmc/cbmc_parse_options.cpp | 3 ++ src/cbmc/cbmc_parse_options.h | 1 + src/util/config.cpp | 10 ++++ src/util/config.h | 9 ++++ 14 files changed, 150 insertions(+), 13 deletions(-) create mode 100644 regression/cbmc/malloc-too-large/largest_representable.c create mode 100644 regression/cbmc/malloc-too-large/largest_representable.desc create mode 100644 regression/cbmc/malloc-too-large/max_size.c create mode 100644 regression/cbmc/malloc-too-large/max_size.desc create mode 100644 regression/cbmc/malloc-too-large/one_byte_too_large.c create mode 100644 regression/cbmc/malloc-too-large/one_byte_too_large.desc diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md index 3014bf2a412..86348cda8ee 100644 --- a/doc/cprover-manual/properties.md +++ b/doc/cprover-manual/properties.md @@ -319,3 +319,19 @@ example, replacing functions or setting global variables with the `__CPROVER` prefix might make analysis impossible. To avoid doing this by accident, negative lookahead can be used. For example, `(?!__).*` matches all names not starting with `__`. + +### Malloc failure mode + +|Flag | Check | +|------------------------|-------------------------------------------------| +| `--malloc-fail-null` | in case malloc fails return NULL | +| `--malloc-fail-assert` | in case malloc fails report as failed property | + +Calling `malloc` may fail for a number of reasons and the function may return a +NULL pointer. The users can choose if and how they want the `malloc`-related +failures to occur. The option `--malloc-fail-null` results in `malloc` returning +the NULL pointer when failing. The option `--malloc-fail-assert` places +additional properties inside `malloc` that are checked and if failing the +verification is terminated (by `assume(false)`). One such property is that the +allocated size is not too large, i.e. internally representable. When neither of +those two options are used, CBMC will assume that `malloc` does not fail. diff --git a/regression/cbmc/malloc-too-large/largest_representable.c b/regression/cbmc/malloc-too-large/largest_representable.c new file mode 100644 index 00000000000..17dd78a4cd8 --- /dev/null +++ b/regression/cbmc/malloc-too-large/largest_representable.c @@ -0,0 +1,10 @@ +#include +#include +#include + +int main() +{ + int *p = malloc(__CPROVER_max_malloc_size); // try to allocate exactly the max + + return 0; +} diff --git a/regression/cbmc/malloc-too-large/largest_representable.desc b/regression/cbmc/malloc-too-large/largest_representable.desc new file mode 100644 index 00000000000..d6f9fd63d14 --- /dev/null +++ b/regression/cbmc/malloc-too-large/largest_representable.desc @@ -0,0 +1,9 @@ +CORE +largest_representable.c +--malloc-fail-assert +^EXIT=0$ +^SIGNAL=0$ +^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/malloc-too-large/max_size.c b/regression/cbmc/malloc-too-large/max_size.c new file mode 100644 index 00000000000..b8a938db857 --- /dev/null +++ b/regression/cbmc/malloc-too-large/max_size.c @@ -0,0 +1,10 @@ +#include +#include +#include + +int main() +{ + int *p = malloc(SIZE_MAX); + + return 0; +} diff --git a/regression/cbmc/malloc-too-large/max_size.desc b/regression/cbmc/malloc-too-large/max_size.desc new file mode 100644 index 00000000000..783470072e3 --- /dev/null +++ b/regression/cbmc/malloc-too-large/max_size.desc @@ -0,0 +1,9 @@ +CORE +max_size.c +--malloc-fail-assert +^EXIT=10$ +^SIGNAL=0$ +^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/malloc-too-large/one_byte_too_large.c b/regression/cbmc/malloc-too-large/one_byte_too_large.c new file mode 100644 index 00000000000..68b571cfe5b --- /dev/null +++ b/regression/cbmc/malloc-too-large/one_byte_too_large.c @@ -0,0 +1,12 @@ +#include +#include +#include + +int main() +{ + // try to allocate the smallest violating amount + int *p = malloc(__CPROVER_max_malloc_size + 1); + assert(p); + + return 0; +} diff --git a/regression/cbmc/malloc-too-large/one_byte_too_large.desc b/regression/cbmc/malloc-too-large/one_byte_too_large.desc new file mode 100644 index 00000000000..dbec5e98957 --- /dev/null +++ b/regression/cbmc/malloc-too-large/one_byte_too_large.desc @@ -0,0 +1,9 @@ +CORE +one_byte_too_large.c +--malloc-fail-null +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 2f758239409..5be02100d99 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -155,6 +155,15 @@ void ansi_c_internal_additions(std::string &code) "void *" CPROVER_PREFIX "allocate(" CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n" "const void *" CPROVER_PREFIX "alloca_object = 0;\n" + "int " CPROVER_PREFIX "malloc_failure_mode="+ + std::to_string(config.ansi_c.malloc_failure_mode)+";\n" + "int " CPROVER_PREFIX "malloc_failure_mode_return_null="+ + std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n" + "int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+ + std::to_string(config.ansi_c.malloc_failure_mode_assert_then_assume)+";\n" + CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+ + std::to_string(1 << (config.ansi_c.pointer_width - + config.bv_encoding.object_bits - 1))+";\n" // this is ANSI-C "extern " CPROVER_PREFIX "thread_local const char __func__[" diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index a070ca1302c..770be402ca0 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -16,6 +16,12 @@ extern const void *__CPROVER_malloc_object; extern __CPROVER_size_t __CPROVER_malloc_size; extern _Bool __CPROVER_malloc_is_new_array; extern const void *__CPROVER_memory_leak; +extern int __CPROVER_malloc_failure_mode; +extern __CPROVER_size_t __CPROVER_max_malloc_size; + +// malloc failure modes +extern int __CPROVER_malloc_failure_mode_return_null; +extern int __CPROVER_malloc_failure_mode_assert_then_assume; void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__)); void __CPROVER_assert(__CPROVER_bool assertion, const char *description); diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index d80ecd1264a..65a0c664732 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -115,23 +115,47 @@ inline void *malloc(__CPROVER_size_t malloc_size) // realistically, malloc may return NULL, // and __CPROVER_allocate doesn't, but no one cares __CPROVER_HIDE:; - void *malloc_res; - malloc_res = __CPROVER_allocate(malloc_size, 0); - // make sure it's not recorded as deallocated - __CPROVER_deallocated=(malloc_res==__CPROVER_deallocated)?0:__CPROVER_deallocated; + if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_return_null) + { + if(malloc_size > __CPROVER_max_malloc_size) + { + return (void *)0; + } + } + else if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_assert_then_assume) + { + __CPROVER_assert( + malloc_size <= __CPROVER_max_malloc_size, + "max allocation size exceeded"); + __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size); + } - // record the object size for non-determistic bounds checking - __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool(); - __CPROVER_malloc_object=record_malloc?malloc_res:__CPROVER_malloc_object; - __CPROVER_malloc_size=record_malloc?malloc_size:__CPROVER_malloc_size; - __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array; + void *malloc_res; + malloc_res = __CPROVER_allocate(malloc_size, 0); - // detect memory leaks - __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool(); - __CPROVER_memory_leak=record_may_leak?malloc_res:__CPROVER_memory_leak; + // make sure it's not recorded as deallocated + __CPROVER_deallocated = + (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated; - return malloc_res; + // record the object size for non-determistic bounds checking + __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); + __CPROVER_malloc_object = + record_malloc ? malloc_res : __CPROVER_malloc_object; + __CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size; + __CPROVER_malloc_is_new_array = + record_malloc ? 0 : __CPROVER_malloc_is_new_array; + + // detect memory leaks + __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool(); + __CPROVER_memory_leak = + record_may_leak ? malloc_res : __CPROVER_memory_leak; + + return malloc_res; } /* FUNCTION: __builtin_alloca */ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index ec7968b5c70..586f47947da 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1067,6 +1067,9 @@ void cbmc_parse_optionst::help() " --error-label label check that label is unreachable\n" " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) + // NOLINTNEXTLINE(whitespace/line_length) + " --malloc-fail-assert set malloc failure mode to assert-then-assume\n" + " --malloc-fail-null set malloc failure mode to return null\n" HELP_REACHABILITY_SLICER HELP_REACHABILITY_SLICER_FB " --full-slice run full slicer (experimental)\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 8d5fba3737f..32edb0ed4a4 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -50,6 +50,7 @@ class optionst; "(object-bits):" \ OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ + "(malloc-fail-assert)(malloc-fail-null)" \ OPT_XML_INTERFACE \ OPT_JSON_INTERFACE \ "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \ diff --git a/src/util/config.cpp b/src/util/config.cpp index cac312f4a97..421f1f65511 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1093,6 +1093,16 @@ bool configt::set(const cmdlinet &cmdline) bv_encoding.is_object_bits_default = false; } + if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null")) + { + throw invalid_command_line_argument_exceptiont{ + "at most one malloc failure mode is acceptable", "--malloc-fail-null"}; + } + if(cmdline.isset("malloc-fail-null")) + ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_return_null; + if(cmdline.isset("malloc-fail-assert")) + ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume; + return false; } diff --git a/src/util/config.h b/src/util/config.h index 608bbbeaf98..b2f2354689b 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -130,6 +130,15 @@ class configt bool string_abstraction; + enum malloc_failure_modet + { + malloc_failure_mode_none = 0, + malloc_failure_mode_return_null = 1, + malloc_failure_mode_assert_then_assume = 2 + }; + + malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none; + static const std::size_t default_object_bits=8; } ansi_c; From 2ad35033f7286969f18ed89cf796d15272531263 Mon Sep 17 00:00:00 2001 From: xbauch Date: Tue, 25 Feb 2020 09:41:02 +0000 Subject: [PATCH 2/5] Update the constant propagation tests More assignments due to the `__CPROVER_malloc_max_size` and `__CPROVER_malloc_failure_mode` instantiations. --- regression/goto-analyzer/constant_propagation_01/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_02/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_03/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_04/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_07/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_12/test.desc | 4 ++-- 6 files changed, 12 insertions(+), 12 deletions(-) diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index f7de54ad46b..0459ac52e6e 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 18, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index 47aea19e28b..d11810ba33b 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index 47aea19e28b..d11810ba33b 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index 47aea19e28b..d11810ba33b 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index a791723bfd2..66d94a757da 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 12, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 13, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index c605898b19d..05dbfa5fd90 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$ -- ^warning: ignoring From de0bc8b49fb206e37b87562b19cb019ad9c2bf87 Mon Sep 17 00:00:00 2001 From: xbauch Date: Tue, 25 Feb 2020 09:41:50 +0000 Subject: [PATCH 3/5] Update the expected number of assertions and test them to any number. --- regression/cbmc/Pointer_byte_extract5/no-simplify.desc | 2 +- regression/cbmc/Pointer_byte_extract5/test.desc | 2 +- regression/cbmc/array_constraints1/test.desc | 2 +- regression/cbmc/pointer-overflow1/test.desc | 2 +- regression/cbmc/r_w_ok1/test.desc | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index 36c5519b60c..a18720e2e8a 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 14 failed +\*\* 1 of 15 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 48d0d5d9c53..e1ebb7f1f4c 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 11 failed +\*\* 1 of 13 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc index 8040e5651bf..cf0c9168734 100644 --- a/regression/cbmc/array_constraints1/test.desc +++ b/regression/cbmc/array_constraints1/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 2 of 14 +^\*\* 2 of 15 -- ^warning: ignoring diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc index 2055355d938..101b9e5bff4 100644 --- a/regression/cbmc/pointer-overflow1/test.desc +++ b/regression/cbmc/pointer-overflow1/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS ^VERIFICATION FAILED$ -^\*\* 8 of 11 failed +^\*\* 8 of 12 failed -- ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE ^warning: ignoring diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc index e50051dc10b..a768254dffe 100644 --- a/regression/cbmc/r_w_ok1/test.desc +++ b/regression/cbmc/r_w_ok1/test.desc @@ -2,7 +2,7 @@ CORE main.c __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$ -^\*\* 2 of 10 failed +^\*\* 2 of 11 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ From 14682de8331cf48cdc2a76dd088f02cd88a73771 Mon Sep 17 00:00:00 2001 From: xbauch Date: Tue, 25 Feb 2020 09:42:15 +0000 Subject: [PATCH 4/5] Remove undefined behaviour from pointer-byte-extract5 specifically the C90-style struct hack with non-flexible member. --- regression/cbmc/Pointer_byte_extract5/main.i | 6 ++++-- regression/cbmc/Pointer_byte_extract5/no-simplify.desc | 7 ++++--- regression/cbmc/Pointer_byte_extract5/test.desc | 5 +++-- 3 files changed, 11 insertions(+), 7 deletions(-) diff --git a/regression/cbmc/Pointer_byte_extract5/main.i b/regression/cbmc/Pointer_byte_extract5/main.i index 023e2197a8d..1d05e271a94 100644 --- a/regression/cbmc/Pointer_byte_extract5/main.i +++ b/regression/cbmc/Pointer_byte_extract5/main.i @@ -11,13 +11,15 @@ typedef union typedef struct { int Count; - Union List[1]; + // flexible array member -- note that smt conversion does not yet support + // 0-sized arrays + Union List[0]; } Struct3; #pragma pack(pop) int main() { - Struct3 *p = malloc(sizeof(Struct3) + sizeof(Union)); + Struct3 *p = malloc(sizeof(Struct3) + 2 * sizeof(Union)); p->Count = 3; int po=0; diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index a18720e2e8a..c10bb5f3a43 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend main.i --bounds-check --32 --no-simplify ^EXIT=10$ @@ -10,5 +10,6 @@ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -- Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c. C90 did not have flexible arrays, and using arrays of size 1 was common -practice: http://c-faq.com/struct/structhack.html. We need to treat those as if -it were a zero-sized array. +practice: http://c-faq.com/struct/structhack.html. But past C90 using +non-flexible members for struct-hack is undefined, hence we changed the test to +use flexible member instead. diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index e1ebb7f1f4c..012bef91e2b 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -10,5 +10,6 @@ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -- Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c. C90 did not have flexible arrays, and using arrays of size 1 was common -practice: http://c-faq.com/struct/structhack.html. We need to treat those as if -it were a zero-sized array. +practice: http://c-faq.com/struct/structhack.html. But past C90 using +non-flexible members for struct-hack is undefined, hence we changed the test to +use flexible member instead. From 195da86ebe0d46f2474c31e1b88c65ad2f367d29 Mon Sep 17 00:00:00 2001 From: xbauch Date: Tue, 25 Feb 2020 12:50:41 +0000 Subject: [PATCH 5/5] Snapshot harness test fix before we were extracting the value for the symbol to be used as array size, but the initialization to the extracted value is not guaranteed to happen before the initialization of the array. So we avoid extracting this value from the snapshot altogether. --- .../test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc index 3b50b0169c0..cb67debb7ff 100644 --- a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc +++ b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc @@ -1,6 +1,6 @@ CORE main.c -first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5 +first,second,string_size,prefix --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5 ^SIGNAL=0$ ^EXIT=0$ VERIFICATION SUCCESSFUL