--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Nitrogen/Jessie crashes



Hello,

On 02/15/2012 10:26 PM, Alwyn Goodloe wrote:
> Having postponed moving to Nitrogen I'm finally caving in. I've gone
> through a lot struggle to get Why3 built on OS X
> 10.6.8 and have been able to work through many of the examples. I've
> also gotten the value analysis tool to run, but jessie
> keeps crashing on everything (for example see below). I'm sure it's some
> silly issue that I just keep missing.
> Anyone who encountered the Jessie translation errors seen below please
> let me know.

Unfortunately I'm not able to reproduce your issue on my AMD64 Linux 
machine using Frama-C Nitrogen, Why 3.0.71 and the Jessie plug-in 
included in Why 2.30.

Thanks to the provided backtrace, I can say that the crash should not be 
system dependent and comes from an undefined function called 
"mem_project" somewhere in the tool. Unfortunately there are hundreds 
definitions of this function in Frama-C and I do not want to check each 
of them one by one to find the wrong undefined one... Without 
reproducing the error, I'm afraid I can do nothing :-(. Could you 
produce you test file?

--
Julien

> ----------------------------------------------------------
>
> rc220016257:examples agoodloe$ frama-c -jessie find.c
> [kernel] preprocessing with "gcc -C -E -I. -dD find.c"
> [jessie] Starting Jessie translation
> [kernel] The full backtrace is:
> Called from file "src/project/state_builder.ml
> <http://state_builder.ml>", line 439, characters 10-31
> Called from file "src/project/project.ml <http://project.ml>", line 119,
> characters 28-67
> Called from file "hashtbl.ml <http://hashtbl.ml>", line 157, characters
> 23-35
> Called from file "hashtbl.ml <http://hashtbl.ml>", line 161, characters
> 12-33
> Called from file "src/project/project.ml <http://project.ml>", line 116,
> characters 6-364
> Called from file "list.ml <http://list.ml>", line 69, characters 12-15
> Called from file "src/lib/qstack.ml <http://qstack.ml>", line 107,
> characters 4-23
> Called from file "src/kernel/file.ml <http://file.ml>", line 1376,
> characters 2-33
> Called from file "register.ml <http://register.ml>", line 96, characters
> 4-93
> Called from file "register.ml <http://register.ml>", line 290,
> characters 6-12
> Called from file "queue.ml <http://queue.ml>", line 134, characters 6-20
> Called from file "src/kernel/boot.ml <http://boot.ml>", line 36,
> characters 4-20
> Called from file "src/kernel/cmdline.ml <http://cmdline.ml>", line 723,
> characters 2-9
> Called from file "src/kernel/cmdline.ml <http://cmdline.ml>", line 200,
> characters 4-8
> Unexpected error (File "src/type/datatype.ml <http://datatype.ml>", line
> 98, characters 18-24: Assertion failed).
> Please report as 'crash' at http://bts.frama-c.com/.
> Your Frama-C version is Nitrogen-20111001.
> Note that a version and a backtrace alone often does not have information
> to understand the bug. Guidelines for reporting bugs are at:
> http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
>
>
> --
> Alwyn E. Goodloe, Ph.D.
> agoodloe at gmail.com <mailto:agoodloe at gmail.com>
>
> Research Computer Engineer
> NASA Langley Research Center
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss