diffblue · kroening · Jan 20, 2017 · Jan 18, 2017 · Jan 18, 2017
diff --git a/regression/Makefile b/regression/Makefile
@@ -1,5 +1,5 @@
 
-DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind goto-analyzer inlining
+DIRS = ansi-c cbmc cpp goto-instrument goto-analyzer
 
 test:
 	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)
diff --git a/regression/goto-instrument-unwind/Makefile b/regression/goto-instrument-unwind/Makefile
diff --git a/regression/goto-instrument-unwind/unwind-chain.sh b/regression/goto-instrument-unwind/unwind-chain.sh
diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
@@ -1,14 +1,27 @@
 #!/bin/bash
 
+set -e
+
 src=../../../src
 goto_cc=$src/goto-cc/goto-cc
 goto_instrument=$src/goto-instrument/goto-instrument
+cbmc=$src/cbmc/cbmc
 
 name=${@:$#}
 name=${name%.c}
 
 args=${@:1:$#-1}
 
 $goto_cc -o $name.gb $name.c
-$goto_instrument $args $name.gb
+# $goto_instrument --show-goto-functions $name.gb
+$goto_instrument $args $name.gb ${name}-mod.gb
+if [ ! -e ${name}-mod.gb ] ; then
+  cp $name.gb ${name}-mod.gb
+elif echo "$args" | grep -q -- "--dump-c" ; then
+  mv ${name}-mod.gb ${name}-mod.c
+  $goto_cc ${name}-mod.c -o ${name}-mod.gb
+  rm ${name}-mod.c
+fi
+$goto_instrument --show-goto-functions ${name}-mod.gb
+$cbmc ${name}-mod.gb
 
diff --git a/regression/goto-instrument/const-struct1/test.desc b/regression/goto-instrument/const-struct1/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-"--show-symbol-table"
+--show-symbol-table
 ^Type\.*: struct struct_tag_name$
 ^Type\.*: const double$
 ^EXIT=0$

diff --git a/regression/goto-instrument/data-flow1/test.desc b/regression/goto-instrument/data-flow1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-"--show-dependence-graph"
+--show-dependence-graph
 ^EXIT=0$
 ^SIGNAL=0$
 Data dependencies: *[0-9]\+,[0-9]\+,[0-9]\+

diff --git a/regression/inlining/inline_01/main.c → regression/goto-instrument/inline_01/main.c b/regression/inlining/inline_01/main.c → regression/goto-instrument/inline_01/main.c
diff --git a/regression/inlining/inline_01/test.desc → ...ssion/goto-instrument/inline_01/test.desc b/regression/inlining/inline_01/test.desc → ...ssion/goto-instrument/inline_01/test.desc
diff --git a/regression/inlining/inline_02/main.c → regression/goto-instrument/inline_02/main.c b/regression/inlining/inline_02/main.c → regression/goto-instrument/inline_02/main.c
diff --git a/regression/inlining/inline_02/test.desc → ...ssion/goto-instrument/inline_02/test.desc b/regression/inlining/inline_02/test.desc → ...ssion/goto-instrument/inline_02/test.desc
diff --git a/regression/inlining/inline_03/main.c → regression/goto-instrument/inline_03/main.c b/regression/inlining/inline_03/main.c → regression/goto-instrument/inline_03/main.c
diff --git a/regression/inlining/inline_03/test.desc → ...ssion/goto-instrument/inline_03/test.desc b/regression/inlining/inline_03/test.desc → ...ssion/goto-instrument/inline_03/test.desc
diff --git a/regression/inlining/inline_04/main.c → regression/goto-instrument/inline_04/main.c b/regression/inlining/inline_04/main.c → regression/goto-instrument/inline_04/main.c
diff --git a/regression/inlining/inline_04/test.desc → ...ssion/goto-instrument/inline_04/test.desc b/regression/inlining/inline_04/test.desc → ...ssion/goto-instrument/inline_04/test.desc
diff --git a/regression/inlining/inline_05/main.c → regression/goto-instrument/inline_05/main.c b/regression/inlining/inline_05/main.c → regression/goto-instrument/inline_05/main.c
diff --git a/regression/inlining/inline_05/test.desc → ...ssion/goto-instrument/inline_05/test.desc b/regression/inlining/inline_05/test.desc → ...ssion/goto-instrument/inline_05/test.desc
diff --git a/regression/inlining/inline_06/main.c → regression/goto-instrument/inline_06/main.c b/regression/inlining/inline_06/main.c → regression/goto-instrument/inline_06/main.c
diff --git a/regression/inlining/inline_06/test.desc → ...ssion/goto-instrument/inline_06/test.desc b/regression/inlining/inline_06/test.desc → ...ssion/goto-instrument/inline_06/test.desc
diff --git a/regression/inlining/inline_07/main.c → regression/goto-instrument/inline_07/main.c b/regression/inlining/inline_07/main.c → regression/goto-instrument/inline_07/main.c
diff --git a/regression/inlining/inline_07/test.desc → ...ssion/goto-instrument/inline_07/test.desc b/regression/inlining/inline_07/test.desc → ...ssion/goto-instrument/inline_07/test.desc
diff --git a/regression/inlining/inline_08/main.c → regression/goto-instrument/inline_08/main.c b/regression/inlining/inline_08/main.c → regression/goto-instrument/inline_08/main.c
diff --git a/regression/inlining/inline_08/test.desc → ...ssion/goto-instrument/inline_08/test.desc b/regression/inlining/inline_08/test.desc → ...ssion/goto-instrument/inline_08/test.desc
diff --git a/regression/inlining/inline_09/main.c → regression/goto-instrument/inline_09/main.c b/regression/inlining/inline_09/main.c → regression/goto-instrument/inline_09/main.c
diff --git a/regression/inlining/inline_09/test.desc → ...ssion/goto-instrument/inline_09/test.desc b/regression/inlining/inline_09/test.desc → ...ssion/goto-instrument/inline_09/test.desc
diff --git a/regression/inlining/inline_10/main.c → regression/goto-instrument/inline_10/main.c b/regression/inlining/inline_10/main.c → regression/goto-instrument/inline_10/main.c
diff --git a/regression/inlining/inline_10/test.desc → ...ssion/goto-instrument/inline_10/test.desc b/regression/inlining/inline_10/test.desc → ...ssion/goto-instrument/inline_10/test.desc
diff --git a/regression/inlining/inline_11/main.c → regression/goto-instrument/inline_11/main.c b/regression/inlining/inline_11/main.c → regression/goto-instrument/inline_11/main.c
diff --git a/regression/inlining/inline_11/test.desc → ...ssion/goto-instrument/inline_11/test.desc b/regression/inlining/inline_11/test.desc → ...ssion/goto-instrument/inline_11/test.desc
diff --git a/regression/inlining/inline_12/main.c → regression/goto-instrument/inline_12/main.c b/regression/inlining/inline_12/main.c → regression/goto-instrument/inline_12/main.c
diff --git a/regression/inlining/inline_12/test.desc → ...ssion/goto-instrument/inline_12/test.desc b/regression/inlining/inline_12/test.desc → ...ssion/goto-instrument/inline_12/test.desc
diff --git a/regression/goto-instrument/slice-global-inits1/main.c b/regression/goto-instrument/slice-global-inits1/main.c
@@ -24,9 +24,10 @@ void func2()
   s2.a = 7;
 }
 
-void func3()
+void func3(int a)
 {
-  func3();
+  if(a>0)
+    func3(a-1);
 }
 
 int main()
@@ -36,7 +37,7 @@ int main()
 
   func2();
 
-  func3();
+  func3(1);
 
   return 0;
 }
