--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Lemma from ACSL doc doesn't verify



More precisely, consider this code:


//@ lemma mean_property2: \forall integer l, h; l <= h  ==>  l <= (l+h)/2 <= h;

//@ ensures l <= \result <= h;
Int foo(int l, int h) {
  return (l+h)/2;
}

Main() {
  int a = foo(maxint, maxint);
}


I can't test this with my installation because Beryllium1 doesn't verify mean_property2. If this lemma can be proved however, what result is Jessie supposed to give on this code?

- Boris


> Lemma mean_property2 DOES HOLD for int since in annotations, + means
> addition on integers and not on ints.

> - Claude