Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001287Frama-CKernelpublic2012-10-23 15:292014-02-12 16:58
ReporterAnne 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001287: no hook table for parameter -plevel
DescriptionThe 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...
TagsNo tags attached.
Attached Filesc file icon bug.c [^] (144 bytes) 2012-10-23 15:29 [Show Content]

- Relationships

-  Notes
(0003503)
signoles (manager)
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.
(0004611)
signoles (manager)
2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-10-23 15:29 Anne New Issue
2012-10-23 15:29 Anne File Added: bug.c
2012-10-23 16:14 signoles Status new => assigned
2012-10-23 16:14 signoles Assigned To => signoles
2012-10-29 10:09 svn Checkin
2012-10-29 10:09 svn Status assigned => resolved
2012-10-29 10:09 svn Resolution open => fixed
2012-10-29 10:11 signoles Note Added: 0003503
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2014-02-12 16:58 signoles Note Added: 0004611
2014-02-12 16:58 signoles Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker