Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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