diff --git a/regression/goto-instrument/slice-global-inits1/test.desc b/regression/goto-instrument/slice-global-inits1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---slice-global-inits --show-goto-functions
+--slice-global-inits
 z = 0;$
 a =
 s2 =

diff --git a/...ion/goto-instrument-unwind/assert1/main.c → ...ion/goto-instrument/unwind-assert1/main.c b/...ion/goto-instrument-unwind/assert1/main.c → ...ion/goto-instrument/unwind-assert1/main.c
diff --git a/.../goto-instrument-unwind/assert1/test.desc → .../goto-instrument/unwind-assert1/test.desc b/.../goto-instrument-unwind/assert1/test.desc → .../goto-instrument/unwind-assert1/test.desc
diff --git a/...ion/goto-instrument-unwind/assert2/main.c → ...ion/goto-instrument/unwind-assert2/main.c b/...ion/goto-instrument-unwind/assert2/main.c → ...ion/goto-instrument/unwind-assert2/main.c
diff --git a/.../goto-instrument-unwind/assert2/test.desc → .../goto-instrument/unwind-assert2/test.desc b/.../goto-instrument-unwind/assert2/test.desc → .../goto-instrument/unwind-assert2/test.desc
diff --git a/...ion/goto-instrument-unwind/assert3/main.c → ...ion/goto-instrument/unwind-assert3/main.c b/...ion/goto-instrument-unwind/assert3/main.c → ...ion/goto-instrument/unwind-assert3/main.c
diff --git a/.../goto-instrument-unwind/assert3/test.desc → .../goto-instrument/unwind-assert3/test.desc b/.../goto-instrument-unwind/assert3/test.desc → .../goto-instrument/unwind-assert3/test.desc
diff --git a/...ion/goto-instrument-unwind/assume1/main.c → ...ion/goto-instrument/unwind-assume1/main.c b/...ion/goto-instrument-unwind/assume1/main.c → ...ion/goto-instrument/unwind-assume1/main.c
diff --git a/.../goto-instrument-unwind/assume1/test.desc → .../goto-instrument/unwind-assume1/test.desc b/.../goto-instrument-unwind/assume1/test.desc → .../goto-instrument/unwind-assume1/test.desc
diff --git a/...ion/goto-instrument-unwind/assume2/main.c → ...ion/goto-instrument/unwind-assume2/main.c b/...ion/goto-instrument-unwind/assume2/main.c → ...ion/goto-instrument/unwind-assume2/main.c
diff --git a/.../goto-instrument-unwind/assume2/test.desc → .../goto-instrument/unwind-assume2/test.desc b/.../goto-instrument-unwind/assume2/test.desc → .../goto-instrument/unwind-assume2/test.desc
diff --git a/...goto-instrument-unwind/break-loop1/main.c → ...goto-instrument/unwind-break-loop1/main.c b/...goto-instrument-unwind/break-loop1/main.c → ...goto-instrument/unwind-break-loop1/main.c
diff --git a/...o-instrument-unwind/break-loop1/test.desc → ...o-instrument/unwind-break-loop1/test.desc b/...o-instrument-unwind/break-loop1/test.desc → ...o-instrument/unwind-break-loop1/test.desc
diff --git a/...goto-instrument-unwind/break-loop2/main.c → ...goto-instrument/unwind-break-loop2/main.c b/...goto-instrument-unwind/break-loop2/main.c → ...goto-instrument/unwind-break-loop2/main.c
diff --git a/...o-instrument-unwind/break-loop2/test.desc → ...o-instrument/unwind-break-loop2/test.desc b/...o-instrument-unwind/break-loop2/test.desc → ...o-instrument/unwind-break-loop2/test.desc
diff --git a/...strument-unwind/continue-as-loops1/main.c → ...strument/unwind-continue-as-loops1/main.c b/...strument-unwind/continue-as-loops1/main.c → ...strument/unwind-continue-as-loops1/main.c
diff --git a/...ument-unwind/continue-as-loops1/test.desc → ...ument/unwind-continue-as-loops1/test.desc b/...ument-unwind/continue-as-loops1/test.desc → ...ument/unwind-continue-as-loops1/test.desc
diff --git a/...o-instrument-unwind/continue-loop1/main.c → ...o-instrument/unwind-continue-loop1/main.c b/...o-instrument-unwind/continue-loop1/main.c → ...o-instrument/unwind-continue-loop1/main.c
diff --git a/...nstrument-unwind/continue-loop1/test.desc → ...nstrument/unwind-continue-loop1/test.desc b/...nstrument-unwind/continue-loop1/test.desc → ...nstrument/unwind-continue-loop1/test.desc
diff --git a/...o-instrument-unwind/continue-loop2/main.c → ...o-instrument/unwind-continue-loop2/main.c b/...o-instrument-unwind/continue-loop2/main.c → ...o-instrument/unwind-continue-loop2/main.c
diff --git a/...nstrument-unwind/continue-loop2/test.desc → ...nstrument/unwind-continue-loop2/test.desc b/...nstrument-unwind/continue-loop2/test.desc → ...nstrument/unwind-continue-loop2/test.desc
diff --git a/...o-instrument-unwind/do-while-loop1/main.c → ...o-instrument/unwind-do-while-loop1/main.c b/...o-instrument-unwind/do-while-loop1/main.c → ...o-instrument/unwind-do-while-loop1/main.c
diff --git a/...nstrument-unwind/do-while-loop1/test.desc → ...nstrument/unwind-do-while-loop1/test.desc b/...nstrument-unwind/do-while-loop1/test.desc → ...nstrument/unwind-do-while-loop1/test.desc
diff --git a/...o-instrument-unwind/do-while-loop2/main.c → ...o-instrument/unwind-do-while-loop2/main.c b/...o-instrument-unwind/do-while-loop2/main.c → ...o-instrument/unwind-do-while-loop2/main.c
diff --git a/...nstrument-unwind/do-while-loop2/test.desc → ...nstrument/unwind-do-while-loop2/test.desc b/...nstrument-unwind/do-while-loop2/test.desc → ...nstrument/unwind-do-while-loop2/test.desc
diff --git a/...goto-instrument-unwind/empty-loop1/main.c → ...goto-instrument/unwind-empty-loop1/main.c b/...goto-instrument-unwind/empty-loop1/main.c → ...goto-instrument/unwind-empty-loop1/main.c
diff --git a/...o-instrument-unwind/empty-loop1/test.desc → ...o-instrument/unwind-empty-loop1/test.desc b/...o-instrument-unwind/empty-loop1/test.desc → ...o-instrument/unwind-empty-loop1/test.desc
diff --git a/...goto-instrument-unwind/empty-loop2/main.c → ...goto-instrument/unwind-empty-loop2/main.c b/...goto-instrument-unwind/empty-loop2/main.c → ...goto-instrument/unwind-empty-loop2/main.c
diff --git a/...o-instrument-unwind/empty-loop2/test.desc → ...o-instrument/unwind-empty-loop2/test.desc b/...o-instrument-unwind/empty-loop2/test.desc → ...o-instrument/unwind-empty-loop2/test.desc
diff --git a/...to-instrument-unwind/nested-loops1/main.c → ...to-instrument/unwind-nested-loops1/main.c b/...to-instrument-unwind/nested-loops1/main.c → ...to-instrument/unwind-nested-loops1/main.c
diff --git a/...instrument-unwind/nested-loops1/test.desc → ...instrument/unwind-nested-loops1/test.desc b/...instrument-unwind/nested-loops1/test.desc → ...instrument/unwind-nested-loops1/test.desc
diff --git a/...to-instrument-unwind/nested-loops2/main.c → ...to-instrument/unwind-nested-loops2/main.c b/...to-instrument-unwind/nested-loops2/main.c → ...to-instrument/unwind-nested-loops2/main.c
diff --git a/...instrument-unwind/nested-loops2/test.desc → ...instrument/unwind-nested-loops2/test.desc b/...instrument-unwind/nested-loops2/test.desc → ...instrument/unwind-nested-loops2/test.desc
diff --git a/...oto-instrument-unwind/simple-loop1/main.c → ...oto-instrument/unwind-simple-loop1/main.c b/...oto-instrument-unwind/simple-loop1/main.c → ...oto-instrument/unwind-simple-loop1/main.c
diff --git a/...-instrument-unwind/simple-loop1/test.desc → ...-instrument/unwind-simple-loop1/test.desc b/...-instrument-unwind/simple-loop1/test.desc → ...-instrument/unwind-simple-loop1/test.desc
diff --git a/...oto-instrument-unwind/simple-loop2/main.c → ...oto-instrument/unwind-simple-loop2/main.c b/...oto-instrument-unwind/simple-loop2/main.c → ...oto-instrument/unwind-simple-loop2/main.c
diff --git a/...-instrument-unwind/simple-loop2/test.desc → ...-instrument/unwind-simple-loop2/test.desc b/...-instrument-unwind/simple-loop2/test.desc → ...-instrument/unwind-simple-loop2/test.desc
diff --git a/...goto-instrument-unwind/unwind-log1/main.c → ...goto-instrument/unwind-unwind-log1/main.c b/...goto-instrument-unwind/unwind-log1/main.c → ...goto-instrument/unwind-unwind-log1/main.c
diff --git a/...o-instrument-unwind/unwind-log1/test.desc → ...o-instrument/unwind-unwind-log1/test.desc b/...o-instrument-unwind/unwind-log1/test.desc → ...o-instrument/unwind-unwind-log1/test.desc
diff --git a/...-instrument-unwind/unwindset-file1/main.c → ...-instrument/unwind-unwindset-file1/main.c b/...-instrument-unwind/unwindset-file1/main.c → ...-instrument/unwind-unwindset-file1/main.c
diff --git a/...strument-unwind/unwindset-file1/test.desc → ...strument/unwind-unwindset-file1/test.desc b/...strument-unwind/unwindset-file1/test.desc → ...strument/unwind-unwindset-file1/test.desc
diff --git a/...nt-unwind/unwindset-file1/unwindset.input → ...nt/unwind-unwindset-file1/unwindset.input b/...nt-unwind/unwindset-file1/unwindset.input → ...nt/unwind-unwindset-file1/unwindset.input
diff --git a/.../goto-instrument-unwind/unwindset1/main.c → .../goto-instrument/unwind-unwindset1/main.c b/.../goto-instrument-unwind/unwindset1/main.c → .../goto-instrument/unwind-unwindset1/main.c
diff --git a/...to-instrument-unwind/unwindset1/test.desc → ...to-instrument/unwind-unwindset1/test.desc b/...to-instrument-unwind/unwindset1/test.desc → ...to-instrument/unwind-unwindset1/test.desc
diff --git a/.../goto-instrument-unwind/unwindset2/main.c → .../goto-instrument/unwind-unwindset2/main.c b/.../goto-instrument-unwind/unwindset2/main.c → .../goto-instrument/unwind-unwindset2/main.c
diff --git a/...to-instrument-unwind/unwindset2/test.desc → ...to-instrument/unwind-unwindset2/test.desc b/...to-instrument-unwind/unwindset2/test.desc → ...to-instrument/unwind-unwindset2/test.desc
diff --git a/.../goto-instrument-unwind/unwindset3/main.c → .../goto-instrument/unwind-unwindset3/main.c b/.../goto-instrument-unwind/unwindset3/main.c → .../goto-instrument/unwind-unwindset3/main.c
diff --git a/...to-instrument-unwind/unwindset3/test.desc → ...to-instrument/unwind-unwindset3/test.desc b/...to-instrument-unwind/unwindset3/test.desc → ...to-instrument/unwind-unwindset3/test.desc
diff --git a/.../goto-instrument-unwind/unwindset4/main.c → .../goto-instrument/unwind-unwindset4/main.c b/.../goto-instrument-unwind/unwindset4/main.c → .../goto-instrument/unwind-unwindset4/main.c
diff --git a/...to-instrument-unwind/unwindset4/test.desc → ...to-instrument/unwind-unwindset4/test.desc b/...to-instrument-unwind/unwindset4/test.desc → ...to-instrument/unwind-unwindset4/test.desc
diff --git a/.../goto-instrument-unwind/unwindset5/main.c → .../goto-instrument/unwind-unwindset5/main.c b/.../goto-instrument-unwind/unwindset5/main.c → .../goto-instrument/unwind-unwindset5/main.c
diff --git a/...to-instrument-unwind/unwindset5/test.desc → ...to-instrument/unwind-unwindset5/test.desc b/...to-instrument-unwind/unwindset5/test.desc → ...to-instrument/unwind-unwindset5/test.desc
diff --git a/...oto-instrument-unwind/zero-unwind1/main.c → ...oto-instrument/unwind-zero-unwind1/main.c b/...oto-instrument-unwind/zero-unwind1/main.c → ...oto-instrument/unwind-zero-unwind1/main.c
diff --git a/...-instrument-unwind/zero-unwind1/test.desc → ...-instrument/unwind-zero-unwind1/test.desc b/...-instrument-unwind/zero-unwind1/test.desc → ...-instrument/unwind-zero-unwind1/test.desc
diff --git a/...oto-instrument-unwind/zero-unwind2/main.c → ...oto-instrument/unwind-zero-unwind2/main.c b/...oto-instrument-unwind/zero-unwind2/main.c → ...oto-instrument/unwind-zero-unwind2/main.c
diff --git a/...-instrument-unwind/zero-unwind2/test.desc → ...-instrument/unwind-zero-unwind2/test.desc b/...-instrument-unwind/zero-unwind2/test.desc → ...-instrument/unwind-zero-unwind2/test.desc
diff --git a/regression/inlining/Makefile b/regression/inlining/Makefile
diff --git a/regression/inlining/chain.sh b/regression/inlining/chain.sh
diff --git a/regression/inlining/test.sh b/regression/inlining/test.sh