Merge pull request #149 from diffblue/release-18/feature/write-stack

Write Stack

Author: thk123

regression/goto-analyzer/sensitivity-test-common-files/pointer_to_array_sensitivity_tests.c

@@ -8,20 +8,21 @@ int main(int argc, char *argv[])
   int *p=a;
   __CPROVER_assert(p==&a[0], "p==&a[0]");
 
+  // Read through pointer
   __CPROVER_assert(*p==1, "*p==1");
 
+  // Read through offset pointer
   __CPROVER_assert(p[1]==2, "p[1]==2");
   __CPROVER_assert(1[p]==2, "1[p]==2");
 
   __CPROVER_assert(*(p+1)==2, "*(p+1)==2");
   __CPROVER_assert(*(1+p)==2, "*(1+p)==2");
 
-  __CPROVER_assert(*(p-1)==1, "*(p-1)==1");
-
   // Test pointer arithmetic
   int *q=&a[1];
   __CPROVER_assert(q==p+1, "q==p+1");
   __CPROVER_assert(*q==2, "*q==2");
+  __CPROVER_assert(*(q-1)==1, "*(q-1)==1");
 
   // Test pointer diffs
   ptrdiff_t x=1;

regression/goto-analyzer/sensitivity-test-common-files/pointer_to_struct_sensitivity_tests.c

@@ -24,5 +24,30 @@ int main(int argc, char *argv[])
   __CPROVER_assert(p->b==2.0, "p->b==2.0");
   __CPROVER_assert(p->b==1.0, "p->b==1.0");
 
+  // pointers to components
+  int * comp_p = &x.a;
+  __CPROVER_assert(comp_p==&x.a, "comp_p==&x.a");
+  __CPROVER_assert(comp_p==&x.b, "comp_p==&x.b");
+  __CPROVER_assert(*comp_p==0, "*comp_p==0");
+  __CPROVER_assert(*comp_p==1, "*comp_p==1");
+
+  float * compb_p = &x.b;
+  __CPROVER_assert(compb_p==&x.a, "compb_p==&x.a");
+  __CPROVER_assert(compb_p==&x.b, "compb_p==&x.b");
+  __CPROVER_assert(*compb_p==2.0, "*compb_p==2.0");
+  __CPROVER_assert(*compb_p==1.0, "*compb_p==1.0");
+
+  // Use pointer implicitly pointing at the first component
+  int * implicit_p = &x;
+  __CPROVER_assert(implicit_p==&x.a, "implicit_p==&x.a");
+  __CPROVER_assert(implicit_p==&x, "implicit_p==&x");
+  __CPROVER_assert(*implicit_p==0, "*implicit_p==0");
+  __CPROVER_assert(*implicit_p==1, "*implicit_p==1");
+
+  // Write through pointer implicitly pointing at the first component
+  *implicit_p=5;
+  __CPROVER_assert(x.a==5, "x.a==5");
+  __CPROVER_assert(x.a==1, "x.a==1");
+
   return 0;
 }

regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_array_of_constants_array.c
---variable --arrays --verify
+--variable --arrays --verify --pointers
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* a\[1\]\[2\]==0: Success$
@@ -17,10 +17,10 @@ sensitivity_test_constants_array_of_constants_array.c
 ^\[main.assertion.12\] .* 1\[b\]\[2\]==0: Failure \(if reachable\)$
 ^\[main.assertion.13\] .* \*\(1\[b\]\+2\)==5: Success$
 ^\[main.assertion.14\] .* \*\(1\[b\]\+2\)==0: Failure \(if reachable\)$
