--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] \at in ACSL assertions



Dear Frama-C discussers,

I submit to you the program below. It raises three questions:

a- should the commented functions main and f be parsable by the
front-end? Currently, they can't be parsed with either Boron or the
development version. The error message is similar to "u.c:14:[kernel]
user error: logic label `cond' not found in annotation"

b- if they were parsable, should the assertion in each function be provable?

c- should the assertion in parsable function g be provable?

Pascal
___

#if 0
int main(void)
{
  int i, j;
  for (i=0; i<=4; i++)
    {
      j=i;
    cond:
      if (i%2)
	{
	odd:
	  j=1;
	}
    }
  /*@ assert \at( \at(j, odd), cond) == 3; */
  return 0;
}

int f(int c, int d)
{
  int i, j;
  if (c)
    i=d;
  if (c)
    {
    then:
      j=1;
    }
  /*@ assert \at(i-d, then) == 0; */
  return 0;
}
#endif


int g(int c, int d)
{
  int i, j;
  if (c) goto next1;
    i=d;
 next1:
    if (c) goto next2;
 then:
    j=1;
 next2:
  /*@ assert \at(i-d, then) == 0; */
  return 0;
}