Frama-C Bug Tracking System - Frama-C
View Issue Details
0000667Frama-CPlug-in > jessiepublic2011-01-11 21:032011-01-25 23:18
dmentre 
cmarche 
normalcrashalways
assignedopen 
Frama-C Boron-20100401 
 
0000667: /usr/share/frama-c/libc/stdio.h:107:[jessie] failure: Unexpected exception.
Hello, I'm using Frama-C Boron (Ubuntu package on Ubuntu 10.10). A fatal exception is raised when applying jessie plugin on attached program using following command: frama-c -jessie -jessie-atp alt-ergo -pp-annot -cpp-command "gcc -C -E -I. -I /usr/share/frama-c/libc" evoting.c Result: [kernel] preprocessing with "gcc -C -E -I. -I /usr/share/frama-c/libc -dD evoting.c" [jessie] Starting Jessie translation [kernel] No code for function __Frama_C_free_at_pos, default assigns generated /usr/share/frama-c/libc/stdio.h:107:[jessie] failure: Unexpected exception. Please submit bug report (Ref. "Extlib.NotYetImplemented("Interp.pred Pfresh")"). [kernel] The full backtrace is: Raised at file "src/kernel/log.ml", line 506, characters 30-31 Called from file "src/kernel/log.ml", line 500, characters 2-9 Re-raised at file "src/kernel/log.ml", line 503, characters 8-9 Called from file "src/lib/type.ml", line 746, characters 40-45 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 50, characters 4-20 Called from file "src/kernel/cmdline.ml", line 170, characters 4-8 Plug-in jessie aborted because of an internal error. Please report as 'crash' at http://bts.frama-c.com Any workaround would be appreciated. Best regards, d.
No tags attached.
gz code.tar.gz (3,010) 2011-01-11 21:03
https://bts.frama-c.com/file_download.php?file_id=149&type=bug
gz code2.tar.gz (3,294) 2011-01-24 18:45
https://bts.frama-c.com/file_download.php?file_id=153&type=bug
Issue History
2011-01-11 21:03dmentreNew Issue
2011-01-11 21:03dmentreStatusnew => assigned
2011-01-11 21:03dmentreAssigned To => cmarche
2011-01-11 21:03dmentreFile Added: code.tar.gz
2011-01-24 18:45dmentreNote Added: 0001420
2011-01-24 18:45dmentreFile Added: code2.tar.gz
2011-01-24 20:25dmentreNote Added: 0001421
2011-01-24 20:25dmentreNote Edited: 0001421
2011-01-25 23:18dmentreNote Added: 0001422

Notes
(0001420)
dmentre   
2011-01-24 18:45   
In code.tar.gz, it is function print_candidate_array() in evoting.c that crashes Jessie plugin. Please find attached the modified project code2.tar.gz that exhibits the fault. Just do a "make check" (tested with Frama-C Boron).
(0001421)
dmentre   
2011-01-24 20:25   
The bug is reproducible with Frama-C Carbon beta2 and Why 2.28. I cannot change the "Product Version" field. Command line: frama-c -jessie-atp alt-ergo -jessie -pp-annot -cpp-command "gcc -DFRAMA_C_MALLOC_INDIVIDUAL -C -E -I. -I /usr/local/stow/frama-c-carbon-beta2/share/frama-c/libc" evoting.c /usr/local/stow/frama-c-carbon-beta2/share/frama-c/libc/stdlib.c Error message: """ [kernel] preprocessing with "gcc -DFRAMA_C_MALLOC_INDIVIDUAL -C -E -I. -I /usr/local/stow/frama-c-carbon-beta2/share/frama-c/libc -dD evoting.c" [kernel] preprocessing with "gcc -DFRAMA_C_MALLOC_INDIVIDUAL -C -E -I. -I /usr/local/stow/frama-c-carbon-beta2/share/frama-c/libc -dD /usr/local/stow/frama-c-carbon-beta2/share/frama-c/libc/stdlib.c" [jessie] Starting Jessie translation [jessie] warning: Termination condition(s) ignored [kernel] State_builder.aborted because of unimplemented feature. Please send a feature request at http://bts.frama-c.com with: 'Interp.pred Pfresh'. """ Is there any way to work around this issue? I was able to check my code with older version of Frama-C.
(0001422)
dmentre   
2011-01-25 23:18   
The issue is with stdlib.h provided by Frama-C Boron and Carbon beta 2. Not including it allows to start Jessie.