2021-03-01 05:21 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000550Frama-CPlug-in > occurrencepublic2014-02-12 16:55
Reporterboris 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000550: Selecting "occurrence" crashes Frama-C
DescriptionMy binary search example crashes Frama-C if I right-click on some variable, eg low, and select "occurrence".
Additional InformationThe full backtrace is:
Raised at file "src/kernel/globals.ml", line 492, characters 10-95
Called from file "src/value/eval.ml", line 5154, characters 22-44
Re-raised at file "src/value/eval.ml", line 5169, characters 50-53
Called from file "src/project/computation.ml", line 914, characters 2-6
Re-raised at file "src/project/computation.ml", line 918, characters 8-11
Called from file "camlinternalOO.ml", line 374, characters 12-17
Called from file "camlinternalOO.ml", line 384, characters 24-40
Called from file "src/project/computation.ml", line 914, characters 2-6
Re-raised at file "src/project/computation.ml", line 918, characters 8-11
Called from file "src/occurrence/register.ml", line 152, characters 2-12
Called from file "src/kernel/journal.ml", line 323, characters 15-26
Re-raised at file "src/kernel/journal.ml", line 338, characters 14-15
Called from file "src/occurrence/register_gui.ml", line 37, characters 9-32
Called from file "src/lib/extlib.ml", line 176, characters 12-15
Re-raised at file "src/lib/extlib.ml", line 181, characters 10-11
Called from file "src/gui/gtk_helper.ml", line 533, characters 8-385

Unexpected error (Globals.No_such_entry_point("Could not find entry point: main")).
Please report as 'crash' at http://bts.frama-c.com
TagsNo tags attached.
Attached Files
  • c file icon binary-search.c (1,085 bytes) 2010-07-28 17:16 -
    /*@ predicate Sorted{L}(int *a, integer l, integer r) =
        \forall integer i,j; l <= i < j <= r ==> a[i] <= a[j];
     */
    
    /*@ requires \valid(a+ (0..a_length-1)) && a_length >= 0;
        requires Sorted(a,0,a_length-1);
        assigns \nothing;
        behavior success:
          assumes \exists integer res; 0 <= res <= a_length-1 && a[res] == val;
          ensures \result >= 0  &&  a[\result] == val;
        behavior failure:
          assumes !(\exists integer res; 0 <= res <= a_length-1 && a[res] == val);
          ensures \result == -1;
        complete behaviors;
        disjoint behaviors;
     */
    int binary_search(int val, int a[], int a_length) {
      int low, mid, high;
    
      low = 0; high = a_length-1;
      /*@ loop invariant 0 <= low && high <= a_length-1;
          loop invariant \forall integer i; 0 <= i < low  ==>  a[i] < val;
          loop invariant \forall integer i; a_length-1  >= i > high  ==>  a[i] > val;
          loop variant high-low;
      */
      while(low <= high) {
        mid = low + (high - low) / 2;
        if (a[mid] < val) low = mid+1;
        else if(a[mid] > val) high = mid-1;
        else return mid;
      }
      return -1;
    }
    
    c file icon binary-search.c (1,085 bytes) 2010-07-28 17:16 +

-Relationships
+Relationships

-Notes

~0001021

signoles (manager)

sure that's a bug.
You have to set kernel parameter "-main" to "binary_search" though.
+Notes

-Issue History
Date Modified Username Field Change
2010-07-28 17:16 boris New Issue
2010-07-28 17:16 boris Status new => assigned
2010-07-28 17:16 boris Assigned To => signoles
2010-07-28 17:16 boris File Added: binary-search.c
2010-07-28 18:21 signoles Note Added: 0001021
2010-07-28 18:21 signoles Status assigned => acknowledged
2010-08-17 10:42 svn
2010-08-17 10:42 svn Status acknowledged => resolved
2010-08-17 10:42 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed
2013-12-19 01:12 signoles Source_changeset_attached => framac master 0c5adb44
2014-02-12 16:55 signoles Source_changeset_attached => framac stable/neon 0c5adb44
+Issue History