--- layout: fc_discuss_archives title: Message 96 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie global variables and functions



Hello,

I have to following simple code

int var1;
int var2;

/*@ assigns var1;
   @ ensures var1 == 1;
*/
void f1(){ var1 = 1 }

/*@ assigns var2;
   @ ensures var1 == 1 ==> var2 == 0;
*/
void f2(){ f1(); if(var1 == 1){ var2 = 0; }‌}


Jessie generates four proof obligations for f2()one of which is not prooved.

H1: true = true
var10: int32
H2: true = true -> integer_of_int32(var10) = 1
H3: integer_of_int32(var10) = 1
result : int32
H4: integer_of_int32(result) = 0
var20 : int32
var20 = result
------------------
var10 = var1


Could someone explain why its trying to prove this as the value of var1
does not change following the execution of f1().

Thank you
Damien