crash

ID0001495: This issue was created automatically from Mantis Issue 1495. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001495	Frama-C	Kernel > ACSL implementation	public	2013-10-01	2014-02-05

Reporter	alessioiotti	Assigned To	virgile	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Fluorine-20130601	Target Version	-	Fixed in Version	-

Description :

The full backtrace is: Raised at file "hashtbl.ml", line 254, characters 18-27 Called from file "hashtbl.ml", line 262, characters 22-38

The program raise an unexpected error trying to prove an ensures clause with behavior using a logic function.

The code is the following:

/*@
  @ predicate IsValidRange(int* a, integer n) =
  @   (0 <= n) && \valid(a+(0.. n-1));
  @
  @
  @ predicate IsEqual{A, B}(int* a, int* b, integer n) =
  @   \forall integer i; 0 <= i < n ==> \at(a[i], A) == \at(b[i], B);
  @
  @ logic integer MinIndex(int* a, int* b, integer starting_index, integer count) =
  @   ((count <= 0 || starting_index >= count) ? -1 : 
  @     (starting_index == count)) ? -1 :
  @        (a[starting_index] != b[starting_index]) ? starting_index : MinIndex(a, b, (starting_index + 1), count);       
*/
 
/*@ requires \valid(a+(0..n-1)) && \valid(b+(0..n-1)) && (n >= 0);
  @ assigns \nothing;
  @ behavior equal:
  @   assumes IsEqual{Here, Here}(a, b, n);
  @   ensures \result == n;
  @ behavior not_equal:
  @   assumes !IsEqual{Here, Here}(a, b, n);
  @   ensures \result == MinIndex(a, b, 0, n);
  @ complete behaviors;
  @ disjoint behaviors;
*/
int mismatch(const int* a, const int* b, int n) {
    /*@ loop assigns i;     	    
      @ loop invariant (0 <= i <= n) && IsEqual{Here, Here}(a, b, i);
      @ loop variant n - i;
    */
  for (int i = 0; i < n; i++)
    if (a[i] != b[i])
      return i;
  
  return n;
}