Run CBMC after goto-instrument's transformations

Author: tautschnig

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
 

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

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 =