[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



Thanks John.  

Also, I found out that the following commands can be used to find information about options:

frama-c -kernel-help
frama-c -value-help


The latter shows the new name for the one I was looking for:  
-val-stop-at-nth-alarm <n> 


Faraz.



On Sun, Nov 27, 2016 at 12:44 PM, John Regehr <regehr@cs.utah.edu> wrote:
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