Merge pull request #59 from tautschnig/properties-2021

Use reach_error function instead of __VERIFIER_error

Author: tautschnig

cbmc.inc

@@ -14,7 +14,7 @@ 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
+  ./goto-cc --object-bits $OBJ_BITS -m$BIT_WIDTH --function $ENTRY "${BM[@]}" -o $LOG.bin
 
   export GMON_OUT_PREFIX="cbmc_$gmon_suffix"
 timeout 875 bash -c ' \

tool-wrapper.inc

@@ -20,7 +20,7 @@ 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\(__VERIFIER_error\(\)\)$/);
+  print "PROP=\"unreach_call\"\n" if($2 =~ /^G!call\(reach_error\(\)\)$/);
   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$/);