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