Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Ghost label and \at construct
  • From: nicolas.ayache at gmail.com (Nicolas Ayache)
  • Date: Mon, 20 Jun 2011 14:07:21 +0200
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