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] static arrays

  • Subject: [Frama-c-discuss] static arrays
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 18 Aug 2015 04:53:15 +0200
  • In-reply-to: <CAL+X0enWOro4KtpXUCBee4=-SG4LNYht8X=VgBad+tjWVsckKQ@mail.gmail.com>
  • References: <CAL+X0enWOro4KtpXUCBee4=-SG4LNYht8X=VgBad+tjWVsckKQ@mail.gmail.com>
On Mon, Aug 17, 2015 at 9:57 PM, Junkil (David) Park <
junkil.park at cis.upenn.edu> wrote:

>  What is the semantics of static arrays in nested curly braces?
>

The front-end moves them outside the block that limits their scope,
renaming them as appropriate to avoid clashes, as you can see for yourself
here:

$ frama-c -print t.c
…
[kernel] preprocessing with "gcc -C -E -I.  t.c"
/* Generated by Frama-C */
void foo(void);

static int const a[2] = {4, 5};
void foo(void)
{
  /*@ assert a[0] ≡ 4; */ ;
  /*@ assert a[1] ≡ 5; */ ;
  return;
}

int main(void);

static int const b[2] = {9, 8};
int main(void)
{
  int __retres;
  /*@ assert b[0] ≡ 9; */ ;
  /*@ assert b[1] ≡ 8; */ ;
  __retres = 0;
  return __retres;
}

So for function foo(), the reason the assertion a[0] == 4 is not proved is
that this property is not the result of local reasoning (after
normalization). Adding a pre-condition to foo() that a[0] == 4 would make
proving the assertion local reasoning, and thus should allow WP to conclude
(untested).

If the caller of foo() is not main() but a function g(), you would need to
make a[0]==4 a pre-condition of g() too.

The function main() is the exception here. WP assumes that global variables
have their initial values at the start of main() without needing to be told
so (page 20 of http://frama-c.com/download/wp-manual-Sodium-20150201.pdf ).

WP does not appear to take advantage of const qualifiers, according to your
results. I will leave you the care of submitting that as a feature wish if
you think that it is important.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150818/e8f7c7ed/attachment.html>