--- layout: fc_discuss_archives title: Message 26 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



Oh, yes sorry, I missed the point.
Indeed, for simple PO discharged by Qed, there is actually no other proof obligation but ? goal PO : true ? !
You can try to deactivate the advanced simplifications of WP with `-wp-no-let` and other options of the same group, but most very low-level simplifications such as ? 1+2 ? into ? 3 ? or ? a+0 = a ? are always applied and can not be deactivated.
Regards,
L.

Le 15 d?c. 2014 ? 09:57, David MENTRE <dmentre at linux-france.org> a ?crit :

> 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
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss