2021-03-01 04:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001287Frama-CKernelpublic2014-02-12 16:58
ReporterAnne 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityhave not tried
StatusclosedResolutionfixed 
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 Files
  • c file icon bug.c (144 bytes) 2012-10-23 15:29 -
    #include <stdio.h>
    
    int main (FILE * f) {
      int res = 0;
      int code;
      res = fscanf (f, "%d", &code);
      if (res > 10) res = 10;
      return res;
    }
    
    c file icon bug.c (144 bytes) 2012-10-23 15:29 +

-Relationships
+Relationships

-Notes

~0003503

signoles (manager)

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)

Fix committed to stable/neon branch.
+Notes

-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
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
2013-12-19 01:11 signoles Source_changeset_attached => framac master 13ab342c
2014-02-12 16:53 signoles Source_changeset_attached => framac stable/neon 13ab342c
2014-02-12 16:58 signoles Note Added: 0004611
2014-02-12 16:58 signoles Status closed => resolved
+Issue History