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

[Frama-c-discuss] Example for jessie



Hello.

I tried to write a program that give the variable z the value of abs(x) and annotate it in ACSL:{T}S{R:z=abs(x)}.
So formally the program looks like this:
     {T}
	if  x≥0→z≔x
	 ∎ x≤0→z≔-x
	fi
     {R:z≥0∧(z=x∨z=-x) }.

In C + ACSL as for me the equal to formal program is:
/*@ requires \true;
  @ assigns  \nothing;
  @ behavior plus:
  @ @ assumes x >= 0;
  @ @ ensures \result ==  x;
  @ @ ensures \result >=  0;
  @ behavior minus:
  @ @ assumes x < 0;
  @ @ ensures \result == -x;
  @ @ ensures \result >=  0;
  @ complete behaviors plus, minus;
  @ disjoint behaviors plus, minus;
  @ */
int z_abs_x(const int x)
{
 int z;
 if (x < 0)         z = -x;
 else if (x >= 0)   z =  x;
 return z;
}
After validation I receive 14 verification conditions, 13 are valid and 1 is unknown. And this result is shown by all Automatic Theorem Provers (Alt-Ergo, CVC3, Z3, yices).
What can be wrong in my annotations?

Thanks in advance.
With best regards,
Viktoriia