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] 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                    |