-^\[main.assertion.15\] .* \(\*\(1\+b\)\)\[2\]==5: Unknown$
-^\[main.assertion.16\] .* \(\*\(1\+b\)\)\[2\]==0: Unknown$
-^\[main.assertion.17\] .* \*\(\*\(1\+b\)\+2\)==5: Unknown$
-^\[main.assertion.18\] .* \*\(\*\(1\+b\)\+2\)==0: Unknown$
+^\[main.assertion.15\] .* \(\*\(1\+b\)\)\[2\]==5: Success$
+^\[main.assertion.16\] .* \(\*\(1\+b\)\)\[2\]==0: Failure \(if reachable\)$
+^\[main.assertion.17\] .* \*\(\*\(1\+b\)\+2\)==5: Success$
+^\[main.assertion.18\] .* \*\(\*\(1\+b\)\+2\)==0: Failure \(if reachable\)$
 ^\[main.assertion.19\] .* 2\[1\[b\]\]==5: Success$
 ^\[main.assertion.20\] .* 2\[1\[b\]\]==0: Failure \(if reachable\)$
 ^\[main.assertion.21\] .* \*\(2\+1\[b\]\)==5: Unknown$

regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/test.desc

@@ -13,14 +13,14 @@ sensitivity_test_constants_array_of_constants_pointer.c
 ^\[main.assertion.8\] .* \*b\[1\]==13: Failure \(if reachable\)$
 ^\[main.assertion.9\] .* \*\(b\+1\)==&b1: Success$
 ^\[main.assertion.10\] .* \*\(b\+1\)==&b3: Failure \(if reachable\)$
-^\[main.assertion.11\] .* \*\(1\+b\)==&b1: Unknown$
-^\[main.assertion.12\] .* \*\(1\+b\)==&b3: Unknown$
+^\[main.assertion.11\] .* \*\(1\+b\)==&b1: Success$
+^\[main.assertion.12\] .* \*\(1\+b\)==&b3: Failure \(if reachable\)$
 ^\[main.assertion.13\] .* 1\[b\]==&b1: Success$
 ^\[main.assertion.14\] .* 1\[b\]==&b3: Failure \(if reachable\)$
 ^\[main.assertion.15\] .* \*\*\(b\+1\)==11: Success$
 ^\[main.assertion.16\] .* \*\*\(b\+1\)==13: Failure \(if reachable\)$
-^\[main.assertion.17\] .* \*\*\(1\+b\)==11: Unknown$
-^\[main.assertion.18\] .* \*\*\(1\+b\)==13: Unknown$
+^\[main.assertion.17\] .* \*\*\(1\+b\)==11: Success$
+^\[main.assertion.18\] .* \*\*\(1\+b\)==13: Failure \(if reachable\)$
 ^\[main.assertion.19\] .* \*1\[b\]==11: Success$
 ^\[main.assertion.20\] .* \*1\[b\]==13: Failure \(if reachable\)$
 ^\[main.assertion.21\] .* c\[0\]==&c0: Unknown$

regression/goto-analyzer/sensitivity-test-constants-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_array.c
---variable --arrays --verify
+--variable --arrays --verify --pointers
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* a\[1\]==0: Success$
@@ -9,8 +9,8 @@ sensitivity_test_constants_array.c
 ^\[main.assertion.4\] .* b\[1\]==1: Failure \(if reachable\)$
 ^\[main.assertion.5\] .* \*\(b\+1\)==0: Success$
 ^\[main.assertion.6\] .* \*\(b\+1\)==1: Failure \(if reachable\)$
-^\[main.assertion.7\] .* \*\(1\+b\)==0: Unknown$
-^\[main.assertion.8\] .* \*\(1\+b\)==1: Unknown$
+^\[main.assertion.7\] .* \*\(1\+b\)==0: Success$
+^\[main.assertion.8\] .* \*\(1\+b\)==1: Failure \(if reachable\)$
 ^\[main.assertion.9\] .* 1\[b\]==0: Success$
 ^\[main.assertion.10\] .* 1\[b\]==1: Failure \(if reachable\)$
 ^\[main.assertion.11\] .* c\[0\]==0: Success$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/test.desc

@@ -5,18 +5,18 @@ sensitivity_test_constants_pointer_to_constants_array.c
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* p==&a\[0\]: Success$
 ^\[main.assertion.2\] .* \*p==1: Success$
