--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Prove mean()



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                    |