### uname -a: Linux clpc8.cs.ox.ac.uk 2.6.34.7-56.fc13.x86_64 #1 SMP Wed Sep 15 03:36:55 UTC 2010 x86_64 x86_64 x86_64 GNU/Linux ### cat /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 0 cpu cores : 4 apicid : 0 initial apicid : 0 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5653.20 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 1 cpu cores : 4 apicid : 1 initial apicid : 1 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.19 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 2 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 2 cpu cores : 4 apicid : 2 initial apicid : 2 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.20 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 3 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 3 cpu cores : 4 apicid : 3 initial apicid : 3 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.21 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: ### cat /proc/meminfo: MemTotal: 3891428 kB MemFree: 3570668 kB Buffers: 904 kB Cached: 63644 kB SwapCached: 39932 kB Active: 36904 kB Inactive: 102908 kB Active(anon): 32712 kB Inactive(anon): 84384 kB Active(file): 4192 kB Inactive(file): 18524 kB Unevictable: 0 kB Mlocked: 0 kB SwapTotal: 12586892 kB SwapFree: 10148420 kB Dirty: 40 kB Writeback: 0 kB AnonPages: 50392 kB Mapped: 3720 kB Shmem: 41844 kB Slab: 39088 kB SReclaimable: 21280 kB SUnreclaim: 17808 kB KernelStack: 2080 kB PageTables: 17292 kB NFS_Unstable: 0 kB Bounce: 0 kB WritebackTmp: 0 kB CommitLimit: 14532604 kB Committed_AS: 2871532 kB VmallocTotal: 34359738367 kB VmallocUsed: 385656 kB VmallocChunk: 34359345788 kB HardwareCorrupted: 0 kB HugePages_Total: 0 HugePages_Free: 0 HugePages_Rsvd: 0 HugePages_Surp: 0 Hugepagesize: 2048 kB DirectMap4k: 10236 kB DirectMap2M: 4016128 kB ### date: Fri Oct 14 01:35:18 BST 2011 ### user: mictau ### ulimit -a: core file size (blocks, -c) 0 data seg size (kbytes, -d) unlimited scheduling priority (-e) 0 file size (blocks, -f) unlimited pending signals (-i) 30273 max locked memory (kbytes, -l) 64 max memory size (kbytes, -m) unlimited open files (-n) 1024 pipe size (512 bytes, -p) 8 POSIX message queues (bytes, -q) 819200 real-time priority (-r) 0 stack size (kbytes, -s) 10240 cpu time (seconds, -t) unlimited max user processes (-u) 1024 virtual memory (kbytes, -v) 3584000 file locks (-x) unlimited ### timeout: timeout -s SIGINT 3600 ### tool version info: 4.0 ### tool command: cbmc ### full command line: cbmc /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/fevs-mean/mean_bad.0.0.i ### expected verification result: unknown ############################################################################### file /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/fevs-mean/mean_bad.0.0.i: Parsing Converting Type-checking mean_bad.0.0 Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking Unwinding loop c::main.0 iteration 1 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 2 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 3 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 4 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 5 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 6 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 7 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 8 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 9 file other/fevs-mean/mean_bad.c line 37 function main Unwinding loop c::main.0 iteration 10 file other/fevs-mean/mean_bad.c line 37 function main size of program expression: 76 assignments simple slicing removed 2 assignments Generated 1 VCC(s), 1 remaining after simplification Passing problem to propositional reduction Running propositional reduction Solving with MiniSAT2 with simplifier 100851 variables, 408314 clauses SAT checker: negated claim is SATISFIABLE, i.e., does not hold Runtime decision procedure: 1.961s Building error trace Counterexample: State 2 file line 26 thread 0 ---------------------------------------------------- __CPROVER_deallocated=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 3 file line 27 thread 0 ---------------------------------------------------- __CPROVER_malloc_object=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 4 file line 28 thread 0 ---------------------------------------------------- __CPROVER_malloc_size=0 (0000000000000000000000000000000000000000000000000000000000000000) State 5 file line 37 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000000000000000000000000000) State 6 file /usr/include/stdio.h line 165 thread 0 ---------------------------------------------------- stdin=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 7 file /usr/include/stdio.h line 166 thread 0 ---------------------------------------------------- stdout=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 8 file /usr/include/stdio.h line 167 thread 0 ---------------------------------------------------- stderr=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 9 file /usr/include/bits/sys_errlist.h line 27 thread 0 ---------------------------------------------------- sys_nerr=0 (00000000000000000000000000000000) State 12 thread 0 ---------------------------------------------------- argv[argc]=(irep("(\"nil\")"))[2] (?) State 14 thread 0 ---------------------------------------------------- argc=2 (00000000000000000000000000000010) State 15 thread 0 ---------------------------------------------------- argv=&argv[0] (0000001000000000000000000000000000000000000000000000000000000000) State 16 file other/fevs-mean/mean_bad.c line 33 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 17 file other/fevs-mean/mean_bad.c line 35 function main thread 0 ---------------------------------------------------- sum=0.000000f (00000000000000000000000000000000) State 18 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=1 (00000000000000000000000000000001) State 20 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=-128 (11111111111111111111111110000000) State 21 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=-128.997864f (11000011000000001111111101110100) State 22 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=2 (00000000000000000000000000000010) State 25 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 26 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+inf (01111111100000000000000000000000) State 27 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=3 (00000000000000000000000000000011) State 30 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 31 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+inf (01111111100000000000000000000000) State 32 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=4 (00000000000000000000000000000100) State 35 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 36 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+NaN (01111111100000000000000000000001) State 37 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=5 (00000000000000000000000000000101) State 40 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 41 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+NaN (01111111100000000000000000000001) State 42 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=6 (00000000000000000000000000000110) State 45 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 46 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+NaN (01111111100000000000000000000001) State 47 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=7 (00000000000000000000000000000111) State 50 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 51 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+NaN (01111111100000000000000000000001) State 52 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=8 (00000000000000000000000000001000) State 55 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 56 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+NaN (01111111100000000000000000000001) State 57 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=9 (00000000000000000000000000001001) State 60 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 61 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+NaN (01111111100000000000000000000001) State 62 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=10 (00000000000000000000000000001010) State 65 file other/fevs-mean/mean_bad.c line 38 function main thread 0 ---------------------------------------------------- x=0 (00000000000000000000000000000000) State 66 file other/fevs-mean/mean_bad.c line 39 function main thread 0 ---------------------------------------------------- sum=+NaN (01111111100000000000000000000001) State 67 file other/fevs-mean/mean_bad.c line 37 function main thread 0 ---------------------------------------------------- i=11 (00000000000000000000000000001011) Violated property: file other/fevs-mean/mean_bad.c line 41 function main assertion sum/10 == (float)x FALSE VERIFICATION FAILED ############################################################################### ### exit code: 10 ### /usr/bin/time -v: Command exited with non-zero status 10 Command being timed: "cbmc /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/fevs-mean/mean_bad.0.0.i" User time (seconds): 2.01 System time (seconds): 0.04 Percent of CPU this job got: 95% Elapsed (wall clock) time (h:mm:ss or m:ss): 0:02.15 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 66152 Average resident set size (kbytes): 0 Major (requiring I/O) page faults: 1 Minor (reclaiming a frame) page faults: 22368 Voluntary context switches: 5 Involuntary context switches: 6 Swaps: 0 File system inputs: 96 File system outputs: 16 Socket messages sent: 0 Socket messages received: 0 Signals delivered: 0 Page size (bytes): 4096 Exit status: 10