search

marek-trtik / cbmc

C Bounded Model Checker
http://www.cprover.org/cbmc
Other
0 stars 0 forks source link

Fixing: too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8); #25

Closed lucasccordeiro closed 6 years ago

lucasccordeiro commented 6 years ago

We have a number of benchmarks that are failing with this issue:

too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8); use the `--object-bits n` option to increase the maximum number

We should use the --object-bits n option to increase the maximum number.

Here is one example:

./cbmc --graphml-witness witness.graphml --32 --propertyfile ../../sv-benchmarks/c/MemSafety.prp ../../sv-benchmarks/c/memsafety/test-0219_true-valid-memsafety.i

lucasccordeiro commented 6 years ago

I have increased the number of objects to 2^10=1024. Now it produces timeout in my laptop. I'll make a PR to change our driver script in order to increase the number of objects. Hopefully, we can solve some additional benchmarks.

lucasccordeiro commented 6 years ago

Duplicate of https://github.com/marek-trtik/cbmc/issues/26.