Frama-C Bug Tracking System - Frama-C
View Issue Details
0001287Frama-CKernelpublic2012-10-23 15:292014-02-12 16:58
normalcrashhave not tried
Frama-C Oxygen-20120901 
Frama-C Fluorine-20130401 
0001287: no hook table for parameter -plevel
The command : cat jnl | frama-c.toplevel with jnl : let cpp = File.get_preprocessor_command ();; (* let cpp = cpp^" -I /usr/local/share/frama-c/libc/";; *) File.init_from_c_files ((File.from_filename ~cpp "bug.c")::[]);; !Db.Value.compute ();; and the attached bug.c file, gives : [kernel] failure: [Emitter] no hook table for parameter -plevel Exception: Log.AbortFatal "kernel". If the second line of jnl is de-commented (use Frama-C includes), or if anything else is changed in the source file, it works ! The problem is not important by itself, but I report it because I think there should be a strange thing somewhere since as soon as I change something in the example, the behavior if different. So, I thought this might interest you...
No tags attached.
c bug.c (144) 2012-10-23 15:29
Issue History
2012-10-23 15:29AnneNew Issue
2012-10-23 15:29AnneFile Added: bug.c
2012-10-23 16:14signolesStatusnew => assigned
2012-10-23 16:14signolesAssigned To => signoles
2012-10-29 10:09svnCheckin
2012-10-29 10:09svnStatusassigned => resolved
2012-10-29 10:09svnResolutionopen => fixed
2012-10-29 10:11signolesNote Added: 0003503
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2014-02-12 16:58signolesNote Added: 0004611
2014-02-12 16:58signolesStatusclosed => resolved

2012-10-29 10:11   
Fixed. But arguably it is not a bug: this code should be part of a main. It is not specified what Frama-C does when running such a code at toplevel.
2014-02-12 16:58   
Fix committed to stable/neon branch.