Re: [creduce-dev] Understanding options to framac in a creduce script

[John Regehr <regehr@cs.utah.edu>]

Faraz, I'd suggest just using tis-interpreter instead of Frama-C:

http://trust-in-soft.com/tis-interpreter/

But to answer your questions, you are running the value analysis plugin 
along with options that favor (relatively) fast concrete interpretation, 
as opposed to abstract interpretation.

> *[-stop-at-first-alarm]*

Don't continue after finding an error.

> *[-no-val-show-progress]*

Don't waste time printing intermediate statuses.

> *[-obviously-terminates]*
> *[-precise-unions]*

I forgot.

John