Frama-C Bug Tracking System - Frama-C
View Issue Details
0001475Frama-CKernelpublic2013-09-03 14:482014-03-13 15:57
dmentre 
virgile 
normalcrashalways
closedfixed 
Frama-C Fluorine-20130601 
Frama-C Neon-20140301 
0001475: Frama-C Kernel on a specific C file (unexpected error, assertion failed)
When 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.
No tags attached.
c q4_error_static_fun.c (770) 2013-09-03 14:48
https://bts.frama-c.com/file_download.php?file_id=518&type=bug
Issue History
2013-09-03 14:48dmentreNew Issue
2013-09-03 14:48dmentreFile Added: q4_error_static_fun.c
2013-09-03 14:53dmentreNote Added: 0004052
2013-09-04 10:19signolesStatusnew => assigned
2013-09-04 10:19signolesAssigned To => virgile
2013-09-18 11:22virgileStatusassigned => acknowledged
2013-09-24 15:01svnCheckin
2013-09-24 15:01svnStatusacknowledged => resolved
2013-09-24 15:01svnResolutionopen => fixed
2014-02-12 16:57Note Added: 0004560
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004052)
dmentre   
2013-09-03 14:53   
Removing the "static" annotation on function F4 avoids the crash.
(0004560)
   
2014-02-12 16:57   
Fix committed to stable/neon branch.