--- layout: fc_discuss_archives title: Message 90 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Array problem - Jessie plugin



Hi,

This is the same situation as your example with a struct. The workaround
is to introduce a ghost variable.

There is no need to introduce ghost variables when you have two or more
array assignments because Jessie does a special treatment of parallel
assignments. However, the current discussion make me think that every
assignments should be treated as parallel assignments are treated. I may
consider adding this in the next release.

- Claude

On 10/21/2013 02:03 PM, Luciana Burgareli wrote:
> Hi,
> 
> This is a very simple example, but it was not proved.
> 
> If we slightly modify the code and we add an assignment to the Ang2[1]
> (and the related assigns and ensures clauses), both the ensures clauses
> are proved.
> 
> Why is not the attached example proved?
> 
> How to solve this problem?
> 
> We are using the Jessie Plugin, Why3 Verification Platform 0.81,
> Fluorine-20130601 and the provers Alt-Ergo 0.95.2, CVC3 2.4.1, Gappa
> 1.0.0 and Z3 4.3.2.
> 
> 
> Luciana
> 
> 
> 
> _______________________________________________
> 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
>