Increase CBMC_OBJECT_BITS for 2 CBMC proofs

angelonakos · paulbartell · commit c0cb120a3dd2 · 2022-09-30T10:24:25.000-07:00
This needs to be done in order for the proofs to pass with CBMC v5.67.0
diff --git a/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile b/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile
@@ -33,6 +33,7 @@ REMOVE_FUNCTION_BODY += _Cellular_CheckLibraryStatus
 # This value was experimentally chosen to provide 100% coverage
 # without tripping unwinding assertions and without exhausting memory.
 CBMC_MAX_BUFSIZE=15
+CBMC_OBJECT_BITS=9
 
 UNWINDSET += __CPROVER_file_local_cellular_common_c__Cellular_FreeContext.0:$(CBMC_MAX_BUFSIZE)
 UNWINDSET += _Cellular_CreateSocketData.0:$(CBMC_MAX_BUFSIZE)
diff --git a/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile b/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile
@@ -33,6 +33,7 @@ REMOVE_FUNCTION_BODY += _Cellular_CheckLibraryStatus
 # This value was experimentally chosen to provide 100% coverage
 # without tripping unwinding assertions and without exhausting memory.
 CBMC_MAX_BUFSIZE=16
+CBMC_OBJECT_BITS=9
 
 UNWINDSET += __CPROVER_file_local_cellular_common_c__Cellular_FreeContext.0:$(CBMC_MAX_BUFSIZE)
 UNWINDSET += _Cellular_CreateSocketData.0:$(CBMC_MAX_BUFSIZE)
