--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Lemma Selection



…but your are right, there is a bug here!
Thanks for reporting.

> Le 22 janv. 2020 à 20:40, Alexander Bakst <abakst at galois.com> a écrit :
> 
> Hi all,
> 
> I have the following (silly, meaningless) program:
> 
> typedef struct foo_s {
>     int x;
>     int y;
> } foo_t;
> 
> /*@ axiomatic funcs {
>   @   logic int func1(foo_t x);
>   @   logic int func2(int x);
>   @   }
>   @   */
> 
> /*@ lemma foo:
>   @   \forall foo_t f1;
>   @   \forall foo_t f2;
>   @   func1(f2) == func1(f1) ==>
>   @   func1(f1) == func2(func1(f2));
>   @*/
> 
> //@assigns pFoo->x, pFoo->y;
> void boo(foo_t *pFoo);
> 
> //@ requires \valid(pFoo);
> void goo(foo_t *pFoo) {
>     //@ ghost foo_t f = *pFoo;
>  PRE:
>     boo(pFoo);
>     //@ ghost foo_t g = *pFoo;
>     //@ assert func1(f) == func2(func1(g));
> }
> 
> When I load this in the frama-c gui and try to prove the assertion, I’m surprised that I can not select the lemma `foo`. How does frama-c/wp decide which lemmas are related to the term?
> 
> Thanks,
> Alexander
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200123/80d45787/attachment-0001.html>