--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Ghost label and \at construct



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