Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001495Frama-CKernel > ACSL implementationpublic2013-10-01 18:032014-02-05 17:40
Reporteralessioiotti 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001495: crash
DescriptionThe 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;
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004511)
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.

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker