--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2020 ---
â¦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>