Merge pull request #1475 from martin-cs/goto-analyzer-6-part1

Goto analyzer 6 part1

Author: Thomas Kiley

regression/goto-instrument/constant-propagation1/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+void main()
+{
+  unsigned char n;
+  __CPROVER_assume(n > 0);   // To keep division well defined
+  __CPROVER_assume(n * n > 0);   // To keep division well defined
+
+  unsigned char i = 0;
+  unsigned char j = 0;
+
+  unsigned char aux1 = i / (n * n);
+  for (i = 0; i < n; ++i, aux1 = i / (n * n)) {
+    for (j = 0; j < n; ++j) {
+    }
+  }
+  assert(i != n);
+}

regression/goto-instrument/constant-propagation1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constant-propagator --unwind 3
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/Makefile

@@ -22,7 +22,6 @@ SRC = ai.cpp \
       locals.cpp \
       natural_loops.cpp \
       reaching_definitions.cpp \
-      replace_symbol_ext.cpp \
       static_analysis.cpp \
       uncaught_exceptions_analysis.cpp \
       uninitialized_domain.cpp \