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()

  • Subject: [Frama-c-discuss] Prove mean()
  • From: artem_kalinovsky at yahoo.com (Artem Kalinovsky)
  • Date: Mon, 9 Jun 2014 01:41:34 -0700 (PDT)

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>