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] perhaps a bug
- Subject: [Frama-c-discuss] perhaps a bug
- From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
- Date: Mon, 19 Jan 2009 15:19:27 +0100
Hello, I am trying to combine numerous annotated algorithms and proving them with Jessie. Unfortunatly I get following message. $ Parsing [preprocessing] running gcc -C -E -I. -ID:/"Eigene Dateien"/StudienUnterlagen/P axissemester/SVN/trunk/Framac/own-examples/predicate_library -include C:\Frama- \share\frama-c\jessie\jessie_prolog.h -D JESSIE_EXACT_INT_MODEL -dD remove_arra .c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir remove_array.jessie File remove_array.jessie/remove_array.jc written. File remove_array.jessie/remove_array.cloc written. Calling Jessie tool in subdir remove_array.jessie Generating Why function remove_copy_array Generating Why function find_array Generating Why function remove_array memory (mem-field(int_M),a_1_24) in memory set (mem-field(int_M),a_1_24), (mem-field(int_M),dest_25) File "jc/jc_interp_misc.ml", line 707, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Assertion failed Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs emove_array.cloc remove_array.jc The corresponding files are appended. I would like to know whether I missed something and Jessie is capable of proving it with a correction or if this is a bug and I should forward this mail to the BTS. Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090119/08ae2bb7/attachment.htm -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: remove_array.c Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090119/08ae2bb7/attachment.txt -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: remove_array.h Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090119/08ae2bb7/attachment-0001.txt