Merge pull request #6212 from NlightNFotis/add_5952_tests

Include tests from reported issue cbmc#5952.

Author: NlightNFotis

regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+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));
+}

regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *data;
+  data = nondet() ? malloc(1) : malloc(2);
+  assert(__CPROVER_OBJECT_SIZE(data) <= 2);
+}

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

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