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] Example for jessie

  • Subject: [Frama-c-discuss] Example for jessie
  • From: devia88 at mail.ru (Viktoriia)
  • Date: Tue, 15 Jun 2010 17:11:00 +0400
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