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] ACSL, globals and ghosts

  • Subject: [Frama-c-discuss] ACSL, globals and ghosts
  • From: Pierre-Loic.Garoche at onera.fr (Pierre-Loïc Garoche)
  • Date: Fri, 9 Aug 2013 11:39:50 +0200
Hi all,

some questions about the use of ACSL, globals and ghost:

* Global variables

How do global variables interact with contracts? When used in ensures, it seems
that the global variable appear as a typed free variable. No knwoledge at all
about its value, even when it is just a constant. For example, the following
ensures is not proved automatically.

int x = 0;

/*@ requires y >= 0;
  @ ensures \result > x;
  @*/
int f(int y) { return y +1; }

When one looks at the generated VC, one can see that no knowledge about x is
available.

goal WP "expl:Post-condition (file global1.c, line 5) in 'f'":
  forall f_0 x_0 : int.
  (0 < f_0) ->
  ((is_sint32 f_0)) ->
  ((is_sint32 x_0)) ->
  ((is_sint32 (f_0 - 1))) ->
  (x_0 < f_0)


How to deal with it? Encode all the semantics of the global variable (its
value, how to can evolve) in a predicate and give it as a "requires" to the
function? Examples would be welcome.

* Additional ghost field in a struct

The manuel mentions ghost fields: If a structure has ghost fields, the sizeof of
the structure is the same has the structure without ghost fields. Also,
alignment of fields remains unchanged

However, it doesn't seems accepted by the Fluorine (June release) and it is not
colored in red in the ACSL implementation document.

struct myStruct { int x; ghost int y; };

State 484: read token SEMICOLON(_)
State 484: reduce by rule 323
State 470: reduce by rule 268
State 337: reduce by rule 260
State 338: reduce by rule 258
State 339: shift to state 502
State 502: read token IDENT(ghost)
ghost2.c:1:[kernel] user error: syntax error



Thx

pl
-- 
Pierre-Lo?c Garoche
Research Scientist @ ONERA
pierre-loic.garoche at onera.fr - pierre-loic-garoche at uiowa.edu
http://www.onera.fr/staff/pierre-loic-garoche/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: Digital signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130809/9a21982a/attachment.pgp>