2021-02-24 18:42 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000752Frama-CPlug-in > Evapublic2014-02-12 16:59
Reporterkerstin 
Assigned Topascal 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000752: Unexpected error (Ival.Float_abstract.Bottom)
DescriptionCrash if the 3 assertions are added to the program.

Unexpected error (Ival.Float_abstract.Bottom).

commandline: frama-c-gui -val -slevel 10 -main interp interp_bug.c
             frama-c -val -slevel 10 -main interp interp_bug.c
TagsNo tags attached.
Attached Files
  • c file icon interp_bug.c (1,159 bytes) 2011-03-11 10:57 -
    struct point { double x; double y; };
    
    struct point t[] =
      { 0.,    1.,
        0.125, 1.00782267782571089,
        0.25,  1.03141309987957319,
        0.5,   1.1276259652063807,
        1.,    1.54308063481524371,
        2.,    3.76219569108363139,
        5.,    74.2099485247878476,
        10.,   11013.2329201033244 };
    
    /*@
      requires 0. <= x <= 10. ;
      ensures 0 <= \result <= 6 ; */
    int choose_segment(double x);
    
    /*@ requires 0. <= x <= 10. ; */
    double interp(double x)
    {
      double x0, x1, y0, y1;
      int i;
      i = choose_segment(x);
      x0 = t[i].x;
      y0 = t[i].y;
      x1 = t[i+1].x;
      y1 = t[i+1].y;
      
      /*@ assert x0 == 0. || x0 == 0.125 || x0 == 0.25 || x0 == 0.5 || 
                 x0 == 1. || x0 == 2. || x0 == 5.;
      */
      /*@ assert x1 == 0.125 || x1 == 0.25 || x1 == 0.5 || 
                 x1 == 1. || x1  == 2. || x1 == 5. || x1 == 10.;
      */
      /*@ assert x0 == 0. && x1 == 0.125 || 
                 x0 == 0.125 && x1 == 0.25 || 
                 x0 == 0.25 && x1 == 0.5 || 
                 x0 == 0.5 && x1 == 1. || 
                 x0 == 1. && x1 == 2. || 
                 x0 == 2. && x1 == 5. || 
                 x0 == 5. && x1 == 10.;
      */
      return (y1 * (x - x0) + y0 * (x1 - x)) / (x1 - x0);
    }
    
    c file icon interp_bug.c (1,159 bytes) 2011-03-11 10:57 +

-Relationships
+Relationships

-Notes

~0004823

pascal (reporter)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-03-11 10:57 kerstin New Issue
2011-03-11 10:57 kerstin Status new => assigned
2011-03-11 10:57 kerstin Assigned To => pascal
2011-03-11 10:57 kerstin File Added: interp_bug.c
2011-03-11 12:41 svn
2011-03-11 12:41 svn Status assigned => resolved
2011-03-11 12:41 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 pascal Source_changeset_attached => framac master b974ea9a
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon b974ea9a
2014-02-12 16:59 pascal Note Added: 0004823
2014-02-12 16:59 pascal Status closed => resolved
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History