2021-02-24 19:06 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001475Frama-CKernelpublic2014-03-13 15:57
Reporterdmentre 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001475: Frama-C Kernel on a specific C file (unexpected error, assertion failed)
DescriptionWhen Frama-C is launched on attached file, I get an exception.

 $ frama-c q4_error_static_fun.c

[kernel] preprocessing with "gcc -C -E -I. questions/q4_error_static_fun.c"
[kernel] failure: Some globals contain dangling references after link:
                  F4:f5;
[kernel] Current source was: questions/q4_error_static_fun.c:35
         The full backtrace is:
         Raised at file "cil/src/mergecil.ml", line 2842, characters 2-167
         Called from file "cil/src/mergecil.ml", line 2903, characters 16-37
         Called from file "src/kernel/file.ml", line 1082, characters 20-56
         Called from file "src/kernel/file.ml", line 1936, characters 12-30
         Called from file "src/kernel/file.ml", line 2020, characters 4-27
         Called from file "src/kernel/ast.ml", line 103, characters 2-28
         Called from file "src/kernel/ast.ml", line 114, characters 53-71
         Called from file "src/kernel/boot.ml", line 29, characters 6-20
         Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
         
         Unexpected error (File "cil/src/mergecil.ml", line 2842, characters 2-8: Assertion failed).
         Please report as 'crash' at http://bts.frama-c.com/.
         Your Frama-C version is Fluorine-20130601.
TagsNo tags attached.
Attached Files
  • c file icon q4_error_static_fun.c (770 bytes) 2013-09-03 14:48 -
    struct T2;
    typedef struct T2 T1;
    struct T2 {
       char M1 ;
       char M2 ;
       char M3 ;
    };
    struct T4;
    typedef struct T4 T3;
    struct T4 {
       char M4 ;
       char M5 ;
       unsigned char M6 ;
       int M7 ;
       int M8 ;
       int M9 ;
       int M10 ;
       int M11 ;
    };
    extern int F1(int f1 , ...);
    
    extern void F2(int f2);
    
    extern int G1;
    
    extern T3 *G2;
    
    /*@ requires \valid(f3); */
    extern char F3(T1 *f3, short f4);
    
    /*@ requires \valid(f5); */
    static char F4(T3 *f5);
    
    static T1 G3[100];
    static char F5(int f6, int f7)
    {
      char V7;
      register T3 *V1;
      register T1 *V2;
      register int V3;
      short V4;
      V1 = (T3 *)((void *)0);
      V2 = G3;
      V3 = f6;
      while (V3 < f7) {
        V1 = G2 + V3;
        switch ((int)V1->M4) {
          case '\000': V4 = (short)F4(V1);
          break;
        }
      }
      return V7;
    }
    
    c file icon q4_error_static_fun.c (770 bytes) 2013-09-03 14:48 +

-Relationships
+Relationships

-Notes

~0004052

dmentre (reporter)

Removing the "static" annotation on function F4 avoids the crash.

~0004560

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2013-09-03 14:48 dmentre New Issue
2013-09-03 14:48 dmentre File Added: q4_error_static_fun.c
2013-09-03 14:53 dmentre Note Added: 0004052
2013-09-04 10:19 signoles Status new => assigned
2013-09-04 10:19 signoles Assigned To => virgile
2013-09-18 11:22 virgile Status assigned => acknowledged
2013-09-24 15:01 svn
2013-09-24 15:01 svn Status acknowledged => resolved
2013-09-24 15:01 svn Resolution open => fixed
2013-12-19 01:11 Source_changeset_attached => framac master 8226db73
2014-02-12 16:53 Source_changeset_attached => framac stable/neon 8226db73
2014-02-12 16:57 Note Added: 0004560
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
+Issue History