Increase the number of objects

There are some benchmarks that CBMC fails due to 'too many addressed
objects'. This PR aims to change the maximum number of objects from
256 to 1024 with the goal to solve more benchmarks in SV-COMP 2018.

Author: lucasccordeiro

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

@@ -18,11 +18,11 @@ 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 $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 $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,6 +74,7 @@ process_graphml()
   fi
 }
 
+OBJ_BITS="10"
 BIT_WIDTH="--64"
 BM=""
 PROP_FILE=""