--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on June 2014 ---
I cannot confirm provability if you use option -jessie-atp z3. This option activates the old why2 VCgen which is not supported anymore. using the now default Why3 backend is the only supported option. - Claude Le 09/06/2014 10:41, Artem Kalinovsky a ?crit : > > Hello! > > I found message: [Frama-c-discuss] label L required? > <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-October/004021.html> > > > > [Frama-c-discuss] label L required? > <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-October/004021.html> > [Frama-c-discuss] label L required? Stephen Siegel siegel at udel.edu > Thu Oct 31 18:42:48 CET 2013 Previous message: [Frama-c-discuss] sums of > arrays > > View on lists.gforge.inria.fr > <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-October/004021.html> > > Preview by Yahoo > > > where you said that you was able to prove mean() function with > Frama-C+Jessie+Z3. I'm tryin to repeat your expirience and prove this > function by myself. I have Ubuntu 12.04 with Frama-C Nitrogen release, > Jessie and Z3 and I have this results: > artem at pb-ts11hr:~$ /usr/bin/frama-c -jessie -jessie-atp z3 > ./?????????/C/mean.c[kernel] preprocessing with "gcc -C -E -I. -dD > ./Documents/C/mean.c" > [jessie] Starting Jessie translation > [jessie] Producing Jessie files in subdir ./?????????/C/mean.jessie > [jessie] File ./?????????/C/mean.jessie/mean.jc written. > [jessie] File ./?????????/C/mean.jessie/mean.cloc written. > [jessie] Calling Jessie tool in subdir ./?????????/C/mean.jessie > Generating Why function mean > [jessie] Calling VCs generator. > why -smtlib [...] why/mean.why > Running Z3 on proof obligations > (. = valid * = invalid ? = unknown # = timeout ! = failure) > smtlib/mean_why.smt : .....#.........# (14/0/0/2/0) > total : 16 > valid : 14 ( 88%) > invalid : 0 ( 0%) > unknown : 0 ( 0%) > timeout : 2 ( 12%) > failure : 0 ( 0%) > total wallclock time : 21.88 sec > total CPU time : 10.57 sec > valid VCs: > average CPU time : 0.04 > max CPU time : 0.06 > invalid VCs: > average CPU time : -nan > max CPU time : 0.00 > unknown VCs: > average CPU time : -nan > max CPU time : 0.00 > > Why I have 2 timeouts? Please, could you provide me with information how > to get 100% valid result? > > Thank you! > > > > _______________________________________________ > 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 > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |