2021-03-02 02:54 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001440Frama-CKernelpublic2014-03-13 15:57
Reporterguillaume-petiot 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001440: AST integrity check failure with kernel-debug
Descriptiona.c:6:[kernel] failure: [AST Integrity Check] initial AST
                  Following functions and variables are present in global tables but not in AST:
                  Functions:
                  __builtin_va_arg(158) __builtin_stdarg_start(162) __builtin_next_arg(310)
                  __builtin_expect(350) __builtin_va_start(357) __builtin_va_arg(541)
                  __builtin_stdarg_start(545) __builtin_next_arg(693) __builtin_expect(733)
                  __builtin_va_start(740)
Fatal error: exception Log.AbortFatal("kernel")
Raised at file "src/kernel/log.ml", line 523, characters 30-31
Called from file "src/kernel/log.ml", line 517, characters 9-16
Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
Called from file "src/kernel/file.ml", line 717, characters 8-413
Called from file "cil/src/cil.ml", line 5887, characters 7-84
Called from file "src/kernel/file.ml", line 1449, characters 36-147
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
Re-raised at file "src/kernel/cmdline.ml", line 226, characters 14-17
Called from file "src/kernel/boot.ml", line 66, characters 2-355
Steps To Reproduce$ frama-c a.c -check -kernel-debug 1
TagsNo tags attached.
Attached Files
  • c file icon a.c (152 bytes) 2013-06-03 15:44 -
    /*@ ensures \result >= i;
      @ ensures \result >= j;
      @ ensures \result == i || \result == j;
      @*/
    int max(int i, int j) {
      return (i>=j) ? i : j;
    }
    
    c file icon a.c (152 bytes) 2013-06-03 15:44 +

-Relationships
+Relationships

-Notes

~0004572

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2013-06-03 15:43 guillaume-petiot New Issue
2013-06-03 15:43 guillaume-petiot Status new => assigned
2013-06-03 15:43 guillaume-petiot Assigned To => virgile
2013-06-03 15:43 guillaume-petiot File Added: a.c
2013-06-03 15:44 guillaume-petiot File Deleted: a.c
2013-06-03 15:44 guillaume-petiot File Added: a.c
2013-06-03 15:57 guillaume-petiot Severity minor => crash
2013-06-06 18:06 svn
2013-06-06 18:06 svn Status assigned => resolved
2013-06-06 18:06 svn Resolution open => fixed
2013-12-19 01:11 Source_changeset_attached => framac master 074ffe12
2014-02-12 16:53 Source_changeset_attached => framac stable/neon 074ffe12
2014-02-12 16:58 Note Added: 0004572
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
+Issue History