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

[Frama-c-discuss] Prove mean()




Hello!

I found? message: [Frama-c-discuss] label L required?


 

 [Frama-c-discuss] label L required?
[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 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!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140609/a28dba31/attachment.html>