Merge pull request #453 from tautschnig/combine-goto-instrument-regr

Combine goto instrument regression tests

Author: Daniel Kroening

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;)

regression/goto-instrument-unwind/Makefile

@@ -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
 

regression/goto-instrument-unwind/unwind-chain.sh

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-"--show-symbol-table"
+--show-symbol-table
 ^Type\.*: struct struct_tag_name$
 ^Type\.*: const double$
 ^EXIT=0$

regression/goto-instrument/chain.sh

@@ -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]\+

regression/goto-instrument/const-struct1/test.desc

@@ -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;
 }

regression/goto-instrument/data-flow1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---slice-global-inits --show-goto-functions
+--slice-global-inits
 z = 0;$
 a =
 s2 =