--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on January 2009 ---
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