Add tests for symex evaluating simple pointer comparisons

At time of writing, develop fails on the following lines of the test:

Failed test.desc lines:
test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$ [FAILED]
test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$ [FAILED]
test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$ [FAILED]
test::1::unreachable_6[^\s]+ = 7$ [FAILED]
test::1::unreachable_14[^\s]+ = 7$ [FAILED]

Author: Owen

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

@@ -0,0 +1,76 @@
+#include <assert.h>
+
+static void noop() { }
+
+int test(int nondet_int) {
+  int a = 1, b = 2, c = 3;
+
+  // Symex knows the value of ptr_to_a, so it should be able to evaluate simple
+  // conditions involving it.
+  int *ptr_to_a = &a;
+
+  int unconditionally_reachable_1;
+  if(ptr_to_a == &a)
+    unconditionally_reachable_1 = 7;
+
+  int unreachable_2;
+  if(ptr_to_a == &c)
+    unreachable_2 = 7;
+
+  int unconditionally_reachable_3;
+  if(ptr_to_a != &c)
+    unconditionally_reachable_3 = 7;
+
+  int unreachable_4;
+  if(ptr_to_a != &a)
+    unreachable_4 = 7;
+
+  // Symex can't tell what ptr_to_a_or_b points to, but we can tell that it
+  // doesn't point to some things
+  int *ptr_to_a_or_b = nondet_int == 0 ? &a : &b;
+
+  int possibly_reachable_5;
+  if(ptr_to_a_or_b == &a)
+    possibly_reachable_5 = 7;
+
+  int unreachable_6;
+  if(ptr_to_a_or_b == &c)
+    unreachable_6 = 7;
+
+  int unconditionally_reachable_7;
+  if(ptr_to_a_or_b != &c)
+    unconditionally_reachable_7 = 7;
+
+  int possibly_reachable_8;
+  if(ptr_to_a_or_b != &a)
+    possibly_reachable_8 = 7;
+
+  // We should also be able to do all of the above in compound expressions which
+  // use logical operators like AND, OR and NOT.
+
+  int unconditionally_reachable_9;
+  if(!(ptr_to_a == &c))
+    unconditionally_reachable_9 = 7;
+
+  int unreachable_10;
+  if(!(ptr_to_a == &a))
+    unreachable_10 = 7;
+
+  int unconditionally_reachable_11;
+  if(!(ptr_to_a_or_b == &c))
+    unconditionally_reachable_11 = 7;
+
+  int possibly_reachable_12;
+  if(!(ptr_to_a_or_b == &a))
+    possibly_reachable_12 = 7;
+
+  int unconditionally_reachable_13;
+  if((ptr_to_a == &a && c == 3) || c == 0)
+    unconditionally_reachable_13 = 7;
+
+  int unreachable_14;
+  if((ptr_to_a_or_b == &c && c == 3) || c == 0)
+    unreachable_14 = 7;
+
+  assert(0);
+}

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc

@@ -0,0 +1,30 @@
+CORE
+test.c
+--function test --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+test::1::unconditionally_reachable_1[^\s]+ = 7$
+test::1::unconditionally_reachable_3[^\s]+ = 7$
+test::1::unconditionally_reachable_7[^\s]+ = 7$
+test::1::unconditionally_reachable_9[^\s]+ = 7$
+test::1::unconditionally_reachable_11[^\s]+ = 7$
+test::1::unconditionally_reachable_13[^\s]+ = 7$
+test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_5[^\s]+\)$
+test::1::possibly_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_8[^\s]+\)$
+test::1::possibly_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_12[^\s]+\)$
+--
+test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$
+test::1::unconditionally_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_3[^\s]+\)$
+test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$
+test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$
+test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$
+test::1::unconditionally_reachable_13[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_13[^\s]+\)$
+test::1::unreachable_2[^\s]+ = 7$
+test::1::unreachable_4[^\s]+ = 7$
+test::1::unreachable_6[^\s]+ = 7$
+test::1::unreachable_10[^\s]+ = 7$
+test::1::unreachable_14[^\s]+ = 7$
+^warning: ignoring
+--
+Pointer comparisons will be resolved in symex by a mixture of constant
+propagation and value-set filtering