diff --git a/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile b/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile index a436623d..2dcf1eb9 100755 --- 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 index f92eee4f..6ce468c2 100755 --- 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)