--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on June 2014 ---
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>