-^\[main\.assertion\.3\] .* p\[1\]==2: Unknown$
-^\[main\.assertion\.4\] .* 1\[p\]==2: Unknown$
-^\[main\.assertion\.5\] .* \*\(p\+1\)==2: Unknown$
-^\[main\.assertion\.6\] .* \*\(1\+p\)==2: Unknown$
-^\[main\.assertion\.7\] .* \*\(p-1\)==1: Unknown$
-^\[main\.assertion\.8\] .* q==p\+1: Unknown$
-^\[main\.assertion\.9\] .* \*q==2: Unknown$
+^\[main\.assertion\.3\] .* p\[1\]==2: Success$
+^\[main\.assertion\.4\] .* 1\[p\]==2: Success$
+^\[main\.assertion\.5\] .* \*\(p\+1\)==2: Success$
+^\[main\.assertion\.6\] .* \*\(1\+p\)==2: Success$
+^\[main\.assertion\.7\] .* q==p\+1: Success$
+^\[main\.assertion\.8\] .* \*q==2: Success$
+^\[main\.assertion\.9\] .* \*\(q-1\)==1: Success$
 ^\[main\.assertion\.10\] .* q-p==x: Unknown$
-^\[main\.assertion\.11\] .* a\[1\]==4: Unknown$
-^\[main\.assertion\.12\] .* a\[1\]==5: Unknown$
-^\[main\.assertion\.13\] .* a\[1\]==6: Unknown$
-^\[main\.assertion\.14\] .* a\[1\]==7: Unknown$
+^\[main\.assertion\.11\] .* a\[1\]==4: Success$
+^\[main\.assertion\.12\] .* a\[1\]==5: Success$
+^\[main\.assertion\.13\] .* a\[1\]==6: Success$
+^\[main\.assertion\.14\] .* a\[1\]==7: Success$
 ^\[main\.assertion\.15\] .* \*r==2: Unknown$
 ^\[main\.assertion\.16\] .* \*r==1: Unknown$
 ^\[main\.assertion\.17\] .* \*s==0: Unknown$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc

@@ -1,16 +1,30 @@
-KNOWNBUG
+CORE
 sensitivity_test_constants_pointer_to_constants_struct.c
 --variable --pointers --structs --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] .* \(\*p\).a==0: Success$
-^\[main.assertion.2\] .* \(\*p\).a==1: Failure \(if reachable\)$
-^\[main.assertion.3\] .* p->a==0: Success$
-^\[main.assertion.4\] .* p->a==1: Failure \(if reachable\)$
-^\[main.assertion.5\] .* p->b==2.0: Success$
-^\[main.assertion.6\] .* p->b==1.0: Failure \(if reachable\)$
+^\[main\.assertion\.1\] .* \(\*p\).a==0: Success$
+^\[main\.assertion\.2\] .* \(\*p\).a==1: Failure \(if reachable\)$
+^\[main\.assertion\.3\] .* p->a==0: Success$
+^\[main\.assertion\.4\] .* p->a==1: Failure \(if reachable\)$
+^\[main\.assertion\.5\] .* p->b==2.0: Success$
+^\[main\.assertion\.6\] .* p->b==1.0: Failure \(if reachable\)$
+^\[main\.assertion\.9\] .* \*comp_p==0: Success$
+^\[main\.assertion\.10\] .* \*comp_p==1: Failure \(if reachable\)$
+^\[main\.assertion\.13\] .* \*compb_p==2.0: Success$
+^\[main\.assertion\.14\] .* \*compb_p==1.0: Failure \(if reachable\)$
+^\[main\.assertion\.17\] .* \*implicit_p==0: Unknown$
+^\[main\.assertion\.18\] .* \*implicit_p==1: Unknown$
+^\[main\.assertion\.19\] .* x.a==5: Unknown$
+^\[main\.assertion\.20\] .* x.a==1: Unknown$
 --
 ^warning: ignoring
 --
