state encoding part II

Author: kroening

regression/cprover/Makefile

@@ -1,13 +1,13 @@
-default: tests.log
+default: test-no-p
 
 include ../../src/config.inc
 include ../../src/common
 
 test:
 	@../test.pl -e -p -c '../../../src/cprover/cprover'
 
-tests.log:
-	@../test.pl -e -p -c '../../../src/cprover/cprover'
+test-no-p:
+	@../test.pl -e -c '../../../src/cprover/cprover'
 
 clean:
 	$(RM) tests.log

regression/cprover/arrays/array1.desc

@@ -1,6 +1,6 @@
 CORE
 array1.c
---text --solve
+--text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, 1\):=10\]\)$

regression/cprover/arrays/array2.desc

@@ -1,6 +1,6 @@
 CORE
 array2.c
---text --solve
+--text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state \. \(S23\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)$

regression/cprover/arrays/array_literal1.c

@@ -0,0 +1,8 @@
+int array[10] = { 0, 1, 2, 3, 4 };
+
+int main()
+{
+  __CPROVER_assert(array[0l] == 0, "property 1"); // passes
+  __CPROVER_assert(array[1l] == 1, "property 2"); // passes
+  return 0;
+}

regression/cprover/arrays/array_literal1.desc

@@ -0,0 +1,8 @@
+CORE
+array_literal1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
+--

regression/cprover/arrays/array_literal2.c

@@ -0,0 +1,8 @@
+int array[] = {'a', 'b', 'c', 'd', 'e', 'f'};
+
+int main()
+{
+  int i;
+  if(i >= 0 && i <= 5)
+    __CPROVER_assert(array[i] == 'a' + i, "property 1"); // passes
+}

regression/cprover/arrays/array_set1.c

@@ -0,0 +1,8 @@
+int array[10];
+
+int main()
+{
+  __CPROVER_array_set(array, 123);
+  __CPROVER_assert(array[5l] == 123, "property 1"); // passes
+  return 0;
+}

regression/cprover/arrays/array_set1.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+array_set1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--

regression/cprover/arrays/iterate_over_array2.desc

@@ -3,5 +3,5 @@ iterate_over_array2.c
 --safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\[find_zero\.pointer\.1\] line \d+ pointer safe: SUCCESS$
+^\[find_zero\.pointer\.1\] line \d+ pointer .* safe: SUCCESS$
 --

regression/cprover/aws-c-common/aws_hash_table_clear.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+aws_hash_table_clear_contract.c
+-I aws-c-common/include aws-c-common/source/hash_table.c
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/aws_hash_table_clear_contract.c

@@ -0,0 +1,15 @@
+// Function: aws_hash_table_clear
+// Source: source/hash_table.c
+
+#include <aws/common/hash_table.h>
+
+// void aws_hash_table_clear(struct aws_hash_table *map)
+
+int main()
+{
+  struct aws_hash_table *map;
+
+  aws_hash_table_clear(map);
+
+  return 0;
+}

regression/cprover/aws-c-common/aws_hash_table_eq.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+aws_hash_table_eq_contract.c
+-I aws-c-common/include aws-c-common/source/hash_table.c
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/aws_hash_table_eq_contract.c

@@ -0,0 +1,20 @@
+// Function: aws_hash_table_eq
+// Source: source/hash_table.c
+
+#include <aws/common/hash_table.h>
+
+// bool aws_hash_table_eq(
+//   const struct aws_hash_table *a,
+//   const struct aws_hash_table *b,
+//   aws_hash_callback_eq_fn *value_eq)
+
+int main()
+{
+  const struct aws_hash_table *a;
+  const struct aws_hash_table *b;
+  aws_hash_callback_eq_fn *value_eq;
+
+  aws_hash_table_eq(a, b, value_eq);
+
+  return 0;
+}

regression/cprover/aws-c-common/aws_hash_table_foreach.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+aws_hash_table_foreach_contract.c
+-I aws-c-common/include aws-c-common/source/hash_table.c
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/aws_hash_table_foreach_contract.c

@@ -0,0 +1,20 @@
+// Function: aws_hash_table_foreach
+// Source: source/hash_table.c
+
+#include <aws/common/hash_table.h>
+
+// int aws_hash_table_foreach(
+//   struct aws_hash_table *map,
+//   int (*callback)(void *context, struct aws_hash_element *pElement),
+//   void *context)
+
+int main()
+{
+  struct aws_hash_table *map;
+  int (*callback)(void *context, struct aws_hash_element *pElement);
+  void *context;
+
+  aws_hash_table_foreach(map, callback, context);
+
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_hash_table_clear_contract.c

@@ -1,6 +1,6 @@
 CORE
 assume1.c
---text --solve
+--text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
 ^ \(\d+\) ∀ ς : state \. true ⇒ SInitial\(ς\)$
@@ -9,7 +9,7 @@ assume1.c
 ^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$
 ^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
 ^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=nondet::S25\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=nondet::S25-0\]\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --

