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] WP plugin / question about address of variable on stack

  • Subject: [Frama-c-discuss] WP plugin / question about address of variable on stack
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Mon, 17 Oct 2011 10:40:10 +0200
  • In-reply-to: <CAFaEDLAvkH=TkN2d_PEQ15dF7x1HFa-OFccf4SvN1NTOahW8jw@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>
Hi,

you are right!

\valid(a) => a != 0.

------------------------------------------------------------------------------
/** @verbatim */
/*@ requires val1_valid: \valid(val1);
  @ requires val2_valid: \valid(val2);

  @ ensures C: *val1 == \old(*val2) ;
  @ ensures D: *val2 == \old(*val1) ;

  @ assigns *val1,*val2 ;
 @*/

/** @endverbatim */

void swap(int *val1,int *val2)
{
	int tmp = *val1;
	*val1 = *val2;
	*val2 = tmp;
}

/*@ assigns \nothing ; */
void call_swap()
{
	int a = 1;
	swap(&a, 0);
}
------------------------------------------------------------------------------

... does not validate.
Given that, the way to specify a pointer that may be valid at address
0 is to specifies it as an integer with the correct range.

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?

Thanks for your hint, again.
Sylvain