Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000667Frama-CPlug-in > jessiepublic2011-01-11 21:032011-01-25 23:18
Reporterdmentre 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000667: /usr/share/frama-c/libc/stdio.h:107:[jessie] failure: Unexpected exception.
DescriptionHello, 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.
TagsNo tags attached.
Attached Filesgz file icon code.tar.gz [^] (3,010 bytes) 2011-01-11 21:03
gz file icon code2.tar.gz [^] (3,294 bytes) 2011-01-24 18:45

- Relationships

-  Notes
(0001420)
dmentre (reporter)
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 (reporter)
2011-01-24 20:25
edited on: 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 (reporter)
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.

- Issue History
Date Modified Username Field Change
2011-01-11 21:03 dmentre New Issue
2011-01-11 21:03 dmentre Status new => assigned
2011-01-11 21:03 dmentre Assigned To => cmarche
2011-01-11 21:03 dmentre File Added: code.tar.gz
2011-01-24 18:45 dmentre Note Added: 0001420
2011-01-24 18:45 dmentre File Added: code2.tar.gz
2011-01-24 20:25 dmentre Note Added: 0001421
2011-01-24 20:25 dmentre Note Edited: 0001421
2011-01-25 23:18 dmentre Note Added: 0001422


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker