diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c new file mode 100644 index 00000000000..f052e2a6ba4 --- /dev/null +++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c @@ -0,0 +1,24 @@ +#include +#include +#include + +bool validate(const char *data, unsigned allocated) +{ + // clang-format off + bool check_1 = (data == NULL ==> allocated == 0); + bool check_2 = (allocated != 0 ==> __CPROVER_r_ok(data, allocated)); + // clang-format on + return check_1 && check_2; +} + +void main() +{ + char *data; + unsigned allocated; + + data = (allocated == 0) ? NULL : malloc(allocated); + + __CPROVER_assume(validate(data, allocated)); + + assert(validate(data, allocated)); +} diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c new file mode 100644 index 00000000000..c92fed9cdad --- /dev/null +++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c @@ -0,0 +1,9 @@ +#include +#include + +void main() +{ + char *data; + data = nondet() ? malloc(1) : malloc(2); + assert(__CPROVER_OBJECT_SIZE(data) <= 2); +} diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc new file mode 100644 index 00000000000..1f09f9e1000 --- /dev/null +++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc @@ -0,0 +1,12 @@ +KNOWNBUG broken-smt-backend +original_repro.c +--smt2 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +\[main.assertion.\d\] line \d+ assertion validate\(data, allocated\): SUCCESS +-- +\[main.assertion.\d\] line \d+ assertion validate\(data, allocated\): FAILURE +-- +This is the original code that demonstrates the issue described in +https://github.com/diffblue/cbmc/issues/5952 diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc new file mode 100644 index 00000000000..eec1fc3fd4f --- /dev/null +++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc @@ -0,0 +1,12 @@ +CORE +short.c +--smt2 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: SUCCESS +-- +\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: FAILURE +-- +This is the reduced version of the issue described in +https://github.com/diffblue/cbmc/issues/5952