Replace reach_error (or equivalent) with assert(0)

2ls.inc

@@ -11,6 +11,11 @@ run()
   gmon_suffix=$GMON_OUT_PREFIX
   export GMON_OUT_PREFIX="goto-cc_$gmon_suffix"
   ./goto-cc -m$BIT_WIDTH --function $ENTRY "${BM[@]}" -o $LOG.bin
+  if [ -n "$FAIL_FUNCTION" ]; then
+    ./goto-instrument $LOG.bin $LOG.bin --remove-function-body "$FAIL_FUNCTION" \
+                                        --generate-function-body "$FAIL_FUNCTION" \
+                                        --generate-function-body-options assert-false
+  fi
 
   export GMON_OUT_PREFIX="2ls_$gmon_suffix"
   # add property-specific options

Makefile

@@ -19,7 +19,7 @@ jbmc: jbmc.zip
 	cat $*.inc tool-wrapper.inc >> $@
 	chmod 755 $@
 
-cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc sv-comp-readme.sh
+cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc $(CBMC)/src/goto-instrument/goto-instrument sv-comp-readme.sh
 	mkdir -p $(basename $@)
 	$(MAKE) cbmc-wrapper
 	mv cbmc-wrapper $(basename $@)/cbmc
@@ -30,12 +30,14 @@ cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $
 	strip $(basename $@)/cbmc-binary
 	cp -L $(CBMC)/src/goto-cc/goto-cc $(basename $@)/
 	strip $(basename $@)/goto-cc
