--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on January 2020 ---
Splendid, thank you! > On Jan 27, 2020, at 12:15 AM, Loïc Correnson <loic.correnson at cea.fr> wrote: > > Absolutely no impact on external provers. > You can use (ghost) lemma functions instead. > L. > > > >>> Le 24 janv. 2020 à 22:08, Alexander Bakst <abakst at galois.com> a écrit : >>> >>> 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> 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 >>> >>> _______________________________________________ >>> Frama-c-discuss mailing list >>> 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 > > _______________________________________________ > 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/20200127/06d6aa9c/attachment.html>