---
layout: fc_discuss_archives
title: Message 21 from Frama-C-discuss on October 2011
---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] WP plugin / question about address of variable on stack
- Subject: [Frama-c-discuss] WP plugin / question about address of variable on stack
- From: anne.pacalet at inria.fr (Anne Pacalet)
- Date: Mon, 17 Oct 2011 11:01:54 +0200
- In-reply-to: <CAFaEDLBHbMS-XxrnqtQkrKjfmAJvJa+sNsPQRrSX0L6=bhp+pQ@mail.gmail.com>
- References: <CAFaEDLB1ae2J8G9g+WzHUkbrVcLDorhPefaq6d9B8OyO5YEF=Q@mail.gmail.com> <F3E66EEC-D8CA-4E87-9DFD-1A64AF1D5878@first.fraunhofer.de> <CAFaEDLAvkH=TkN2d_PEQ15dF7x1HFa-OFccf4SvN1NTOahW8jw@mail.gmail.com> <CAFaEDLBHbMS-XxrnqtQkrKjfmAJvJa+sNsPQRrSX0L6=bhp+pQ@mail.gmail.com>
Le 17/10/2011 10:40, sylvain nahas a ?crit :
> Still, I would really like to know the actual definition of \valid in
> the Frama-C framework.
> Does it only cover positive non zero integers or is there other constraints?
I think that \valid(p) holds at program points where
the memory location (*p) is allocated.
Hope this helps,
--
Anne.