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

[Frama-c-discuss] Lemma Selection



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>