Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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