regression/cprover/aws-c-common/todo/aws_hash_table_eq_contract.c

@@ -1,6 +1,6 @@
 CORE
 basic1.c
---text --solve
+--text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
 ^ \(\d+\) ∀ ς : state \. true ⇒ SInitial\(ς\)$

regression/cprover/aws-c-common/todo/aws_hash_table_foreach.desc

@@ -1,6 +1,6 @@
 CORE
 basic2.c
---text --solve
+--text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$

regression/cprover/aws-c-common/todo/aws_hash_table_foreach_contract.c

@@ -1,6 +1,6 @@
 CORE
 basic3.c
---text --solve
+--text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
 \(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)

regression/cprover/basic/assume1.desc

@@ -1,6 +1,6 @@
 CORE
 basic4.c
---text --solve
+--text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$

regression/cprover/basic/basic1.desc

@@ -1,10 +1,10 @@
 CORE
 basic5.c
---text --solve
+--text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
-^\(\d+\) S23 = S22$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
 ^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
 ^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
 ^\(\d+\) S25 = S24$

regression/cprover/basic/basic2.desc

@@ -1,6 +1,6 @@
 CORE
 basic6.c
---text --solve
+--text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
 ^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$

regression/cprover/basic/basic3.desc

@@ -0,0 +1,13 @@
+struct S
+{
+  int x, y;
+};
+
+extern struct S some_struct;
+
+int main()
+{
+  // should fail
+  __CPROVER_assert(some_struct.x == some_struct.y, "property 1");
+  return 0;
+}

regression/cprover/basic/basic4.desc

@@ -0,0 +1,7 @@
+CORE
+extern1.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
+--

regression/cprover/basic/basic5.desc

@@ -1,12 +1,12 @@
 CORE
 nondet1.c
---text --solve
+--text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22-0\]\)$
 ^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
 ^\(\d+\) S23 = S22$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24-0\]\)$
 ^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
 ^\(\d+\) S25 = S24$
 ^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$

regression/cprover/basic/basic6.desc

@@ -1,6 +1,6 @@
 CORE
 branching1.c
---text --solve
+--text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S21T\(\ς\)$

regression/cprover/basic/extern1.c

@@ -1,6 +1,6 @@
 CORE
 branching2.c
---text --solve
+--text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S22T\(ς\)$

regression/cprover/basic/extern1.desc

@@ -3,6 +3,6 @@ cstring_is_memory_safe1.c
 --safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.pointer\.1\] line \d+ pointer safe: SUCCESS$
-^\[main\.pointer\.2\] line \d+ pointer safe: REFUTED$
+^\[main\.pointer\.1\] line \d+ pointer p safe: SUCCESS$
+^\[main\.pointer\.2\] line \d+ pointer .* safe: REFUTED$
 --

regression/cprover/basic/nondet1.desc

@@ -3,5 +3,5 @@ cstring_is_memory_safe2.c
 --safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.pointer\.1\] line \d+ pointer safe: SUCCESS$
+^\[main\.pointer\.1\] line \d+ pointer .* safe: SUCCESS$
 --

regression/cprover/branching/branching1.desc

@@ -3,5 +3,5 @@ cstring_is_memory_safe3.c
 --safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.pointer\.1\] line \d+ pointer safe: SUCCESS$
+^\[main\.pointer\.1\] line \d+ pointer .* safe: SUCCESS$
 --

regression/cprover/branching/branching2.desc

@@ -0,0 +1,11 @@
+const char *HEX_CHARS = "0123456789abcdef";
+
+int main()
+{
+  unsigned char input;
+  char output;
+
+  output = HEX_CHARS[input & 0xf];
+
+  return 0;
+}

regression/cprover/cstrings/cstring_is_memory_safe1.desc

@@ -1,5 +1,5 @@
 CORE
-aws_hash_table_eq_contract.c
+string_literal2.c
 --safety
 ^EXIT=0$
 ^SIGNAL=0$

regression/cprover/cstrings/cstring_is_memory_safe2.desc

@@ -0,0 +1,7 @@
+int main()
+{
+  char *p = "0123";
+  __CPROVER_assert(__CPROVER_r_ok(p), "property 1"); // passes
+  __CPROVER_assert(__CPROVER_w_ok(p), "property 2"); // fails
+  return 0;
+}

regression/cprover/cstrings/cstring_is_memory_safe3.desc

@@ -0,0 +1,8 @@
+CORE
+string_literal3.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
+--

regression/cprover/cstrings/string_literal2.c

@@ -0,0 +1,7 @@
+int main()
+{
+  char *p = "0123";
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(p) == 5, "property 1"); // passes
+  __CPROVER_assert(__CPROVER_LIVE_OBJECT(p), "property 2");      // passes
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_hash_table_eq.desc renamed to regression/cprover/cstrings/string_literal2.desc

@@ -0,0 +1,6 @@
+CORE
+string_literal4.c
+
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/cstrings/string_literal3.c

@@ -1,6 +1,6 @@
 CORE
 basic-float1.c
---text --solve
+--text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$