-The final two assertions are the wrong way round as modifying the pointer
-does not seem to be propogating through. See #96
+The following assertions are not checked since simplify_expr doesn't handle
+them. See issue diffblue/cbmc-toyota#145
+^\[main\.assertion\.7\] .* comp_p==&x.a: Success
+^\[main\.assertion\.8\] .* comp_p==&x.b: Failure \(if reachable\)$
+^\[main\.assertion\.11\] .* compb_p==&x.a: Failure \(if reachable\)$
+^\[main\.assertion\.12\] .* compb_p==&x.b: Success
+^\[main\.assertion\.15\] .* implicit_p==&x.a: Success
+^\[main\.assertion\.16\] .* implicit_p==&x: Success

regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/test.desc

@@ -9,9 +9,9 @@ sensitivity_test_constants_pointer_to_two_value_array.c
 ^\[main\.assertion\.4\] .* 1\[p\]==2: Unknown$
 ^\[main\.assertion\.5\] .* \*\(p\+1\)==2: Unknown$
 ^\[main\.assertion\.6\] .* \*\(1\+p\)==2: Unknown$
-^\[main\.assertion\.7\] .* \*\(p-1\)==1: Unknown$
-^\[main.assertion.8\] .* q==p\+1: Unknown$
-^\[main.assertion.9\] .* \*q==2: Unknown$
+^\[main.assertion\.7\] .* q==p\+1: Success$
+^\[main.assertion\.8\] .* \*q==2: Unknown$
+^\[main\.assertion\.9\] .* \*\(q-1\)==1: Unknown$
 ^\[main.assertion.10\] .* q-p==x: Unknown$
 ^\[main.assertion.11\] .* a\[1\]==4: Unknown$
 ^\[main.assertion.12\] .* a\[1\]==5: Unknown$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/test.desc

@@ -9,5 +9,19 @@ sensitivity_test_constants_pointer_to_two_value_struct.c
 ^\[main.assertion.4\] .* p->a==1: Unknown$
 ^\[main.assertion.5\] .* p->b==2.0: Unknown$
 ^\[main.assertion.6\] .* p->b==1.0: Unknown$
+\[main\.assertion\.7\] .* comp_p==&x\.a: Unknown$
+\[main\.assertion\.8\] .* comp_p==&x\.b: Unknown$
+\[main\.assertion\.9\] .* \*comp_p==0: Unknown$
+\[main\.assertion\.10\] .* \*comp_p==1: Unknown$
+\[main\.assertion\.11\] .* compb_p==&x\.a: Unknown$
+\[main\.assertion\.12\] .* compb_p==&x\.b: Unknown$
+\[main\.assertion\.13\] .* \*compb_p==2\.0: Unknown$
+\[main\.assertion\.14\] .* \*compb_p==1\.0: Unknown$
+\[main\.assertion\.15\] .* implicit_p==&x\.a: Unknown$
+\[main\.assertion\.16\] .* implicit_p==&x: Unknown$
+\[main\.assertion\.17\] .* \*implicit_p==0: Unknown$
+\[main\.assertion\.18\] .* \*implicit_p==1: Unknown$
+\[main\.assertion\.19\] .* x\.a==5: Unknown$
+\[main\.assertion\.20\] .* x\.a==1: Unknown$
 --
 ^warning: ignoring

regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-array/test.desc

@@ -9,9 +9,9 @@ sensitivity_test_two_value_pointer_to_two_value_array.c
 ^\[main\.assertion\.4\] .* 1\[p\]==2: Unknown$
 ^\[main\.assertion\.5\] .* \*\(p\+1\)==2: Unknown$
 ^\[main\.assertion\.6\] .* \*\(1\+p\)==2: Unknown$
-^\[main\.assertion\.7\] .* \*\(p-1\)==1: Unknown$
-^\[main\.assertion\.8\] .* q==p\+1: Unknown$
-^\[main\.assertion\.9\] .* \*q==2: Unknown$
+^\[main\.assertion\.7\] .* q==p\+1: Unknown$
+^\[main\.assertion\.8\] .* \*q==2: Unknown$
+^\[main\.assertion\.9\] .* \*\(q-1\)==1: Unknown$
 ^\[main\.assertion\.10\] .* q-p==x: Unknown$
 ^\[main\.assertion\.11\] .* a\[1\]==4: Unknown$
 ^\[main\.assertion\.12\] .* a\[1\]==5: Unknown$