2021-03-02 15:52 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001584Frama-CPlug-in > Evapublic2014-03-13 15:57
Reporteryakobowski 
Assigned Topascal 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001584: Assertion failure in Ival.scale_div
Description(Csmith-found program, reduced by creduce)

To be analyzed with -slevel 4.

Interesting part of the backtrace:
         Called from file "src/ai/ival.ml", line 1011, characters 3-123
         Called from file "src/ai/ival.ml", line 1166, characters 2-35
         Called from file "src/ai/ival.ml", line 2370, characters 20-48
TagsNo tags attached.
Attached Files
  • ? file icon small3.i (226 bytes) 2013-12-09 17:30 -
    int a, c, d, e, f;
    int *b = &a;
    main ()
    {   /*    *//*    */
        f = fn1 ();
        *b = 4294967288 | f;
        d = 1;
        for (;; d = d - 9)
        {   /*    */
            c = 0;
            for (; c < 3; c++)
                e = d / a;
        }
    }
    
    ? file icon small3.i (226 bytes) 2013-12-09 17:30 +

-Relationships
+Relationships

-Notes

~0004545

pascal (reporter)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2013-12-09 17:29 yakobowski New Issue
2013-12-09 17:29 yakobowski Status new => assigned
2013-12-09 17:29 yakobowski Assigned To => pascal
2013-12-09 17:30 yakobowski File Added: small3.i
2013-12-09 20:55 svn
2013-12-09 20:55 svn Status assigned => resolved
2013-12-09 20:55 svn Resolution open => fixed
2013-12-19 01:11 pascal Source_changeset_attached => framac master 639c69ca
2014-02-12 16:53 pascal Source_changeset_attached => framac stable/neon 639c69ca
2014-02-12 16:57 pascal Note Added: 0004545
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History