Merge pull request #26 from peterschrammel/obj-bits-fixes

Object bits and other params

Author: peterschrammel

2ls.inc

@@ -13,10 +13,10 @@ run()
     PROPERTY2="$PROPERTY --nontermination --competition-mode"
 
     # run the termination and nontermination analysis in parallel
-    $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits OBJ_BITS $PROPERTY1 \
+    $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY1 \
       --function $ENTRY $BM >> $LOG.ok1 2>&1 &
     PID1="$!"
-    $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits OBJ_BITS $PROPERTY2 \
+    $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY2 \
       --function $ENTRY $BM >> $LOG.ok2 2>&1 &
     PID2="$!"
     # this might not work in all environments
@@ -57,7 +57,7 @@ run()
     PROPERTY="$PROPERTY --heap-interval --k-induction --competition-mode"
 
     # run the tool
-    $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits OBJ_BITS $PROPERTY \
+    $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY \
       --function $ENTRY $BM >> $LOG.ok 2>&1
 
     # store the exit code

cbmc.inc

@@ -8,21 +8,21 @@ TOOL_NAME=CBMC
 run()
 {
   if [ "$PROP" = "termination" ] ; then
-    PROPERTY="$PROPERTY --no-assertions"
+    PROPERTY="$PROPERTY --no-assertions --no-self-loops-to-assumptions"
   fi
 
-timeout 850 bash -c ' \
+timeout 875 bash -c ' \
 \
 ulimit -v 15000000 ; \
 \
 EC=42 ; \
 for c in 2 6 12 17 21 40 200 400 1025 2049 268435456 ; do \
 echo "Unwind: $c" > $LOG.latest ; \
-./cbmc-binary --graphml-witness $LOG.witness --unwind $c --stop-on-fail $BIT_WIDTH --object-bits OBJ_BITS $PROPERTY --function $ENTRY $BM >> $LOG.latest 2>&1 ; \
+./cbmc-binary --graphml-witness $LOG.witness --unwind $c --stop-on-fail $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $BM >> $LOG.latest 2>&1 ; \
 ec=$? ; \
 if [ $ec -eq 0 ] ; then \
 if ! tail -n 10 $LOG.latest | grep -q "^VERIFICATION SUCCESSFUL$" ; then ec=1 ; else \
-./cbmc-binary --unwinding-assertions --unwind $c --stop-on-fail $BIT_WIDTH --object-bits OBJ_BITS $PROPERTY --function $ENTRY $BM > /dev/null 2>&1 || ec=42 ; \
+./cbmc-binary --unwinding-assertions --unwind $c --stop-on-fail $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $BM > /dev/null 2>&1 || ec=42 ; \
 fi ; \
 fi ; \
 if [ $ec -eq 10 ] ; then \

tool-wrapper.inc

@@ -74,7 +74,7 @@ process_graphml()
   fi
 }
 
-OBJ_BITS="10"
+OBJ_BITS="11"
 BIT_WIDTH="--64"
 BM=""
 PROP_FILE=""
@@ -116,6 +116,7 @@ export PROPERTY
 export BIT_WIDTH
 export BM
 export PROP
+export OBJ_BITS
 
 export GMON_OUT_PREFIX=`basename $BM`.gmon.out