--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on January 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Lemma Selection



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>