2021-02-27 11:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000239Frama-CPlug-in > jessiepublic2013-03-27 09:44
ReporterChristoph 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000239: internal error when analyzing max.h
DescriptionCall and message:

File max.h is appended, no file created by frama-c

$ frama-c -jessie max.h
[kernel] preprocessing with "gcc -C -E -I. -dD max.h"
[jessie] Starting Jessie translation
[jessie] user error: Nothing to process. There was probably an error before.
max.h:27:[jessie] failure: Unexpected exception.
                  Please submit bug report (Ref. "Log.AbortError("jessie")").
[kernel] Plugin jessie aborted because of an internal error.
         Please report with 'crash' at http://bts.frama-c.com
TagsNo tags attached.
Attached Files
  • ? file icon max.h (735 bytes) 2009-09-11 13:42 -
    #ifndef _max_h
    #define _max_h
    /*
     frama-c -jessie-analysis -jessie-int-model exact -jessie-gui max.c
     ======================================================================================
     DESCRIPTION:
      Returns the greater of a and b.
      The comparison uses operator< (b<a) for the first version, and comp for the second.
    
    
     Parameters:
      a, b:
       Items to compare. T is any type supporting copy constructions and comparisons with
       operator<.
      Return value:
       The greater of its two arguments
    
     Complexity:
      Constant
     ======================================================================================
    */
    
    /*@
     ensures \result >= a && \result >= b;
      ensures \result == a || \result == b;
    */
    int max ( int a, int b );
    
    #endif
    
    ? file icon max.h (735 bytes) 2009-09-11 13:42 +

-Relationships
related to 0000509closedcmarche Unexpected exception if no input file 
+Relationships

-Notes

~0000396

virgile (developer)

jessie should exit more gracefully, but the initial issue is that there is indeed nothing to do here: frama-c does not keep pure prototypes (i.e. which are not bound to a definition elsewhere) which are not used. This behavior is intended to avoid cluttering a project with unused prototypes coming from the inclusion of a standard library file.

~0003433

yakobowski (manager)

Jessie now exits more gracefully on empty. Moreover, starting from Oxygen, Frama-C will keep unreferenced functions with specifications.

~0003777

signoles (manager)

Fixed in Frama-C Oxygen + Why 2.32.
+Notes

-Issue History
Date Modified Username Field Change
2009-09-11 13:42 Christoph New Issue
2009-09-11 13:42 Christoph File Added: max.h
2009-09-12 07:15 signoles Status new => assigned
2009-09-12 07:15 signoles Assigned To => correnson
2009-09-14 10:21 virgile Note Added: 0000396
2010-07-19 16:43 signoles Relationship added related to 0000509
2012-09-07 17:57 yakobowski Note Added: 0003433
2012-09-07 17:57 yakobowski Status assigned => resolved
2012-09-07 17:57 yakobowski Resolution open => fixed
2013-03-27 09:43 signoles Note Added: 0003777
2013-03-27 09:44 signoles Fixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44 signoles Status resolved => closed
+Issue History