+	cp -L $(CBMC)/src/goto-instrument/goto-instrument $(basename $@)/
+	strip $(basename $@)/goto-instrument
 	chmod a+rX $(basename $@)/*
 	zip -r $@ $(basename $@)
-	cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE README
+	cd $(basename $@) && rm cbmc cbmc-binary goto-cc goto-instrument LICENSE README
 	rmdir $(basename $@)
 
-cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc sv-comp-readme.sh
+cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc $(CBMC)/src/goto-instrument/goto-instrument sv-comp-readme.sh
 	mkdir -p $(basename $@)
 	$(MAKE) cbmc-wrapper
 	mv cbmc-wrapper $(basename $@)/cbmc
@@ -45,12 +47,14 @@ cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC
 	strip $(basename $@)/cbmc-binary
 	cp -L $(CBMC)/src/goto-cc/goto-cc $(basename $@)/
 	strip $(basename $@)/goto-cc
+	cp -L $(CBMC)/src/goto-instrument/goto-instrument $(basename $@)/
+	strip $(basename $@)/goto-instrument
 	chmod a+rX $(basename $@)/*
 	zip -r $@ $(basename $@)
-	cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE README
+	cd $(basename $@) && rm cbmc cbmc-binary goto-cc goto-instrument LICENSE README
 	rmdir $(basename $@)
 
-2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/lib/cbmc/src/goto-cc/goto-cc sv-comp-readme.sh
+2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/lib/cbmc/src/goto-cc/goto-cc $(2LS)/lib/cbmc/src/goto-instrument/goto-instrument sv-comp-readme.sh
 	mkdir -p $(basename $@)
 	$(MAKE) 2ls-wrapper
 	mv 2ls-wrapper $(basename $@)/2ls
@@ -60,9 +64,11 @@ cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC
 	strip $(basename $@)/2ls-binary
 	cp -L $(2LS)/lib/cbmc/src/goto-cc/goto-cc $(basename $@)/
 	strip $(basename $@)/goto-cc
+	cp -L $(2LS)/lib/cbmc/src/goto-instrument/goto-instrument $(basename $@)/
+	strip $(basename $@)/goto-instrument
 	chmod a+rX $(basename $@)/*
 	zip -r $@ $(basename $@)
-	cd $(basename $@) && rm 2ls 2ls-binary goto-cc LICENSE README
+	cd $(basename $@) && rm 2ls 2ls-binary goto-cc goto-instrument LICENSE README
 	rmdir $(basename $@)
 
 jbmc.zip: jbmc.inc tool-wrapper.inc $(JBMC)/LICENSE $(JBMC)/jbmc/src/jbmc/jbmc $(JBMC)/jbmc/lib/java-models-library/target/core-models.jar sv-comp-readme.sh

README.cbmc-path.txt

@@ -6,16 +6,20 @@ This archive contains the following files:
 - goto-cc: this C compiler transforms input files into so-called
   `goto-binaries,' which are encoded in CBMC's intermediate representation.
 
+- goto-instrument: performs required preliminary transformations on the
+  'goto-binary'.
+
 - cbmc-binary: this is the actual verification tool. It takes a goto-binary
   as input and checks the properties specified by command-line flags.
 
-- cbmc: this wrapper script invokes cbmc-binary and goto-cc, parsing the
-  property file to pass the correct flags to cbmc-binary and returning the
-  correct return codes for SV-COMP.
+- cbmc: this wrapper script invokes cbmc-binary, goto-cc and goto-instrument,
+  parsing the property file to pass the correct flags to cbmc-binary and
+  returning the correct return codes for SV-COMP.
 
-goto-cc and cbmc-binary were compiled on Debian 9 (stretch); the binaries
-should be self-hosting on similar operating systems.  The upstream URL, if
-you wish to compile it yourself, is https://github.com/diffblue/cbmc
+goto-cc, goto-instrument and cbmc-binary were compiled on Debian 9 (stretch);
+the binaries should be self-hosting on similar operating systems.
+The upstream URL, if you wish to compile it yourself, is
+https://github.com/diffblue/cbmc
 
 To run CBMC Path manually, you need to invoke the tool as
 

cbmc.inc

@@ -15,6 +15,11 @@ run()
   gmon_suffix=$GMON_OUT_PREFIX
   export GMON_OUT_PREFIX="goto-cc_$gmon_suffix"
   ./goto-cc --object-bits $OBJ_BITS -m$BIT_WIDTH --function $ENTRY "${BM[@]}" -o $LOG.bin
+  if [ -n "$FAIL_FUNCTION" ]; then
+    ./goto-instrument $LOG.bin $LOG.bin --remove-function-body "$FAIL_FUNCTION" \
+                                        --generate-function-body "$FAIL_FUNCTION" \
+                                        --generate-function-body-options assert-false
+  fi
 
   export GMON_OUT_PREFIX="cbmc_$gmon_suffix"
 timeout 875 bash -c ' \

sv-comp-readme.sh

@@ -36,13 +36,16 @@ then
 - goto-cc: this C compiler transforms input files into so-called
   "goto-binaries," which are encoded in CBMC's intermediate representation.
 
+- goto-instrument: performs required preliminary transformations on the
+  "goto-binary".
+
 - $TOOL-binary: this is the actual verification tool. It takes a goto-binary or
   source code as input and checks the properties specified by command-line
   flags.
 
-- $TOOL: this wrapper script invokes $TOOL-binary and goto-cc, parsing the
-  property file to pass the correct flags to $TOOL-binary and returning the
-  correct return codes for SV-COMP.
+- $TOOL: this wrapper script invokes $TOOL-binary, goto-cc and goto-instrument,
+  parsing the property file to pass the correct flags to $TOOL-binary and
+  returning the correct return codes for SV-COMP.
 EOF
 else
   cat <<EOF

tool-wrapper.inc

@@ -20,7 +20,10 @@ parse_property_file()
 if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) {
   print "ENTRY=$1\n";
   print "PROP=\"label\"\nLABEL=\"$1\"\n" if($2 =~ /^G!label\((\S+)\)$/);
-  print "PROP=\"unreach_call\"\n" if($2 =~ /^G!call\(reach_error\(\)\)$/);
+  if($2 =~ /^G!call\((?<fn>\S+)\(\)\)$/) {
+    print "PROP=\"unreach_call\"\n";
+    print "FAIL_FUNCTION=\"$+{fn}\"\n";
+  }
   print "PROP=\"unreach_call\"\n" if($2 =~ /^Gassert$/);
   print "PROP=\"memsafety\"\n" if($2 =~ /^Gvalid-(free|deref|memtrack)$/);
   print "PROP=\"memcleanup\"\n" if($2 =~ /^Gvalid-memcleanup$/);