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

[Faraz Hussain <fh.faraz.hussain@gmail.com>]

Hi,

I am trying to understand how frama-c is invoked in this interesting test script: https://embed.cs.utah.edu/creduce/using/wrong1/test2.sh. I will reproduce the command here:

 frama-c -cpp-command "gcc -C -Dvolatile= -E -I." -val-signed-overflow-alarms -val -stop-at-first-alarm -no-val-show-progress -machdep x86_64 -obviously-terminates -precise-unions small-framac.c >out_framac.txt 2>&1 &&   ! egrep -i '(user error|assert)' out_framac.txt >/dev/null 2>&1

I am consulting this manual frama-c manual (http://frama-c.com/download/user-manual-Aluminium-20160501.pdf).  My question is about the options to the frama-c command.

[.] Which frama-c plugins are required in order to execute this command? (The plugins have their own separate manuals and I think I will have to consult those to find out the exact meaning of these options.)

[.] What are the options in the command above really doing? 

The list below shows what I've been able to find out so far (please correct me if I'm mistaken). The entries in bold are the ones for which I need help.

[-val-signed-overflow-alarm] 

[-val] Runs the value analysis plugin.

[-stop-at-first-alarm]

[-no-val-show-progress]

[-machdep] specifies target machine architecture

[-obviously-terminates]

[-precise-unions]

Thanks!

Regards

Faraz.