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



OK. Goals named after ? Qed_nnn ? are auto-checks generated by WP on-the-fly for asserting the soundness of Qed simplifications.
This was a very experimental feature that shall not survive to the next release of Frama-C ;-)
Sorry for my misunderstanding.
	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