--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on December 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Queries regarding WP plugin



Hello Lo?c,

Le 15/12/2014 09:40, Lo?c Correnson a ?crit :
> You shall use option '-wp-gen? to generate the proof obligations without sending them to the prover.

But this does not generate anything for simple VCs!

For example:
"""
$ cat f_wp.c

/*@ requires 0 <= x <= 10;
     ensures 1 <= \result <= 11;
*/
int f(int x)
{
   return x + 1;
}
"""

$ frama-c -wp-out out -wp -wp-gen f_wp.c
[kernel] preprocessing with "gcc -C -E -I.  f_wp.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_post : Valid
[wp] Proved goals:    1 / 1
      Qed:             1

$ ls out
ls: cannot access out: No such file or directory
"""

Would you have a command line that works on above program?

Above command line works with more complicated program, like:
"""
*@ requires 0 <= x <= 10;
     ensures 0 <= \result <= 33;
*/
int f_complicated(int x)
{
   return x * 3;
}
"""

> The ? *.ergo ? files only contains the goal part, without the necessary libraries and definitions, which are generated aside.
> The ? *_Alt-Ergo.mlw ? files are self-contained.

I understand that *.ergo files contain only goals. But a goal like "goal 
Qed_19_20: (0 <" seems rather strange to me.

Best regards,
david