--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on June 2011 ---
Dear Frama-Cist, I am currently writing a Frama-C plug-in that will add ACSL annotations to a source C code. In particular, I would like to make use of the \at construct to reference the value of a local variable at a given program point (specified by a ghost label). However, I have difficulties to understand the semantics of this combination. The following example illustrates my problem: void f () { int i = 0; //@ ghost L: i = 1; /*@ assert \at(i, L) == 0; */ } I would have expected the assertion to be true. But running the jessie plug-in leads to a proof obligation that none of the automatic provers on my computer has been able to discharge. Indeed, the produced proof obligation seems impossible to prove: H1: true result: int32 result0: int32 H3: integer_of_int32(result0) = 0 i: int32 H4: i = result0 result1: int32 H5: integer_of_int(result1) = 1 i0: int32 H6: i0 = result1 ------------------------------------------------ integer_of_int32(result) = 0 Would someone be kind enough to explain to me what I am missing? Thank you in advance. frama-c: Carbon-20110201 why: 2.29 Cheers, Nicolas Ayache