--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on January 2020 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200122/591e3a20/attachment.html>