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; }