| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0001495 | Frama-C | Kernel > ACSL implementation | public | 2013-10-01 18:03 | 2014-02-05 17:40 | ||||||||
| Reporter | alessioiotti | ||||||||||||
| Assigned To | virgile | ||||||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Product Version | Frama-C Fluorine-20130601 | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0001495: crash | ||||||||||||
| 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; } | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
virgile (developer) 2014-02-05 17:40 |
issue lies in the fact that MinIndex is recursive and uses an implicit label, which fails to be propagated in the recursive call. A work around is to explicitely declare MinIndex as taking a label argument and to pass it in the recursive call. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2013-10-01 18:03 | alessioiotti | New Issue | |
| 2013-10-01 18:03 | alessioiotti | Status | new => assigned |
| 2013-10-01 18:03 | alessioiotti | Assigned To | => correnson |
| 2014-02-05 17:37 | virgile | Assigned To | correnson => virgile |
| 2014-02-05 17:37 | virgile | Category | Plug-in > wp => Kernel > ACSL implementation |
| 2014-02-05 17:40 | virgile | Note Added: 0004511 | |
| Issue History |