--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on January 2020 ---
Thanks for taking a look. Is there a way I can work around it? Does it affect lemma instantiation in any way when attempting to discharge the obligation by an external prover? Thanks, Alexander > On Jan 23, 2020, at 1:23 AM, Loïc Correnson <loic.correnson at cea.fr> wrote: > > â¦but your are right, there is a bug here! > Thanks for reporting. > >> Le 22 janv. 2020 à 20:40, Alexander Bakst <abakst at galois.com <mailto: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 <mailto:Frama-c-discuss at lists.gforge.inria.fr> >> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > _______________________________________________ > 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/20200124/54c36598/attachment.html>