--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on May 2009 ---
Hi all I am new in community. If someone has problem with Ubuntu Z3 installation I have solution: 1) download z3-1.3.6.msi Latest version: Z3 1.3<http://research.microsoft.com/research/downloads/details/0a7db466-c2d7-4c51-8246-07e25900c7e7/details.aspx> . 2) open with wine and install 3) create your home/user/bin directory 4) in .bashrc add : export PATH=/home/user/bin:$PATH 5) restart session 6)in home/user/bin add file z3 with content wine /home/dragan/.wine/drive_c/Program_Files/Microsoft_Research/Z3-1.3.6/bin/z3.exe /s $* 7)save and change permission 8)sudo chmod 775 z3 9) why-config starting autodetection... Found prover Alt-Ergo version 0.8 Found prover Simplify version 1.5.4 err:winedevice:ServiceMain driver L"vstor2-ws60" failed to load Found prover Z3 version 1.3 Found prover Yices version 1.0.21 Found prover CVC3 version devel Found prover Coq version 8.1pl3 detection done. writing rc file... all other provers you can set-up on similar way after running frama-c -jessie-analysis -jessie-gui file.c you will see all available provers. Also two question. In frama-c/why directory I found why-2.17. It is not clear to me ...? Why we have two " why " version ? Another question: Is it possible somehow to include escJava2 prover in frama-c why environment? Best Regards Dragan Senior Software Developer UCD_CASL On Wed, May 20, 2009 at 4:25 PM, Virgile Prevosto <virgile.prevosto at cea.fr>wrote: > Le mer. 20 mai 2009 15:17:29 CEST, > JENN Eric <eric.jenn at fr.thalesgroup.com> a ?crit : > > > Me, again. > > Consider the following code: > > > > void test1() { > > //... > > > { > > /*@ loop invariant 0 <= b <= 3; > > loop invariant > > \forall integer j; > > ( 0 <= j < b ) ==> (the_array[a+j*3] == -1); > > @*/ > > for ( b = 0; b< 3 ; b++) > > { > > the_array[a+b*3] = -1; > > } > > > > /*@ > > assert > > \forall integer j; > > ( 0 <= j < 3 ) ==> (the_array[a+j*3] == -1); > > @*/ > > } > > } > > > > All POs corresponding to the invariants of the inner-most loop, and the > assertion, are discharged. > > The PO corresponding to the preservation of invariant of the outer-most > is demonstrated not to be valid... and I don't understand why? > > Because, the loop invariant of the inner loop is too weak: you specify > what happens on the a-th 'column' of the array, but not that the > preceding ones are left untouched by the loop. And since the loop > annotation is the only thing that jessie sees outside of the loop, > there is nothing in the hypotheses of the PO that says that these > 'columns' still contain -1. > Now the standard ACSL way of specifying that would be a via loop assigns > (left as an exercise for the reader). However, since loop assigns are > not handled by the current version of the jessie plugin, a work-around > must be found in the form of another invariant: > loop invariant > \forall integer i,j; > (0<=i <a) && (0<=j<3) ==> the_array[i+j*3] == -1; > > > In particular, the assertion is demonstrated to be TRUE for all a in > [0,3[ so, doesn't this guarantee the preservation of the outer-most > invariant? > > No, for the same reason as above: the assertion talks about the a-th > 'column'. > > As a final note, note that the outer loop invariant seem to be handled > more easily by ATP when it is written in this form: > loop invariant > \forall integer i,j; > ( 0 <= i < a ) && (0<=j<3) ==> > (the_array[i+j*3] == -1); > > Best regards, > -- > E tutto per oggi, a la prossima volta. > Virgile > > > _______________________________________________ > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090520/a114e1c8/attachment.htm