SE547: CBMC: Using CBMC [5/19] Previous pageContentsNext page

Download CBMC from http://www-2.cs.cmu.edu/~modelcheck/cbmc/. You may also need file:ansi-c-lib.zip 

  cbmc --decide --unwind 5 --no-unwinding-assertions --function mkstring mkstring-buggy.c

What those options mean:

  cbmc --decide run the model checker
       --unwind 5 expand the for-loop 5 times
       --no-unwinding-assertions don't issue warnings about --unwind
       --function mkstring which function to check
       mkstring-buggy.c filename

What edits do we need to make to get this program to pass the test?

Previous pageContentsNext page