--- layout: fc_discuss_archives title: Message 96 from Frama-C-discuss on December 2009 ---
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