--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on January 2020 ---
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 <mailto: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 <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss> >> _______________________________________________ >> 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/20200127/d41feb4d/attachment.html>