--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on February 2012 ---
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