--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on June 2010 ---
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