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

[Frama-c-discuss] Lemma Selection



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>