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