Tool 2LS 0.5.0 BLAST 2.7.3 CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux SMACK+Corral 1.7.2 symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a ULTIMATE Automizer f7c3ed31 ULTIMATE Kojak f7c3ed31 ULTIMATE Taipan f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS [Linux 4.4.0-59-generic; Linux 4.4.0-57-generic] Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution [2017-01-11 09:48:02 CET [[ 2017-01-14 21:34:09 CET ]] [[ 2017-01-14 21:49:16 CET ]] [[ 2017-01-14 21:34:25 CET ]] [[ 2017-01-14 21:52:20 CET ]]; 2017-01-11 11:02:28 CET [[ 2017-01-14 22:09:21 CET ]] [[ 2017-01-14 22:27:59 CET ]] [[ 2017-01-14 22:12:16 CET ]] [[ 2017-01-14 22:31:32 CET ]]; 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]]] [2017-01-11 10:12:01 CET [[ 2017-01-14 21:12:06 CET ]] [[ 2017-01-14 21:17:30 CET ]] [[ 2017-01-14 21:14:22 CET ]] [[ 2017-01-14 21:21:19 CET ]]; 2017-01-11 10:41:01 CET [[ 2017-01-14 21:37:14 CET ]] [[ 2017-01-14 21:52:04 CET ]]; 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:51:44 CET ]] [[ 2017-01-14 18:06:48 CET ]] [[ 2017-01-14 19:59:41 CET ]]] [2017-01-11 10:20:18 CET [[ 2017-01-14 21:14:41 CET ]] [[ 2017-01-14 21:35:33 CET ]] [[ 2017-01-14 21:19:46 CET ]] [[ 2017-01-14 21:37:38 CET ]]; 2017-01-11 13:54:34 CET [[ 2017-01-14 21:55:46 CET ]] [[ 2017-01-14 22:15:53 CET ]] [[ 2017-01-14 21:57:58 CET ]] [[ 2017-01-14 22:18:07 CET ]]; 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]]] [2017-01-11 09:49:51 CET [[ 2017-01-14 20:52:01 CET ]] [[ 2017-01-14 21:02:28 CET ]] [[ 2017-01-14 20:57:34 CET ]] [[ 2017-01-14 21:06:31 CET ]]; 2017-01-11 10:43:25 CET [[ 2017-01-14 21:26:44 CET ]] [[ 2017-01-14 21:28:35 CET ]] [[ 2017-01-14 21:27:51 CET ]] [[ 2017-01-14 21:29:04 CET ]]; 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]]] [2017-01-11 10:43:32 CET [[ 2017-01-14 21:41:35 CET ]] [[ 2017-01-14 21:45:05 CET ]] [[ 2017-01-14 21:43:06 CET ]] [[ 2017-01-14 21:46:49 CET ]]; 2017-01-11 11:20:09 CET [[ 2017-01-14 21:49:20 CET ]] [[ 2017-01-14 22:06:43 CET ]] [[ 2017-01-14 21:51:07 CET ]] [[ 2017-01-14 22:08:18 CET ]]; 2017-01-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]]] [2017-01-13 04:38:11 CET [[ 2017-01-14 23:48:17 CET ]] [[ 2017-01-14 23:57:43 CET ]] [[ 2017-01-14 23:52:59 CET ]] [[ 2017-01-15 00:03:21 CET ]]; 2017-01-13 07:44:08 CET [[ 2017-01-15 00:24:53 CET ]] [[ 2017-01-15 00:50:42 CET ]] [[ 2017-01-15 00:30:44 CET ]] [[ 2017-01-15 00:56:39 CET ]]; 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]]] [2017-01-13 04:51:53 CET [[ 2017-01-15 00:05:22 CET ]] [[ 2017-01-15 00:31:32 CET ]] [[ 2017-01-15 00:11:25 CET ]] [[ 2017-01-15 00:39:18 CET ]]; 2017-01-13 09:01:17 CET [[ 2017-01-15 01:00:51 CET ]] [[ 2017-01-15 01:12:27 CET ]] [[ 2017-01-15 01:06:42 CET ]] [[ 2017-01-15 01:18:39 CET ]]; 2017-01-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]]] [2017-01-13 04:52:43 CET [[ 2017-01-15 00:23:14 CET ]] [[ 2017-01-15 00:35:58 CET ]] [[ 2017-01-15 00:29:47 CET ]] [[ 2017-01-15 00:40:29 CET ]]; 2017-01-13 08:09:41 CET [[ 2017-01-15 00:46:31 CET ]] [[ 2017-01-15 01:12:25 CET ]] [[ 2017-01-15 00:52:40 CET ]] [[ 2017-01-15 01:18:42 CET ]]; 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]] [2017-01-13 05:20:12 CET [[ 2017-01-15 00:51:08 CET ]] [[ 2017-01-15 01:00:54 CET ]] [[ 2017-01-15 00:55:05 CET ]] [[ 2017-01-15 01:06:26 CET ]]; 2017-01-13 08:59:26 CET [[ 2017-01-15 01:13:08 CET ]] [[ 2017-01-15 01:19:20 CET ]] [[ 2017-01-15 01:18:26 CET ]] [[ 2017-01-15 01:22:10 CET ]]; 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]] [2017-01-13 05:51:33 CET [[ 2017-01-15 01:19:13 CET ]] [[ 2017-01-15 01:22:10 CET ]] [[ 2017-01-15 01:20:47 CET ]] [[ 2017-01-15 01:23:25 CET ]]; 2017-01-13 09:24:14 CET [[ 2017-01-15 01:24:24 CET ]] [[ 2017-01-15 01:40:44 CET ]] [[ 2017-01-15 01:25:54 CET ]] [[ 2017-01-15 01:44:51 CET ]]; 2017-01-11 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]]] [2017-01-13 06:35:22 CET [[ 2017-01-15 01:30:25 CET ]] [[ 2017-01-15 01:30:43 CET ]] [[ 2017-01-15 01:30:33 CET ]] [[ 2017-01-15 01:30:54 CET ]]; 2017-01-13 09:57:49 CET [[ 2017-01-15 01:31:06 CET ]] [[ 2017-01-15 01:47:27 CET ]] [[ 2017-01-15 01:32:35 CET ]] [[ 2017-01-15 01:49:35 CET ]]; 2017-01-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]]] [2017-01-14 05:56:27 CET [[ 2017-01-15 04:08:20 CET ]] [[ 2017-01-15 04:18:47 CET ]] [[ 2017-01-15 04:12:29 CET ]] [[ 2017-01-15 04:25:58 CET ]]; 2017-01-14 07:19:02 CET [[ 2017-01-15 04:32:52 CET ]] [[ 2017-01-15 05:00:11 CET ]] [[ 2017-01-15 04:38:10 CET ]] [[ 2017-01-15 05:08:13 CET ]]; 2017-01-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]]] [2017-01-14 11:37:51 CET [[ 2017-01-15 04:18:56 CET ]] [[ 2017-01-15 04:38:06 CET ]] [[ 2017-01-15 04:27:27 CET ]] [[ 2017-01-15 04:45:45 CET ]]; 2017-01-14 13:43:12 CET [[ 2017-01-15 05:08:16 CET ]] [[ 2017-01-15 05:40:54 CET ]] [[ 2017-01-15 05:24:54 CET ]] [[ 2017-01-15 05:42:22 CET ]]; 2017-01-13 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]]] [2017-01-14 06:16:04 CET [[ 2017-01-15 05:34:44 CET ]] [[ 2017-01-15 05:49:53 CET ]] [[ 2017-01-15 05:35:06 CET ]] [[ 2017-01-15 05:51:11 CET ]]; 2017-01-14 07:34:03 CET [[ 2017-01-15 06:02:28 CET ]] [[ 2017-01-15 06:17:25 CET ]] [[ 2017-01-15 06:02:42 CET ]] [[ 2017-01-15 06:18:28 CET ]]; 2017-01-13 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]]] [2017-01-14 06:29:29 CET [[ 2017-01-15 05:44:30 CET ]] [[ 2017-01-15 05:59:35 CET ]] [[ 2017-01-15 05:44:48 CET ]] [[ 2017-01-15 06:00:32 CET ]]; 2017-01-14 07:32:15 CET [[ 2017-01-15 06:03:36 CET ]] [[ 2017-01-15 06:19:08 CET ]] [[ 2017-01-15 06:04:26 CET ]] [[ 2017-01-15 06:20:07 CET ]]; 2017-01-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]]] [2017-01-14 16:15:06 CET [[ 2017-01-15 05:45:52 CET ]] [[ 2017-01-15 06:00:59 CET ]] [[ 2017-01-15 05:46:10 CET ]] [[ 2017-01-15 06:02:27 CET ]]; 2017-01-14 16:52:13 CET [[ 2017-01-15 06:05:33 CET ]] [[ 2017-01-15 06:20:29 CET ]] [[ 2017-01-15 06:05:48 CET ]] [[ 2017-01-15 06:21:18 CET ]]; 2017-01-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]]]
Run set 2ls.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] blast.[sv-comp17; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] cbmc.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] ceagle.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] cpa-kind.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] depthk.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] esbmc.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] esbmc-falsi.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] esbmc-incr.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] esbmc-kind.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] smack.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] symbiotic4.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] uautomizer.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] ukojak.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] utaipan.[sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety]
Options [--graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [-alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-11_1012.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-11_1012.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-11_1012.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-11_1012.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-11_1041.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-11_1041.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [--graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1354.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [--compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [-sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [-sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [ [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0901.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0901.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0901.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0901.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [-s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [-s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [-s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0924.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [-s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0957.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [-w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [--witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1343.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [ [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [ [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]] [ [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]]
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_false-valid-deref.i valid-deref valid-free valid-memtrack error (8) .35  32 3.0  unknown .067 9.2 .65 false(valid-deref) 9.1  690 110   unknown .052 8.4  .57  error (1) .41 38 4.2 error 4.2 280 34 unknown 890   1200 7100 out of memory 360    15000 3400   timeout 900     530 6600    timeout 900     550 6200    unknown .19  28 1.8  timeout 880    290   11000   false(valid-deref) 1.3  64   13   error 44   820 360 error 760   1400 10000 error 80   1200 740
busybox-1.22.0/head_true-no-overflow_false-valid-deref.i valid-deref valid-free valid-memtrack error (8) 11     1100 120    unknown .082 11   .48 error (1) 3.4  65 41   unknown .11  9.2  1.2   error (1) .40 38 3.4 error 3.5 260 27 unknown 900   2900 10000 out of memory 820    15000 7500   timeout 900     5300 7000    timeout 900     5400 7400    unknown .21  34 2.3  timeout 900    7.5 12000   false(valid-deref) 22    1500   230   unknown 5.4 310 42 unknown 5.8 310 49 unknown 5.4 310 43
busybox-1.22.0/sleep_true-no-overflow_false-valid-deref.i valid-deref valid-free valid-memtrack error (8) 1.7   180 19    unknown .050 7.9 .41 error (1) 1.0  36 11   unknown .057 9.8  .48  error (1) .43 37 3.2 error 3.4 260 28 unknown 900   2500 12000 out of memory 250    15000 3400   timeout 900     1800 12000    timeout 900     1800 12000    unknown .23  32 2.3  false(valid-deref) 7.7  130   98   unknown 5.2  700   64   unknown 5.9 330 47 unknown 5.4 310 43 unknown 5.9 310 45
busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i valid-deref valid-free valid-memtrack error (8) .45  48 4.9  unknown .052 8.0 .46 error (1) .38 29 4.4 unknown .065 9.0  .69  error (1) .41 40 4.3 error 3.7 270 28 unknown 900   2800 5400 out of memory 730    15000 6900   timeout 900     2000 6500    timeout 900     2000 5500    unknown .20  31 2.4  false(valid-memtrack) 840    400   8400   false(valid-memtrack) 1.9  200   25   unknown 5.4 310 42 unknown 5.9 310 43 unknown 5.9 310 40
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .32  38 3.4  unknown .079 9.3 .45 error (42) 850    5300 6200   unknown .058 8.7  .48  error (1) .40 38 3.7 error 4.1 270 33 unknown 890   1300 8600 out of memory 390    15000 3400   timeout 900     500 6600    timeout 900     540 6500    unknown .16  28 2.1  timeout 880    230   12000   timeout (timeout) 900    1100   12000   error 110   1700 950 timeout 900   1800 12000 error 150   3300 1600
busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 1.0   110 11    unknown .050 8.0 .45 error (1) .58 30 5.2 unknown .074 8.9  .72  error (1) .38 37 3.9 error 3.7 270 30 unknown 900   870 11000 out of memory 900    15000 6600   unknown 3.9   100 47    unknown 3.9   110 51    unknown .23  32 2.1  false(valid-deref) 530    310   6400   timeout (timeout) 900    1700   9200   unknown 5.2 310 41 unknown 5.4 310 40 unknown 6.6 350 51
busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack timeout 900     1300 11000    unknown .081 9.3 .41 error (1) 6.2  110 84   unknown .17  9.9  1.7   error (1) .41 41 4.4 error 3.9 270 30 unknown 44   46 470 unknown .36 38 4.9 unknown .23  38 1.8  unknown .22  38 1.9  unknown .21  37 1.8  timeout 900    7.5 12000   false(valid-deref) 26    3500   280   unknown 5.7 310 44 unknown 6.0 320 47 unknown 6.1 320 51
busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 12     990 150    unknown .079 9.2 .49 error (1) 2.8  210 34   unknown .16  10    1.8   error (1) .40 40 4.4 error 4.0 270 32 unknown 48   48 660 unknown .39 41 4.1 unknown .22  41 2.0  unknown .23  40 2.2  unknown .21  40 1.9  timeout 900    9.4 11000   false(valid-deref) 85    6800   1200   unknown 5.6 310 44 unknown 6.7 340 54 unknown 5.7 310 48
busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .28  31 3.4  unknown .049 8.2 .47 error (134) 350    14000 4800   unknown .052 8.6  .47  error (1) .42 38 3.7 error 3.1 230 27 unknown 890   970 7900 out of memory 110    15000 1200   timeout 900     330 11000    timeout 900     310 7400    unknown .20  28 2.0  true 880    330   7500   timeout (timeout) 900    2300   10000   timeout 900   2600 7800 timeout 900   2900 12000 timeout 900   870 7000
busybox-1.22.0/du_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (5) 8.7   66 91    unknown .056 8.0 .45 error (1) 20    150 260   unknown .27  46    2.5   error (1) .43 40 4.6 error 15   270 19 unknown 45   46 650 unknown .40 39 3.8 unknown .21  38 2.2  unknown .19  38 2.2  unknown .22  38 2.3  timeout 880    3400   11000   false(valid-deref) 29    3400   370   unknown 6.6 340 48 unknown 6.1 320 44 unknown 6.8 340 54
busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .96  97 8.9  unknown .063 9.4 .47 error (134) 53    13000 650   unknown .073 8.8  .75  error (1) .44 40 3.6 error 3.5 270 29 unknown 890   750 9900 out of memory 110    15000 1200   timeout 900     2200 10000    timeout 900     2200 10000    unknown .18  32 2.1  timeout 880    480   8700   timeout (timeout) 900    1600   10000   unknown 6.1 330 47 unknown 5.9 310 44 unknown 5.5 310 39
busybox-1.22.0/expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 72     2500 490    unknown .077 10   .49 error (1) 22    140 240   unknown .21  9.7  2.6   error (1) .40 37 3.8 error 16   270 20 unknown 45   49 540 unknown .37 39 4.0 unknown .19  39 2.7  unknown .21  39 2.0  unknown .22  39 2.1  timeout 900    7.7 10000   false(valid-deref) 130    6300   1500   unknown 5.8 310 49 unknown 5.8 330 46 unknown 5.7 310 48
busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack timeout 900     760 11000    unknown .081 9.0 .42 error (1) 4.2  66 54   unknown .13  9.8  1.4   error (1) .40 37 3.9 error 3.9 280 32 unknown 42   44 510 unknown .35 37 3.7 unknown .68  37 1.4  unknown .21  36 2.3  unknown .24  36 1.8  timeout 900    7.5 11000   false(valid-deref) 67    2500   710   unknown 5.8 310 47 unknown 6.3 330 47 unknown 5.4 310 43
busybox-1.22.0/hostid_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .26  34 2.2  unknown .060 9.1 .50 error (134) 340    14000 3800   unknown .053 8.7  .42  error (1) .39 37 3.5 error 3.2 260 24 unknown 890   1100 6500 out of memory 67    15000 620   timeout 900     380 7500    timeout 900     400 6900    timeout 900     570 7700    true 880    320   7600   timeout (timeout) 900    2300   9700   timeout 900   1300 13000 timeout 900   1600 13000 timeout 900   5800 11000
busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .43  40 4.0  unknown .080 9.2 .45 error (1) .32 29 3.1 unknown .068 9.2  .55  error (1) .42 37 4.1 error 3.7 270 29 unknown 900   920 12000 out of memory 830    15000 7100   unknown 1.6   67 19    unknown 1.7   74 20    unknown .18  31 2.3  true 880    330   8600   false(valid-deref) 120    420   1500   unknown 5.4 300 46 unknown 6.2 340 46 unknown 5.6 320 42
busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (5) 740     330 3700    unknown .047 8.1 .54 error (1) 25    180 260   unknown .67  22    8.2   error (1) .40 37 3.9 error 4.8 280 39 unknown 58   59 630 unknown .49 51 4.4 unknown .26  51 2.2  unknown .23  51 2.7  unknown .24  51 2.8  timeout 880    3600   11000   timeout (timeout) 900    380   9400   error 9.9 310 78 error 11   310 75 error 11   320 76
busybox-1.22.0/mkdir_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack timeout 900     370 12000    unknown .048 8.0 .55 error (1) 2.4  190 32   unknown .12  9.7  1.3   error (1) .41 38 3.7 error 4.0 270 33 unknown 43   46 530 unknown .36 38 4.3 unknown .18  38 2.1  unknown .20  38 2.2  unknown .21  38 1.9  timeout 900    7.4 13000   false(valid-deref) 20    2400   260   unknown 5.9 310 46 unknown 5.7 310 43 unknown 6.3 330 45
busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .42  45 4.0  unknown .079 9.4 .45 error (1) .41 30 3.6 unknown .064 9.2  .58  error (1) .42 37 3.7 error 3.5 260 30 unknown 900   3000 11000 timeout 900    15000 6000   unknown 670     520 9400    unknown 670     520 8900    unknown .20  30 2.4  timeout 880    300   11000   false(valid-memtrack) 110    340   1200   unknown 5.7 320 41 unknown 5.4 310 41 unknown 5.6 310 40
busybox-1.22.0/od_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack timeout 900     270 3100    unknown .048 8.2 .57 error (1) 16    140 230   unknown .091 10    .86  error (1) .45 38 4.3 error 4.6 280 37 unknown 61   56 760 unknown .51 48 4.9 unknown .26  48 3.1  unknown .26  48 2.5  unknown .28  48 2.8  timeout 900    7.6 12000   out of memory 190    15000   2300   unknown 6.2 320 43 unknown 6.8 330 49 unknown 6.8 340 48
busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 58     880 420    unknown .049 8.1 .46 error (1) 20    130 230   unknown .076 9.9  .46  error (1) .48 37 3.4 error 3.9 270 36 unknown 900   2600 10000 timeout 900    760 13000   timeout 900     4800 9100    timeout 900     4800 9200    unknown .24  37 2.8  timeout 880    550   7300   unknown 32    3000   410   unknown 6.5 340 49 unknown 5.6 320 49 unknown 5.8 310 43
busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 4.5   360 50    unknown .061 8.1 .37 error (1) .89 43 11   unknown .14  46    1.5   error (1) .40 40 4.2 error 3.8 270 32 unknown 40   43 480 unknown .35 35 3.8 unknown .18  35 1.9  unknown .18  35 1.7  unknown .20  35 1.9  true 880    730   7900   timeout (timeout) 900    2000   9500   unknown 6.4 350 52 unknown 5.5 310 44 unknown 6.6 350 52
busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .49  51 4.9  unknown .081 9.1 .56 error (1) .41 31 3.8 unknown .071 9.0  .59  error (1) .43 40 3.7 error 3.6 270 27 unknown 900   3900 12000 out of memory 810    15000 6300   unknown 670     780 8800    unknown 660     780 9000    unknown .19  31 2.3  timeout 880    320   12000   false(valid-memtrack) 440    780   3300   unknown 5.3 310 39 unknown 5.3 310 45 unknown 6.0 330 45
busybox-1.22.0/rm_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (5) 8.6   64 85    unknown .049 8.1 .49 error (1) 33    150 370   unknown .21  11    2.2   error (1) .42 40 4.3 error 3.9 270 35 unknown 43   46 570 unknown .36 38 4.6 unknown .20  38 2.0  unknown .23  38 1.9  unknown .21  38 1.8  true 880    740   7600   false(valid-deref) 470    3000   5000   unknown 5.9 320 43 unknown 5.4 310 45 unknown 5.9 310 45
busybox-1.22.0/seq_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 3.2   260 37    unknown .046 8.1 .59 error (1) .84 53 9.2 unknown .10  9.5  .46  error (1) .46 40 3.6 error 15   260 17 unknown 39   43 520 unknown .32 35 3.3 unknown .20  35 1.8  unknown .20  35 2.1  unknown .17  35 2.2  timeout 900    7.4 12000   unknown 16    1900   190   error 9.6 340 88 error 9.3 310 72 error 9.9 330 76
busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 200     4700 1500    unknown .048 8.1 .47 error (1) 40    180 460   unknown .36  47    4.3   error (1) .42 40 4.0 error 4.9 290 42 unknown 900   1100 2000 out of memory 17    15000 200   timeout 900     4500 7700    timeout 900     4600 7500    unknown .32  55 3.5  timeout 890    540   7200   timeout (timeout) 900    11000   9900   unknown 6.0 320 47 unknown 6.6 330 51 unknown 6.1 310 46
busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .41  38 4.0  unknown .046 8.2 .59 error (1) .30 27 2.9 unknown .070 8.9  .55  error (1) .43 39 3.6 error 3.2 230 27 unknown 890   1200 6000 out of memory 820    15000 6800   timeout 900     510 6200    timeout 900     510 7100    unknown .17  30 2.6  true 880    340   11000   false(valid-memtrack) 160    410   1600   unknown 5.8 320 43 unknown 5.8 310 42 unknown 5.3 310 41
busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 8.6   580 100    unknown .051 8.2 .39 error (1) 2.6  62 32   unknown .13  9.5  1.3   error (1) .39 37 4.0 error 3.7 270 28 unknown 40   44 480 unknown .33 36 3.9 unknown .65  35 1.4  unknown .17  35 1.8  unknown .17  35 1.9  timeout 880    570   8900   false(valid-memtrack) 58    2000   700   unknown 5.4 310 41 unknown 5.9 310 43 unknown 6.1 330 47
busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 5.3   470 59    unknown .049 8.1 .51 error (1) 1.2  51 14   unknown .18  45    1.4   error (1) .42 38 3.9 error 3.8 270 30 unknown 40   43 490 unknown .34 36 4.6 unknown .17  35 2.0  unknown .17  36 2.0  unknown .19  36 2.2  timeout 880    3300   11000   timeout (timeout) 900    2400   8700   unknown 5.8 310 39 unknown 5.6 310 43 unknown 5.7 310 40
busybox-1.22.0/test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (5) 62     120 430    unknown .080 9.1 .47 error (1) 18    150 250   unknown 5.6   190    63     error (1) .42 38 3.7 error 3.9 270 27 unknown 890   1500 5700 out of memory 400    15000 3400   timeout 900     740 6900    timeout 900     760 6600    unknown .22  38 2.6  timeout 880    440   11000   false(valid-memtrack) 3.4  350   41   unknown 6.0 330 44 unknown 6.5 340 50 unknown 5.6 310 41
busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 10     810 110    unknown .047 8.3 .47 error (1) 2.7  190 37   unknown .15  9.9  1.8   error (1) .39 37 3.6 error 4.2 280 33 unknown 45   47 550 unknown .37 39 4.2 unknown .21  39 2.5  unknown .22  39 1.9  unknown .23  39 1.9  timeout 900    7.4 12000   false(valid-deref) 38    5000   460   unknown 6.5 330 51 unknown 5.8 320 48 unknown 5.8 310 41
busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 2.9   280 32    unknown .069 9.3 .57 error (1) 1.2  190 14   unknown .10  9.2  1.2   error (1) .45 38 3.8 error 3.8 270 33 unknown 40   43 540 unknown .34 35 4.2 unknown .19  35 2.1  unknown .65  35 2.0  unknown .18  35 2.1  true 880    730   9000   timeout (timeout) 900    3400   8500   unknown 5.4 310 46 unknown 5.8 310 41 unknown 5.6 310 46
busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 8.3   700 99    unknown .080 8.6 .47 error (1) 2.0  54 24   unknown .13  9.5  1.5   error (1) .42 37 3.9 error 4.0 270 33 unknown 170   44 390 unknown .33 36 4.7 unknown .21  36 2.1  unknown .19  36 1.8  unknown .18  36 2.0  timeout 900    7.4 13000   false(valid-deref) 24    2500   280   unknown 6.2 330 47 unknown 5.8 320 49 unknown 5.6 330 44
busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .77  78 8.1  unknown .082 8.0 .37 error (1) .35 29 3.2 unknown .11  45    1.1   error (1) .41 37 3.8 error 3.4 260 29 unknown 890   1300 5400 out of memory 270    15000 3300   timeout 900     600 7900    timeout 900     610 6300    unknown .18  31 2.3  timeout 880    390   10000   timeout (timeout) 900    1900   11000   unknown 5.7 300 46 unknown 6.0 350 51 unknown 5.5 310 45
busybox-1.22.0/uudecode_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 18     1500 190    unknown .079 9.6 .51 error (1) 5.8  110 76   unknown .16  10    1.5   error (1) .39 38 3.6 error 4.0 270 36 unknown 46   50 600 unknown .41 40 3.9 unknown .22  40 2.0  unknown .23  40 2.3  unknown .20  40 1.9  timeout 900    7.4 13000   false(valid-deref) 50    5200   550   unknown 5.7 320 44 unknown 5.8 320 50 unknown 5.8 320 44
busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack timeout 900     440 9400    unknown .048 8.1 .53 error (1) 2.6  65 31   unknown .12  9.3  1.2   error (1) .40 37 3.4 error 3.8 270 32 unknown 41   44 500 unknown .37 36 3.7 unknown .18  36 2.0  unknown .18  36 2.2  unknown .17  36 2.3  true 880    800   8400   timeout (timeout) 900    3800   8700   unknown 6.3 330 43 unknown 5.9 310 45 unknown 5.5 310 44
busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) 3.4   300 39    unknown .049 8.1 .49 error (1) .86 41 9.4 unknown .11  9.3  1.1   error (1) .42 38 3.8 error 4.1 270 33 unknown 40   45 520 unknown .37 36 3.5 unknown .19  36 2.1  unknown .20  36 2.1  unknown .18  36 1.8  timeout 880    630   6400   timeout (timeout) 900    2100   7200   unknown 6.1 320 49 unknown 5.4 310 38 unknown 6.2 330 50
busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .43  39 3.8  unknown .084 9.1 .54 error (134) 340    14000 3900   unknown .071 9.4  .67  error (1) .42 40 4.0 error 3.5 270 30 unknown 900   1200 2000 out of memory 900    15000 7600   timeout 900     450 6100    timeout 900     450 8100    unknown .20  31 2.3  true 880    360   8000   timeout (timeout) 900    2300   10000   unknown 5.6 320 46 unknown 5.4 310 38 unknown 5.4 310 48
busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (8) .45  46 4.5  unknown .068 8.2 .35 error (1) .38 33 3.0 unknown .063 8.8  .55  error (1) .40 38 4.0 error 3.3 260 27 unknown 900   490 2000 out of memory 560    15000 5600   unknown 2.1   81 27    unknown 2.2   88 31    unknown .18  31 2.0  true 830    370   8000   false(valid-deref) 110    470   1300   unknown 6.1 330 45 unknown 5.5 330 43 unknown 5.7 320 39
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_false-valid-deref.i no-overflow error (8) .27  32 2.6  exception (gremlins) .073 11   .42 error (42) 850    4900 7200   unknown .019 .89 .026 error 5.0  280 40   error 4.4 280 37 unknown 890   1100 7800 out of memory 680    15000 6200   timeout 900     400 11000    timeout 900     420 11000    unknown .16  28 1.9  timeout 880    540   7400   timeout (timeout) 900    260   12000   timeout 900   5500 12000 timeout 900   4600 12000 timeout 900   2400 9500
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .28  32 2.2  exception (gremlins) .054 11   .47 error (42) 850    5000 5600   unknown .015 1.0  .032 error 4.8  280 36   error 4.7 290 37 unknown 890   1100 6600 out of memory 650    15000 5300   timeout 900     420 12000    timeout 900     400 10000    unknown .16  28 1.6  timeout 880    840   8600   timeout (timeout) 900    260   11000   timeout 900   5500 12000 timeout 900   5100 15000 timeout 900   2400 9500
busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i no-overflow error (8) .33  37 2.7  exception (gremlins) .061 11   .48 error (1) .35 29 3.7 unknown .022 .91 .044 error 5.2  280 43   error 5.3 280 45 unknown 900   2500 5600 out of memory 620    15000 6100   timeout 900     1100 8200    timeout 900     1200 7100    unknown .18  31 2.3  true 880    440   9600   timeout (timeout) 900    370   11000   unknown 6.2 330 51 unknown 5.9 330 45 unknown 6.1 320 48
busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .51  72 5.0  exception (gremlins) .071 11   .45 error (1) .47 31 6.0 unknown .016 .88 .051 error 5.7  330 46   error 5.2 280 42 unknown 900   930 12000 out of memory 820    15000 5800   unknown 3.4   89 42    unknown 3.4   93 40    unknown .19  32 2.5  true 880    480   7500   timeout (timeout) 900    490   12000   unknown 5.4 310 40 unknown 5.3 310 46 unknown 5.8 320 42
busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow timeout 900     910 12000    exception (gremlins) .077 11   .51 error (1) 4.9  96 51   unknown .015 .91 .069 error 7.1  450 54   error 7.2 430 56 unknown 48   500 680 unknown .38 38 4.0 unknown .23  37 2.2  unknown .19  37 2.1  unknown .19  38 2.0  true 880    620   7500   timeout (timeout) 900    280   10000   unknown 5.5 310 42 unknown 5.6 310 48 unknown 6.5 340 49
busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 2.8   620 30    exception (gremlins) .087 15   .50 error (1) 2.3  200 26   unknown .018 .85 .067 error 7.1  460 57   error 7.5 440 60 unknown 51   500 580 unknown .38 41 4.5 unknown .22  40 2.3  unknown .22  40 2.5  unknown .20  40 2.6  timeout 880    800   7600   false(no-overflow) 1.3  81   14   unknown 5.8 310 46 unknown 6.2 330 48 unknown 6.2 330 44
busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .25  31 2.1  exception (gremlins) .084 13   .49 error (134) 320    14000 3900   unknown .016 1.0  .034 error 4.7  270 35   error 4.4 280 34 unknown 890   790 7900 out of memory 130    15000 1300   out of memory 290     15000 3100    timeout 900     310 7200    unknown .16  28 1.8  true 880    630   10000   timeout (timeout) 900    1400   11000   error (1) 160   1100 1500 error (1) 190   11000 2100 error (1) 400   1100 3000
busybox-1.22.0/du_true-no-overflow_true-valid-memsafety.i no-overflow error (5) 1.1   44 12    exception (gremlins) .074 11   .50 error (1) 16    140 160   unknown .014 1.0  .071 error 7.0  450 56   error 6.6 420 54 unknown 46   500 500 unknown .38 38 4.1 unknown .20  39 2.5  unknown .21  39 2.2  unknown .20  38 1.8  timeout 880    3400   9500   error 8.1  67   85   unknown 6.2 330 46 unknown 5.7 320 46 unknown 5.8 310 49
busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .46  51 3.7  exception (gremlins) .083 14   .47 error (42) 850    7300 5800   unknown .014 1.0  .071 error 5.8  290 43   error 5.4 290 48 unknown 890   700 11000 out of memory 150    15000 1900   timeout 900     2100 9900    timeout 900     2100 11000    unknown .18  32 2.0  timeout 880    570   8000   timeout (timeout) 900    470   10000   unknown 5.4 310 42 unknown 5.2 310 36 unknown 5.8 310 42
busybox-1.22.0/expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 10     1600 140    exception (gremlins) .089 12   .46 error (1) 17    130 200   unknown .021 1.0  .062 error 7.9  440 63   error 7.8 440 57 unknown 61   930 710 unknown .39 39 4.7 unknown .22  39 2.0  unknown .22  39 2.0  unknown .23  39 2.3  true 880    550   7900   timeout (timeout) 900    420   10000   unknown 5.8 320 47 unknown 5.4 310 47 unknown 5.7 310 47
busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i no-overflow timeout 900     470 9700    exception (gremlins) .055 12   .45 error (1) 3.2  60 40   unknown .015 1.0  .081 error 7.7  460 59   error 6.4 430 54 unknown 46   550 570 unknown .35 37 4.3 unknown .19  36 2.1  unknown .21  36 2.2  unknown .18  36 2.5  timeout 880    620   7100   timeout (timeout) 900    360   13000   unknown 5.6 320 43 unknown 5.9 320 43 unknown 5.8 310 49
busybox-1.22.0/head_true-no-overflow_false-valid-deref.i no-overflow error (8) 3.6   750 43    exception (gremlins) .087 10   .45 error (1) 2.8  60 39   unknown .015 .77 .056 error 6.0  340 48   error 6.2 350 46 unknown 900   2400 13000 out of memory 700    15000 5700   timeout 900     4600 8100    timeout 900     4700 7300    unknown .23  34 2.1  true 880    400   10000   timeout (timeout) 900    330   12000   unknown 5.3 310 41 unknown 6.3 340 49 unknown 5.7 320 47
busybox-1.22.0/hostid_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .24  34 1.8  exception (gremlins) .089 11   .51 error (134) 320    14000 4100   unknown .014 1.0  .048 error 4.8  280 34   error 4.6 280 39 unknown 900   930 6400 out of memory 65    15000 680   out of memory 180     15000 1700    timeout 900     280 10000    timeout 900     370 12000    true 880    650   12000   timeout (timeout) 900    1100   13000   true 10   380 70 true 15   500 110 true 10   380 74
busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .33  37 3.0  exception (gremlins) .051 10   .50 error (1) .30 29 2.9 unknown .015 .91 .065 error 5.2  280 42   error 5.4 280 44 unknown 900   1000 11000 out of memory 770    15000 5400   unknown 1.2   55 13    unknown 1.3   59 16    unknown .18  31 2.2  true 880    440   10000   timeout (timeout) 900    270   11000   unknown 6.4 330 50 unknown 5.4 310 42 unknown 5.8 320 43
busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (5) 55     160 340    exception (gremlins) .050 13   .65 error (1) 19    150 210   unknown .021 1.1  .068 error 8.6  500 80   error 8.9 490 76 unknown 58   59 780 unknown .47 51 4.4 unknown .26  51 2.2  unknown .24  51 2.4  unknown .22  51 2.6  timeout 880    3500   9600   error 220    180   2600   error (1) 6.1 320 53 error (1) 6.0 320 45 error (1) 5.8 310 48
busybox-1.22.0/mkdir_true-no-overflow_true-valid-memsafety.i no-overflow timeout 900     220 12000    exception (gremlins) .085 13   .55 error (1) 1.9  180 23   unknown .012 .85 .057 error 6.9  470 59   error 7.1 460 54 unknown 47   510 580 unknown .38 38 3.8 unknown .21  38 2.0  unknown .18  38 2.5  unknown .18  38 2.5  true 880    560   7200   timeout (timeout) 900    910   8200   unknown 6.0 310 42 unknown 6.0 310 42 unknown 5.7 310 43
busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .31  36 3.3  exception (gremlins) .051 10   .58 error (1) .37 29 3.0 unknown .016 1.0  .052 error 5.1  280 40   error 5.1 280 40 unknown 900   1200 11000 out of memory 840    15000 6600   unknown 550     280 8100    unknown 540     290 6000    unknown .21  30 1.8  true 880    440   11000   timeout (timeout) 900    450   11000   unknown 6.0 320 39 unknown 5.3 300 41 unknown 6.2 340 42
busybox-1.22.0/od_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow out of memory 260     15000 1500    exception (gremlins) .085 11   .47 error (1) 13    120 130   unknown .013 1.0  .058 error 11    640 86   error 11   550 92 unknown 63   1700 900 unknown .48 48 4.7 unknown .26  48 3.1  unknown .28  48 2.6  unknown .28  48 2.5  error (1) 1.2  63   17   true 1.5  120   16   unknown 7.5 340 48 unknown 6.3 310 50 unknown 6.2 320 44
busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 6.3   890 72    exception (gremlins) .081 11   .48 error (1) 15    120 210   unknown .011 .88 .049 error 6.8  440 58   error 7.1 430 60 unknown 900   1900 12000 timeout 900    770 11000   timeout 900     3900 7700    timeout 900     3900 9700    unknown .25  37 2.2  error (1) .66 41   7.7 unknown .57 40   7.1 unknown 6.2 340 46 unknown 6.5 330 53 unknown 6.9 320 51
busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 1.2   220 17    exception (gremlins) .087 11   .56 error (1) .77 40 9.9 unknown .011 .92 .050 error 6.3  400 55   error 6.4 420 53 unknown 40   43 490 unknown .35 35 3.7 unknown .20  35 2.0  unknown .18  35 2.4  unknown .21  35 2.2  true 880    420   9400   timeout (timeout) 900    1200   8200   unknown 6.4 330 54 unknown 5.8 310 46 unknown 5.6 310 45
busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .36  37 3.4  exception (gremlins) .085 11   .43 error (1) .34 30 3.7 unknown .016 1.0  .054 error 5.2  280 43   error 5.2 290 42 unknown 900   1200 10000 out of memory 750    15000 6000   unknown 540     300 7100    unknown 540     310 6800    unknown .20  31 2.5  true 880    440   7400   timeout (timeout) 900    610   11000   unknown 5.5 310 42 unknown 6.3 320 44 unknown 5.4 310 42
busybox-1.22.0/rm_true-no-overflow_true-valid-memsafety.i no-overflow error (5) 1.2   44 10    exception (gremlins) .058 10   .44 error (1) 24    130 280   unknown .016 .87 .054 error 6.8  450 60   error 7.1 460 52 unknown 45   510 550 unknown .36 38 4.9 unknown .20  38 1.9  unknown .19  38 1.9  unknown .19  38 2.0  true 880    540   6500   timeout (timeout) 900    2100   9400   unknown 5.5 310 40 unknown 5.7 320 40 unknown 5.6 310 43
busybox-1.22.0/seq_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .93  150 9.0  exception (gremlins) .056 12   .52 error (1) .73 48 7.4 unknown .016 .64 .056 error 6.6  410 54   error 6.6 410 51 unknown 42   500 470 unknown .32 35 4.4 unknown .20  35 2.2  unknown .17  35 1.9  unknown .17  35 1.9  true 880    460   7500   unknown .56 39   6.9 error (1) 6.0 310 40 error (1) 5.6 320 43 error (1) 6.0 320 41
busybox-1.22.0/sleep_true-no-overflow_false-valid-deref.i no-overflow error (8) .70  110 7.3  exception (gremlins) .089 11   .43 error (1) .89 36 11   unknown .015 .99 .080 error 5.9  330 44   error 5.7 290 46 unknown 900   1000 11000 out of memory 870    15000 8000   timeout 900     1100 12000    timeout 900     1100 11000    unknown .23  32 2.2  error (1) .55 31   7.0 unknown .42 20   5.1 unknown 6.1 330 52 unknown 6.3 330 46 unknown 5.9 320 41
busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 24     3100 210    exception (gremlins) .087 11   .44 error (1) 31    170 300   unknown .013 .93 .055 error 9.6  440 84   error 9.9 450 75 unknown 890   2000 11000 out of memory 17    15000 200   timeout 900     3900 6400    timeout 900     3900 7000    unknown .33  55 4.0  timeout 890    640   6400   error 76    110   730   unknown 6.2 320 52 unknown 6.2 330 50 unknown 6.4 320 50
busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .30  35 2.9  exception (gremlins) .085 11   .45 error (1) .30 29 2.7 unknown .016 1.1  .057 error 5.3  290 41   error 5.0 290 43 unknown 890   1000 5900 out of memory 750    15000 5400   timeout 900     310 10000    timeout 900     260 13000    unknown .17  30 1.9  true 880    450   8800   timeout (timeout) 900    270   12000   unknown 5.6 310 45 unknown 6.2 330 46 unknown 5.6 320 40
busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 2.1   360 24    exception (gremlins) .060 11   .42 error (1) 2.1  55 27   unknown .017 1.0  .049 error 6.7  430 60   error 6.7 390 47 unknown 43   500 490 unknown .32 35 3.5 unknown .19  35 1.7  unknown .20  35 2.0  unknown .18  35 1.8  timeout 880    520   8000   timeout (timeout) 900    1200   12000   unknown 5.6 320 44 unknown 5.6 310 47 unknown 6.5 350 42
busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 1.6   310 17    exception (gremlins) .051 12   .50 error (1) .98 45 10   unknown .022 1.1  .052 error 6.9  340 49   error 6.5 410 54 unknown 43   500 590 unknown .33 36 3.5 unknown .17  36 2.0  unknown .17  36 1.9  unknown .19  36 2.4  timeout 880    3400   11000   timeout (timeout) 900    730   11000   unknown 6.4 330 48 unknown 5.8 310 42 unknown 5.5 300 47
busybox-1.22.0/test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (5) 4.2   58 40    exception (gremlins) .057 12   .42 error (1) 14    130 170   unknown .014 .88 .071 error 6.3  390 56   error 7.0 400 52 unknown 890   1300 8200 out of memory 710    15000 6400   timeout 900     510 10000    timeout 900     450 10000    unknown .23  37 3.0  true 880    470   7200   timeout (timeout) 900    720   12000   unknown 5.5 300 43 unknown 5.6 310 44 unknown 5.6 310 43
busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 2.4   500 24    exception (gremlins) .052 9.1 .56 error (1) 2.2  180 27   unknown .017 .88 .061 error 7.5  420 68   error 6.8 420 58 unknown 47   500 640 unknown .36 39 4.2 unknown .19  39 2.4  unknown .21  39 1.9  unknown .20  39 2.2  timeout 880    640   8100   false(no-overflow) 210    420   2300   unknown 5.7 310 46 unknown 6.3 340 46 unknown 6.3 320 47
busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .94  160 9.1  exception (gremlins) .079 11   .51 error (1) 1.1  190 14   unknown .014 .86 .057 error 6.8  390 50   error 6.7 400 59 unknown 43   500 500 unknown .33 36 3.3 unknown .17  35 1.8  unknown .21  35 1.8  unknown .17  35 1.9  true 880    490   6200   timeout (timeout) 900    5100   7000   unknown 5.9 310 49 unknown 5.7 310 51 unknown 6.6 330 50
busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 2.2   450 25    exception (gremlins) .081 11   .53 error (1) 1.6  46 19   unknown .012 .86 .055 error 6.8  440 54   error 7.0 430 53 unknown 44   510 600 unknown .33 37 4.7 unknown .17  36 1.9  unknown .20  36 2.1  unknown .18  36 1.8  true 880    550   11000   timeout (timeout) 900    310   9800   unknown 6.2 330 46 unknown 5.6 320 48 unknown 5.9 320 48
busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .43  51 3.5  exception (gremlins) .083 12   .51 error (1) .32 29 2.8 unknown .016 .95 .055 error 5.2  290 41   error 5.2 280 47 unknown 890   1200 6200 out of memory 300    15000 3600   timeout 900     300 10000    timeout 900     290 9900    unknown .20  31 2.0  true 880    1200   10000   timeout (timeout) 900    220   10000   unknown 6.1 350 45 unknown 5.4 310 36 unknown 5.2 300 41
busybox-1.22.0/uudecode_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 4.5   980 46    exception (gremlins) .080 12   .44 error (1) 4.6  100 47   unknown .014 .79 .062 error 7.2  460 55   error 8.0 430 55 unknown 51   500 700 unknown .39 40 3.6 unknown .23  40 2.1  unknown .20  40 2.1  unknown .21  40 2.6  timeout 880    1200   8000   timeout (timeout) 900    620   11000   unknown 5.6 310 45 unknown 5.7 310 49 unknown 5.7 310 48
busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow timeout 900     270 11000    exception (gremlins) .078 9.7 .53 error (1) 2.0  58 24   unknown .015 .89 .050 error 6.4  450 46   error 7.1 420 54 unknown 44   500 550 unknown .36 36 3.2 unknown .19  36 2.0  unknown .20  36 1.9  unknown .21  36 2.1  true 880    500   7400   timeout (timeout) 900    2600   11000   unknown 5.4 310 43 unknown 6.0 320 51 unknown 5.8 300 45
busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i no-overflow error (8) 1.0   170 12    exception (gremlins) .090 12   .47 error (1) .72 42 7.8 unknown .015 .80 .065 error 6.5  420 54   error 6.0 390 50 unknown 40   44 550 unknown .36 36 3.7 unknown .20  36 1.9  unknown .17  36 2.2  unknown .17  36 2.0  timeout 880    540   6200   timeout (timeout) 900    5100   7300   unknown 6.7 350 49 unknown 5.5 320 43 unknown 5.8 310 44
busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .33  37 3.1  exception (gremlins) .087 11   .46 error (134) 310    14000 4200   unknown .023 .93 .058 error 5.2  280 44   error 5.2 280 43 unknown 890   1100 5700 out of memory 850    15000 6900   timeout 900     5100 12000    timeout 900     360 8500    unknown .18  31 2.6  true 880    660   12000   timeout (timeout) 900    1300   11000   unknown 6.1 330 44 unknown 5.8 320 47 unknown 5.7 320 43
busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i no-overflow error (8) .32  37 3.8  exception (gremlins) .086 11   .45 error (1) .34 32 3.1 unknown .012 .87 .045 error 5.4  330 44   error 5.3 280 39 unknown 900   1200 11000 out of memory 890    15000 8200   unknown 1.7   66 24    unknown 1.8   71 21    unknown .17  31 2.4  true 880    520   8600   timeout (timeout) 900    300   10000   unknown 5.1 310 37 unknown 5.3 310 43 unknown 5.7 330 43
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (134) 1.7   270 16    false(unreach-call) 1.6   110   21    error (1) 4.5  250 50   segmentation fault 1.1   35    13     exception 24    870 160   false(unreach-call) 170   2100 2300 out of memory 190   15000 2500 unknown 14    3900 160   unknown 7.1   3900 90    unknown 7.1   3900 99    unknown 7.1   3900 94    false(unreach-call) 640    880   7800   false(unreach-call) 710    180   9100   error 8.0 410 68 error 8.3 410 63 error 8.3 420 62
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i unreach-call out of memory 79     15000 730    false(unreach-call) 3.8   82   40    error (1) 240    1000 1400   segmentation fault .93  12    12     exception 96    3600 630   timeout 940   8300 7800 unknown 570   450 7700 unknown .58 100 6.4 unknown .28  100 3.7  unknown .28  100 3.7  unknown .28  100 3.1  timeout 880    480   8700   timeout (timeout) 900    390   8700   timeout 900   3700 8900 timeout 900   13000 12000 error 490   3600 4600
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (5) 91     1500 570    exception (gremlins) 40     280   470    error (1) 25    340 300   segmentation fault 1.3   13    16     segmentation fault 510    7200 4300   timeout 910   8600 7800 unknown 600   1100 7800 unknown .78 160 8.3 unknown .43  160 4.9  unknown .40  160 5.1  unknown .40  160 4.4  false(unreach-call) 16    220   190   timeout (timeout) 900    360   11000   unknown 110   2900 1000 timeout 900   11000 12000 unknown 110   3000 1100
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (5) 1.3   110 11    false(unreach-call) 7.6   210   75    false(unreach-call) 54    2300 380   segmentation fault 2.4   18    27     timeout 930    6200 8200   timeout 940   6600 9800 unknown 280   450 3500 unknown 1.7  440 16   unknown .85  440 11    unknown .87  440 9.3  unknown .90  440 9.2  timeout 880    990   11000   timeout (timeout) 900    260   11000   unknown 7.5 330 57 unknown 8.0 350 66 unknown 8.1 350 60
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i unreach-call out of memory 100     15000 850    false(unreach-call) 4.6   160   44    error (1) 850    6900 9200   segmentation fault 2.6   18    31     timeout 960    4600 8200   timeout 960   4900 12000 unknown 10   350 120 unknown 1.7  450 20   unknown .88  450 11    unknown .90  450 9.1  unknown .89  450 11    false(unreach-call) 56    310   680   false(unreach-call) 130    100   1400   unknown 7.3 340 55 unknown 7.0 330 54 unknown 7.4 350 54
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (5) 28     440 180    false(unreach-call) 24     260   310    error (1) 850    2700 5400   segmentation fault 1.4   14    16     false(unreach-call) 80    2300 460   false(unreach-call) 100   1000 1200 unknown 620   2600 7900 unknown .85 190 11   unknown .48  190 4.7  unknown .43  190 5.0  unknown .43  190 5.6  false(unreach-call) 8.8  210   100   timeout (timeout) 900    850   10000   error 550   2500 6100 timeout 900   12000 10000 error 80   1400 650
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i unreach-call out of memory 49     15000 520    false(unreach-call) 24     160   280    error (1) 5.8  180 65   segmentation fault 1.1   12    13     timeout 920    8800 6400   timeout 960   7900 9400 unknown 120   700 1600 unknown .62 140 6.8 unknown .36  140 3.7  unknown .31  140 3.6  unknown .32  140 4.0  false(unreach-call) 11    240   140   timeout (timeout) 900    270   9200   timeout 900   2400 9000 timeout 900   13000 12000 timeout 900   4100 5700
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i unreach-call out of memory 120     15000 1000    false(unreach-call) 61     660   600    error (1) 850    4400 4200   segmentation fault 2.0   16    22     timeout 960    9700 7400   timeout 920   6800 10000 unknown 820   9800 11000 unknown 1.9  630 25   unknown .97  630 12    unknown .98  630 12    unknown .96  630 12    false(unreach-call) 47    1700   600   timeout (timeout) 900    510   12000   unknown 230   2700 2500 timeout 900   12000 11000 error 120   3100 1100
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i unreach-call out of memory 160     15000 1200    false(unreach-call) 16     190   190    error (1) 850    2700 10000   segmentation fault 5.2   27    58     false(unreach-call) 120    2700 830   false(unreach-call) 350   5200 3300 out of memory 230   15000 2500 unknown 3.9  1100 46   unknown 1.9   1100 25    unknown 2.0   1100 22    unknown 1.9   1100 22    timeout 900    1700   10000   timeout (timeout) 900    470   10000   error 15   420 110 error 17   440 130 error 17   420 140
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (134) .93  220 9.8  false(unreach-call) 6.8   55   85    false(unreach-call) 5.0  270 56   false(unreach-call) 4.1   9.6  52     timeout 960    4400 11000   timeout 960   4800 11000 unknown 21   210 260 unknown .16 21 1.5 unknown .088 21 .84 unknown .11  21 .73 unknown .074 21 .88 false(unreach-call) 120    300   910   timeout (timeout) 900    98   10000   unknown 60   1200 480 timeout 900   12000 13000 unknown 64   1400 470
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (134) 1.2   270 14    false(unreach-call) 34     160   380    error (42) 850    1300 7200   false(unreach-call) 4.9   10    60     timeout 940    4800 7800   timeout 960   5200 10000 false(unreach-call) 7.3 410 89 out of memory 92    15000 1100   false(unreach-call) .34  76 4.7  false(unreach-call) .33  76 4.4  false(unreach-call) .37  76 4.2  timeout 880    770   6100   timeout (timeout) 900    110   9200   timeout 900   2600 6600 unknown 220   13000 2400 timeout 900   2800 5100
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (5) 1.1   81 10    timeout 3.0   130   1100    error (1) 850    2800 4200   false(unreach-call) 17     15    200     timeout 920    6500 8300   timeout 910   4600 10000 unknown 92   1000 1200 unknown .29 48 3.1 unknown .15  45 1.9  unknown .15  45 1.8  unknown .18  45 1.7  false(unreach-call) 16    220   200   error 15    110   200   unknown 96   1800 740 unknown 180   11000 2100 unknown 97   1900 910
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (134) 4.3   1100 46    exception (gremlins) 14     140   140    false(unreach-call) 42    3300 450   false(unreach-call) 12     13    140     timeout 960    10000 8600   timeout 960   8300 9800 false(unreach-call) 16   470 220 timeout 900    7900 7000   false(unreach-call) .67  130 8.2  false(unreach-call) .76  140 9.0  false(unreach-call) .75  140 9.3  false(unreach-call) 4.5  130   53   timeout (timeout) 900    240   12000   unknown 60   1600 480 unknown 52   9100 560 unknown 62   1600 500
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (134) 8.9   2400 130    false(unreach-call) 82     270   940    error (134) 65    14000 850   false(unreach-call) 12     15    150     timeout 960    6400 9400   timeout 960   12000 12000 unknown 900   720 11000 timeout 900    4000 5600   false(unreach-call) .66  130 7.8  false(unreach-call) .69  130 8.8  false(unreach-call) .67  140 7.1  false(unreach-call) 13    160   140   timeout (timeout) 900    260   9900   unknown 870   2700 11000 unknown 51   10000 440 timeout 900   2800 11000
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (134) 3.1   360 34    timeout 3.6   190   1100    false(unreach-call) 36    700 470   false(unreach-call) 8.0   11    91     timeout 960    4200 11000   timeout 910   4900 9200 unknown 31   250 370 unknown .17 29 2.3 unknown .12  29 1.1  unknown .095 29 1.3  unknown .10  29 1.1  false(unreach-call) 24    220   230   timeout (timeout) 900    230   11000   timeout 900   4200 13000 unknown 460   12000 5800 timeout 900   4300 11000
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i unreach-call error (134) 4.8   1200 66    exception (gremlins) 16     200   180    false(unreach-call) 2.7  290 29   segmentation fault .98  11    11     timeout 960    6500 7700   timeout 960   6600 9100 unknown 460   400 6000 unknown .19 29 2.1 unknown .12  29 1.0  unknown .097 29 1.0  unknown .12  29 1.1  false(unreach-call) 12    170   140   error 70    15000   780   unknown 180   4700 1800 unknown 340   12000 3700 unknown 200   4700 2000
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (5) 46     2300 260    true 3.2   270   36    error (1) 850    4200 6200   segmentation fault 1.4   14    16     timeout 960    10000 6500   true 98   2900 1200 unknown 620   2100 6900 unknown .86 210 11   unknown .46  210 5.3  unknown .49  210 5.2  unknown .48  210 4.7  true 35    420   420   timeout (timeout) 900    260   13000   true 26   720 210 error 760   11000 9100 true 26   700 210
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i unreach-call true 16     2800 180    true 3.2   290   42    true 680    7100 6100   segmentation fault 1.0   35    14     exception 330    5300 2500   true 100   2000 1400 out of memory 190   15000 2400 unknown 14    3900 190   unknown 7.1   3900 81    unknown 7.1   3900 110    unknown 7.0   3900 82    true 80    400   630   error 81    190   1200   true 130   2500 1400 timeout 900   9900 11000 true 130   2600 1400
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i unreach-call out of memory 40     15000 460    true 7.6   710   89    error (42) 850    810 3400   segmentation fault .58  10    6.7   exception 570    5400 5600   true 98   710 1100 unknown 530   9200 6800 unknown .38 51 3.7 unknown .19  51 1.9  unknown .21  51 1.8  unknown .21  51 2.0  true 4.0  130   53   true .68 38   7.1 true 34   2000 240 timeout 900   13000 13000 true 36   2000 240
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i unreach-call out of memory 85     15000 770    true 2.5   300   30    error (1) 850    3500 4100   segmentation fault 1.0   12    13     timeout 900    4600 9300   true 96   2900 1000 unknown 570   250 6700 unknown .57 110 7.0 unknown .34  110 3.2  unknown .31  110 3.1  unknown .30  110 3.2  true 3.4  130   37   timeout (timeout) 900    130   9800   true 16   540 120 timeout 900   2400 11000 true 15   540 110
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (5) .98  120 6.5  true 8.5   1100   110    error (42) 850    2400 4100   segmentation fault 1.0   11    12     timeout 960    6300 10000   timeout 960   6300 10000 unknown 85   260 1100 unknown .55 96 6.8 unknown .29  96 3.6  unknown .32  96 3.6  unknown 1.1   96 2.5  true 4.7  180   58   timeout (timeout) 900    210   12000   true 86   5200 600 timeout 900   12000 12000 true 83   5200 570
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i unreach-call true 16     3400 180    true 4.1   500   53    error (42) 850    3200 8100   segmentation fault 12     54    140     true 870    5700 7800   true 110   3200 1400 unknown 180   12000 2000 unknown 12    4700 150   unknown 5.8   4700 65    unknown 1.2   450 14    unknown 1.2   450 15    true 730    11000   6500   timeout (timeout) 900    330   10000   true 510   11000 5500 timeout 900   12000 11000 true 500   11000 5400
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (5) .25  35 2.4  true 8.2   770   100    error (42) 850    2800 3000   segmentation fault .49  9.8  5.5   true 120    4000 910   true 100   3700 1200 unknown 890   1400 9500 timeout 900    11000 6300   timeout 900     1800 9800    timeout 900     2100 12000    unknown 2.0   110 29    true 2.3  100   32   timeout (timeout) 900    180   12000   true 13   530 100 error 810   11000 11000 true 13   530 110
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i unreach-call true 5.3   1600 60    true 3.1   580   41    error (42) 850    1200 4900   segmentation fault 1.6   12    17     true 76    2700 490   true 55   3100 490 unknown 890   3600 10000 timeout 900    12000 6500   timeout 900     2300 8300    timeout 900     2300 8100    unknown 2.4   170 4.7  true 4.3  130   61   true .93 22   14   true 40   3000 340 error 260   11000 3200 true 37   2700 290
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i unreach-call true 82     14000 930    true 2.3   210   29    error (42) 850    3000 7000   segmentation fault 1.9   14    23     timeout 960    9200 6500   true 100   4100 970 unknown 500   3100 4900 unknown 1.2  320 12   unknown .63  320 8.0  unknown .59  320 6.5  unknown .64  320 5.9  true 7.3  190   93   timeout (timeout) 900    4100   11000   true 31   960 230 timeout 900   12000 11000 true 32   910 290
ldv-linux-3.0/module_get_put-drivers-net-pppox.ko_true-unreach-call.cil.out.i.pp.i unreach-call true .53  44 5.2  true 1.2   29   13    error (42) 850    3300 6300   segmentation fault .49  10    5.1   true 17    810 100   true 160   3600 1900 unknown 250   140 3600 out of memory 56    15000 500   timeout 900     14000 13000    out of memory 630     15000 7500    unknown .15  36 1.9  true 880    250   8100   timeout (timeout) 900    3600   9600   true 14   520 95 true 13   500 96 true 14   530 110
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i unreach-call out of memory 21     15000 280    true 5.6   560   62    error (42) 850    2600 4100   segmentation fault 1.1   12    13     timeout 960    11000 5400   true 100   3800 1100 unknown 590   11000 6500 unknown .67 160 9.3 unknown .34  160 3.9  unknown .35  160 4.0  unknown .33  160 3.8  true 32    500   420   timeout (timeout) 900    460   9300   true 25   720 180 timeout 900   12000 11000 true 23   830 160
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (5) 52     4300 420    true 5.7   600   72    error (1) 850    5900 4800   segmentation fault 1.6   50    22     timeout 920    9800 5700   true 100   2700 1200 unknown 630   5400 6700 unknown .92 230 10   unknown .50  230 4.9  unknown .50  230 5.7  unknown .49  230 5.3  true 31    300   340   timeout (timeout) 900    380   9700   true 31   1100 290 timeout 900   11000 13000 true 31   920 240
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i unreach-call out of memory 38     15000 390    true 4.6   500   56    error (42) 850    14000 7000   segmentation fault 1.6   14    22     exception 150    4400 1100   true 100   2800 1100 unknown 730   6900 8700 unknown 1.4  420 18   unknown .73  420 8.0  unknown .72  420 8.6  unknown .75  420 11    true 38    1200   510   timeout (timeout) 900    320   9100   error 100   13000 1000 error 100   13000 1100 error 100   12000 980
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (5) 3.4   500 26    true 3.2   390   47    error (1) 850    3400 8300   segmentation fault .92  48    11     timeout 910    10000 6400   true 98   1500 1200 unknown 900   4700 7100 timeout 900    12000 11000   timeout 900     2500 10000    timeout 900     2100 9000    unknown 51     610 520    true 5.3  140   66   timeout (timeout) 900    220   11000   true 24   820 190 timeout 900   12000 11000 true 25   800 190
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (134) .58  150 7.3  true 75     200   970    error (42) 850    2100 5000   witness invalid (true) .089 9.6  .55  true 42    1600 330   true 15   530 140 false(unreach-call) 4.1 200 57 out of memory 110    15000 1200   false(unreach-call) .99  55 2.1  false(unreach-call) .27  55 3.3  false(unreach-call) .27  55 3.1  timeout 880    720   7100   timeout (timeout) 900    170   9400   true 79   1400 660 timeout 900   13000 10000 true 110   1500 660
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i unreach-call out of memory 31     15000 390    true 7.3   750   86    error (42) 850    3200 5800   segmentation fault 1.6   11    18     timeout 970    11000 6300   true 100   2700 1200 out of memory 4.8 15000 48 timeout 900    3900 14000   timeout 900     5400 11000    unknown 260     3400 3400    unknown 260     3400 3300    true 3.9  130   59   timeout (timeout) 900    390   11000   true 19   730 170 unknown 110   12000 1200 true 21   570 140
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i unreach-call out of memory 31     15000 350    true 6.6   690   93    error (42) 850    4700 5900   segmentation fault 2.2   13    30     exception 300    6100 2100   true 100   1300 1200 unknown 900   5500 7800 out of memory 21    15000 260   out of memory 580     15000 7900    out of memory 460     15000 5300    true 38     2400 450    true 5.0  150   63   timeout (timeout) 900    460   8400   unknown 12   340 92 error 7.6 330 57 unknown 13   340 91
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i unreach-call true 6.6   1400 77    true 4.3   520   57    error (42) 850    1000 3900   segmentation fault 1.2   11    13     timeout (true) 960    5300 13000   true 110   4900 960 out of memory 690   15000 7500 out of memory 300    15000 3400   out of memory 69     15000 790    out of memory 73     15000 950    true 16     800 180    true 2.9  120   39   true 1.7  20   20   true 18   660 140 timeout 900   13000 10000 true 19   640 140
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (5) 1.2   87 9.9  true 5.8   490   66    error (1) 850    1600 5500   segmentation fault 1.4   11    16     timeout 940    8400 7800   timeout 900   8200 8900 unknown 510   4000 4400 unknown .22 35 3.2 unknown .14  35 1.1  unknown .13  35 1.1  unknown .12  35 1.1  true 4.2  140   59   error 770    250   9000   true 21   560 160 unknown 49   11000 520 true 21   560 170
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (5) 7.2   150 53    true 5.8   530   80    error (1) 850    2800 3800   segmentation fault 3.1   15    37     exception 270    5500 2000   true 100   1700 1400 unknown 540   3300 5400 unknown .38 73 4.6 unknown .23  70 2.9  unknown .22  68 2.3  unknown .23  71 2.1  true 28    300   400   timeout (timeout) 900    230   12000   error 11   330 87 error 11   330 92 error 11   330 93
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (134) .90  260 11    timeout 1.6   170   900    error (42) 850    1800 4800   witness invalid (true) .10  10    .66  true 40    1600 300   true 170   4800 1500 unknown 900   300 14000 true 900    10000 9000   timeout 900     4200 13000    timeout 900     2300 2000    unknown 2.3   78 6.3  timeout 880    920   6200   timeout (timeout) 900    140   9700   true 48   1400 320 unknown 110   10000 1200 true 53   1400 350
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i unreach-call false(unreach-call) 38     7600 450    true 16     660   200    error (42) 850    910 9300   segmentation fault 1.7   12    21     true 160    4800 1200   true 97   2300 1100 unknown 890   1600 7200 out of memory 94    15000 1000   timeout 900     5200 12000    timeout 900     2400 8700    unknown 30     600 380    timeout 880    1900   8400   timeout (timeout) 900    140   13000   true 48   2100 370 unknown 380   12000 4300 true 50   2000 370
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i unreach-call timeout 900     1500 9100    true 5.4   140   74    error (42) 850    950 9400   segmentation fault 1.2   11    15     exception 75    2900 460   timeout 900   7300 8100 false(unreach-call) 58   1100 720 timeout 900    650 11000   false(unreach-call) .79  93 9.3  false(unreach-call) .82  93 9.6  false(unreach-call) .77  93 9.9  true 890    420   7700   timeout (timeout) 900    290   10000   timeout 900   1400 12000 unknown 110   11000 1200 timeout 900   1400 10000
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i unreach-call true 32     6800 410    true 9.2   1100   110    error (42) 850    14000 6500   segmentation fault 2.7   15    30     timeout 970    11000 6100   true 99   1500 1300 unknown 520   2400 4900 unknown .32 63 3.7 unknown .19  62 1.8  unknown .16  62 2.1  unknown .17  62 2.1  true 6.4  150   92   timeout (timeout) 900    290   11000   true 30   1000 230 unknown 290   10000 3600 true 30   1000 230
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i unreach-call error (5) 1.9   210 17    true 7.5   900   80    error (1) 850    5700 6700   segmentation fault 1.7   11    18     timeout 940    11000 6600   true 98   2600 1100 unknown 900   1900 12000 timeout 900    9900 6900   timeout 900     3200 11000    timeout 900     7100 11000    unknown 11     500 130    true 4.0  130   49   timeout (timeout) 900    170   7700   true 29   1500 240 unknown 300   11000 3600 true 31   1200 250
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--gpu--drm--vmwgfx--vmwgfx.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c unreach-call out of memory 120     15000 870    false(unreach-call) 1.5   170   22    error (1) 850    4800 5500   timeout 900     89    12000     timeout 960    8900 6800   false(unreach-call) 38   920 340 unknown 890   14000 8900 out of memory 140    15000 1800   timeout 900     2900 5700    timeout 900     2900 6500    timeout 900     2900 5100    false(unreach-call) 240    800   2300   false(unreach-call) 170    1500   2100   out of memory 770   15000 7600 timeout 900   12000 10000 error 660   7500 7700
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call false(unreach-call) 170     1800 1300    false(unreach-call) 18     140   230    error (1) 4.5  1200 58   false(unreach-call) 8.9   11    110     timeout 960    11000 9400   out of memory 210   15000 2900 unknown 890   1000 6400 out of memory 93    15000 1100   false(unreach-call) 4.9   170 60    false(unreach-call) 7.2   290 110    false(unreach-call) 11     400 140    timeout 880    400   6500   timeout (timeout) 900    1300   11000   timeout 900   1500 6700 error 900   2100 11000 error 53   1500 380
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) .94  75 8.4  false(unreach-call) 19     160   240    error (1) 15    420 210   segmentation fault .25  26    2.6   out of memory 370    15000 3200   false(unreach-call) 18   740 140 unknown 890   2100 8200 timeout 900    5000 11000   false(unreach-call) 3.2   170 43    false(unreach-call) 3.2   170 36    timeout 900     4600 11000    false(unreach-call) 35    240   380   false(unreach-call) 61    72   680   timeout 900   4800 8900 timeout 900   12000 11000 error 210   4800 1900
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--isdn--capi--kernelcapi.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c unreach-call false(unreach-call) 1.6   310 15    false(unreach-call) 1.5   75   18    false(unreach-call) 1.3  130 14   witness invalid (false(unreach-call)) .31  15    4.0   false(unreach-call) 42    1700 260   false(unreach-call) 17   600 170 unknown 900   670 12000 out of memory 290    15000 3400   false(unreach-call) .88  190 7.6  false(unreach-call) .89  190 8.0  false(unreach-call) .93  190 9.2  timeout 890    1400   11000   false(unreach-call) 1.5  28   18   unknown 7.6 330 60 unknown 8.4 340 57 unknown 7.1 330 51
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call false(unreach-call) 12     2500 120    false(unreach-call) 10     800   120    error (134) 75    14000 960   witness invalid (false(unreach-call)) .63  24    7.8   false(unreach-call) 160    4400 1200   false(unreach-call) 61   2000 580 unknown 900   1100 13000 out of memory 11    15000 130   false(unreach-call) 2.1   440 26    false(unreach-call) 2.1   440 25    false(unreach-call) 2.2   440 20    timeout 900    5800   11000   error 740    160   7500   timeout 900   14000 6100 timeout 900   11000 11000 timeout 900   14000 5200
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 46     5400 420    false(unreach-call) 1.6   190   20    error (1) 850    2800 2900   false(unreach-call) 46     72    480     timeout 970    8600 6300   timeout 960   7900 8200 unknown 890   3200 12000 timeout 900    10000 11000   out of memory 330     15000 3000    out of memory 320     15000 3000    timeout 900     370 11000    false(unreach-call) 81    740   810   timeout (timeout) 900    320   10000   timeout 900   5200 11000 timeout 900   2500 13000 timeout 900   5300 11000
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--mem2mem_testdev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call false(unreach-call) 19     5500 250    false(unreach-call) 2.6   150   24    error (134) 40    13000 450   false(unreach-call) 10     14    110     false(unreach-call) 25    1200 150   false(unreach-call) 8.1 360 64 unknown 890   1100 6600 out of memory 11    15000 130   false(unreach-call) .95  140 11    false(unreach-call) .92  140 13    false(unreach-call) .94  140 13    false(unreach-call) 8.4  170   110   false(unreach-call) 8.5  49   100   timeout 900   2800 11000 timeout 900   9600 11000 error 72   1200 650
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--vivi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call timeout 900     8900 9100    false(unreach-call) 9.8   150   110    error (134) 45    13000 620   false(unreach-call) 23     20    230     timeout 960    10000 7700   out of memory 230   15000 2500 unknown 900   2400 2900 out of memory 11    15000 130   false(unreach-call) 2.9   190 33    false(unreach-call) 3.4   200 48    false(unreach-call) 3.4   210 44    timeout 880    260   12000   true 1.2  42   15   unknown 47   1400 380 timeout 900   13000 11000 unknown 45   1500 410
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--mtd--chips--cfi_cmdset_0001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 1.2   100 10    false(unreach-call) .42  50   5.2  error (1) 850    1100 6200   segmentation fault .63  130    6.2   false(unreach-call) 29    990 170   false(unreach-call) 9.0 390 72 unknown 880   6000 9900 out of memory 11    15000 130   unknown .90  330 9.5  unknown .90  330 9.5  unknown 4.3   340 10    false(unreach-call) 9.9  150   140   timeout (timeout) 900    180   9300   false(unreach-call) 43   950 380 timeout 900   900 11000 false(unreach-call) 44   940 410
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call false(unreach-call) 27     5800 320    false(unreach-call) 4.8   99   51    error (134) 38    14000 500   segmentation fault 2.5   13    32     timeout 960    12000 6600   false(unreach-call) 30   1400 270 unknown 900   1500 13000 out of memory 36    15000 410   false(unreach-call) .82  110 9.1  false(unreach-call) .83  110 9.8  false(unreach-call) .82  110 9.0  false(unreach-call) 16    220   210   timeout (timeout) 900    190   9800   timeout 900   4900 7400 timeout 900   5800 9300 timeout 900   4900 9000
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 1.6   200 14    false(unreach-call) .50  62   5.4  error (1) 850    4900 4300   false(unreach-call) 10     17    110     false(unreach-call) 39    2100 260   false(unreach-call) 9.4 400 68 false(unreach-call) 86   420 700 out of memory 9.6  15000 120   false(unreach-call) .62  120 7.2  false(unreach-call) .63  120 6.1  false(unreach-call) .65  120 6.8  false(unreach-call) 19    240   260   timeout (timeout) 900    460   9900   false(unreach-call) 40   960 330 timeout 900   13000 10000 false(unreach-call) 37   1100 300
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c unreach-call out of memory 130     15000 1100    false(unreach-call) 260     560   2400    error (1) 850    4400 7300   segmentation fault .99  37    10     timeout 950    11000 4800   false(unreach-call) 17   730 130 unknown 900   2800 10000 timeout 900    5000 13000   false(unreach-call) 24     1500 270    false(unreach-call) 24     1500 240    timeout 900     1700 9800    false(unreach-call) 710    1400   5600   error 32    130   420   false(unreach-call) 370   3500 4500 timeout 900   11000 9400 false(unreach-call) 370   3900 4500
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c unreach-call out of memory 140     15000 1100    exception (gremlins) 2.0   150   22    error (1) 850    3700 5200   false(unreach-call) 32     34    360     false(unreach-call) 290    5700 2000   false(unreach-call) 20   950 170 false(unreach-call) 60   3000 590 out of memory 10    15000 130   false(unreach-call) 1.2   220 13    false(unreach-call) 1.2   220 10    false(unreach-call) 2.0   240 21    timeout 900    11000   11000   error 560    130   6000   timeout 900   4600 9300 timeout 900   4700 9100 timeout 900   4600 9400
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call false(unreach-call) 2.2   500 22    false(unreach-call) .25  37   3.1  error (134) 44    13000 550   false(unreach-call) 5.1   12    55     false(unreach-call) 16    640 110   false(unreach-call) 6.7 330 51 false(unreach-call) 4.0 120 50 out of memory 180    15000 2100   false(unreach-call) .32  60 3.7  false(unreach-call) 1.2   60 3.1  false(unreach-call) .38  61 3.4  false(unreach-call) 6.0  110   95   timeout (timeout) 900    150   9500   false(unreach-call) 14   500 110 error 390   9700 4500 false(unreach-call) 15   510 100
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--storage--usb-storage.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 290     8000 1700    exception (gremlins) 1.5   120   20    error (1) 850    3900 7500   false(unreach-call) 27     32    340     false(unreach-call) 120    4500 880   false(unreach-call) 15   610 120 unknown 890   9200 4900 out of memory 67    15000 840   false(unreach-call) 1.2   230 11    false(unreach-call) 3.9   230 7.9  false(unreach-call) 1.2   240 13    timeout 890    1800   9600   timeout (timeout) 900    320   12000   timeout 900   5200 6800 timeout 900   2600 12000 timeout 900   4900 6400
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--vhost--vhost_net.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 100     2600 600    false(unreach-call) .76  92   8.6  error (134) 130    13000 1300   witness invalid (false(unreach-call)) .43  19    5.6   false(unreach-call) 260    5500 2000   false(unreach-call) 12   430 86 unknown 890   14000 9000 timeout 900    2200 8300   false(unreach-call) 52     640 750    false(unreach-call) 51     640 560    false(unreach-call) 53     660 550    timeout 890    570   7600   error 43    130   520   timeout 900   4000 11000 timeout 900   12000 12000 timeout 900   4300 11000
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 28     3400 280    false(unreach-call) 5.1   550   57    error (1) 850    3700 5000   false(unreach-call) 50     35    560     timeout 960    14000 6400   timeout 930   11000 8000 unknown 890   6200 9300 out of memory 11    15000 120   timeout 900     2100 9800    timeout 900     2400 8500    timeout 900     3600 9000    timeout 890    280   12000   timeout (timeout) 900    210   10000   timeout 900   4600 9100 timeout 900   1600 11000 unknown 870   6300 8900
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c unreach-call timeout 900     2200 12000    timeout 15     290   1100    error (1) 4.2  440 52   unknown 46     19    540     exception 17    1400 130   unknown 330   4500 3200 unknown 500   640 6800 unknown .32 32 4.0 unknown .16  32 1.9  unknown .19  32 1.8  unknown .16  32 2.3  false(unreach-call) 31    280   390   true .91 25   11   error 12   350 96 error 13   350 100 error 12   350 100
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.c unreach-call error (5) 1.2   170 10    false(unreach-call) .51  57   5.2  false(unreach-call) 440    2400 2800   segmentation fault .62  91    6.8   exception 16    1200 120   unknown 250   2900 2300 unknown 500   6300 6000 unknown .29 30 3.1 unknown .19  30 2.1  unknown .19  30 1.8  unknown .16  30 2.0  false(unreach-call) 5.2  130   64   timeout (timeout) 900    160   12000   error 12   350 99 error 12   340 85 error 12   350 110
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c unreach-call timeout 900     1800 12000    false(unreach-call) 4.4   110   49    false(unreach-call) 6.1  630 64   false(unreach-call) 320     63    3500     exception 18    1300 120   unknown 270   3500 2800 unknown 43   550 500 unknown .40 36 4.8 unknown .21  36 2.4  unknown .24  36 2.5  unknown .21  36 2.7  false(unreach-call) 8.6  160   110   timeout (timeout) 900    190   9100   error 13   350 93 error 12   350 97 error 12   340 100
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c unreach-call out of memory 120     15000 880    false(unreach-call) 1.1   140   14    error (1) 850    2500 6300   segmentation fault .43  26    5.6   exception 30    1900 220   unknown 390   4200 5200 out of memory 12   15000 120 unknown .50 39 6.1 unknown .28  39 2.6  unknown .24  39 2.7  unknown .25  39 3.2  false(unreach-call) 120    1000   1500   timeout (timeout) 900    330   9800   error 14   340 120 error 13   350 94 error 13   360 94
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c unreach-call error (5) 2.8   270 20    false(unreach-call) .79  94   9.6  error (1) 850    3800 4600   segmentation fault 22     39    270     exception 22    1600 180   unknown 280   4400 2800 unknown 28   270 330 unknown .45 39 6.0 unknown .22  39 2.8  unknown .23  39 2.5  unknown .26  39 2.4  false(unreach-call) 34    270   480   timeout (timeout) 900    470   9700   error 13   340 100 error 13   350 110 error 13   350 120
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c unreach-call false(unreach-call) 14     3000 150    false(unreach-call) .57  69   6.8  false(unreach-call) 7.5  1000 88   unknown 24     23    310     exception 19    1100 140   unknown 270   2300 2900 unknown 27   370 340 unknown .34 34 4.7 unknown .21  34 2.1  unknown .74  34 1.5  unknown .74  34 2.0  false(unreach-call) 9.6  210   150   false(unreach-call) 4.8  34   61   error 12   350 97 error 13   350 110 error 12   360 96
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c unreach-call false(unreach-call) 2.4   230 22    false(unreach-call) .55  63   7.9  false(unreach-call) 1.8  180 17   unknown 25     32    280     exception 19    1300 130   unknown 86   2600 900 unknown 23   310 290 unknown .37 35 4.1 unknown .22  35 2.3  unknown .23  35 2.2  unknown .19  35 2.3  false(unreach-call) 4.1  110   55   timeout (timeout) 900    130   10000   error 12   350 95 error 14   340 94 error 13   340 95
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--misc--sgi-xp--xpc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c unreach-call out of memory 140     15000 990    false(unreach-call) 160     8200   2400    error (42) 850    13000 3800   unknown 100     21    1200     timeout 960    12000 6100   timeout 920   9800 7900 unknown 890   14000 10000 timeout 900    870 11000   false(unreach-call) 530     2200 6600    false(unreach-call) 530     2400 8100    timeout 900     840 11000    false(unreach-call) 180    600   2000   error 27    79   350   timeout 900   3900 11000 timeout 900   13000 12000 timeout 900   4200 10000
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--net--wireless--orinoco--orinoco_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 40     1100 310    exception (gremlins) .44  51   4.5  error (1) 850    4000 4200   segmentation fault .20  14    2.5   timeout 970    12000 6400   timeout 910   8800 8300 unknown 260   4400 2700 unknown .37 66 4.0 unknown .18  66 1.9  unknown .19  66 1.8  unknown .18  66 1.9  false(unreach-call) 25    300   310   error 13    100   150   false(unreach-call) 350   1200 3100 error 860   12000 10000 error 50   920 400
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 430     5300 2300    timeout 900     6900   10000    error (1) 850    3600 6000   segmentation fault 8.0   18    90     timeout 960    11000 7000   timeout 930   9800 8800 unknown 570   13000 5100 unknown .60 130 7.4 unknown 1.2   130 2.8  unknown .34  130 3.5  unknown .31  130 3.6  error (1) 240    14000   2300   timeout (timeout) 900    430   13000   timeout 900   3700 5500 timeout 900   11000 11000 timeout 900   3900 4600
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call timeout 900     11000 10000    false(unreach-call) 54     450   620    false(unreach-call) 570    9100 3100   segmentation fault 2.2   11    28     segmentation fault 840    9800 6300   timeout 960   9200 9400 unknown 37   430 430 unknown .23 44 2.4 unknown .11  43 1.4  unknown .15  44 1.3  unknown .15  44 1.3  false(unreach-call) 6.7  140   96   timeout (timeout) 900    3800   11000   timeout 900   2900 9800 timeout 900   10000 11000 timeout 900   2900 7800
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--mv_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call error (5) 810     12000 6200    false(unreach-call) 22     410   260    error (1) 850    5700 5000   segmentation fault 22     15    280     out of memory 620    15000 4700   false(unreach-call) 100   2000 1100 unknown 470   3600 6200 unknown .47 100 6.8 unknown .28  100 3.0  unknown .28  100 2.8  unknown .25  100 3.0  error (1) 240    14000   2800   timeout (timeout) 900    270   10000   false(unreach-call) 51   1500 460 timeout 900   8900 11000 false(unreach-call) 53   1300 440
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--pch_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call timeout 900     8400 6000    false(unreach-call) 1.1   130   15    error (1) 850    7300 4100   unknown 32     15    420     timeout 960    12000 6100   false(unreach-call) 110   3200 1200 unknown 900   6800 6000 out of memory 230    15000 2800   timeout 900     1800 10000    timeout 900     2000 8000    unknown 160     710 1700    timeout 900    1100   7800   timeout (timeout) 900    140   9900   unknown 120   1600 1000 timeout 900   11000 11000 error 79   1500 640
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--apei--einj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call true .80  210 8.9  true .15  27   1.7  error (42) 850    4700 4500   unknown 1.9   10    24     true 14    630 110   true 95   2300 1300 unknown 900   380 9500 true 210    8900 2400   timeout 900     1000 3300    out of memory 670     15000 8300    true .56  67 6.8  true 2.4  97   32   true .47 15   5.8 true 15   530 110 timeout 900   12000 10000 true 16   550 110
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--bgrt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call true .25  37 2.6  true .087 26   .96 error (42) 850    14000 5600   true 1.5   9.5  16     true 4.9  290 36   true 3.7 270 28 true 6.5 280 66 true 53    3400 670   timeout 900     1300 13000    out of memory 460     15000 6400    true .23  32 2.6  true 1.6  78   21   true .32 13   3.6 true 9.9 430 76 true 110   670 1200 true 9.2 410 65
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call true .41  56 4.2  true .087 22   1.0  error (42) 850    14000 10000   true 1.7   9.7  22     true 5.6  290 46   true 4.0 270 34 unknown 900   760 10000 timeout 900    5800 7000   timeout 900     930 11000    timeout 900     3800 11000    unknown .23  34 2.6  true 1.8  89   21   true .40 14   4.7 true 13   540 92 timeout 900   12000 12000 true 13   550 95
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call true .28  46 2.7  true .079 21   .87 error (42) 850    1600 6900   true 1.4   9.1  15     true 6.1  300 44   true 4.5 280 33 true 25   290 320 timeout 900    11000 7400   timeout 900     530 11000    timeout 900     2200 13000    true .32  38 3.8  true 1.7  88   20   true .33 13   4.0 true 9.8 400 66 error 200   11000 2400 true 9.3 400 70
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call true .76  160 8.6  true .10  27   1.2  error (42) 850    14000 7000   true 1.6   9.4  19     true 6.3  320 52   true 4.0 270 30 unknown 890   1000 6900 timeout 900    5600 6700   timeout 900     950 13000    timeout 900     3600 13000    unknown .25  34 3.4  true 1.8  84   22   true .38 14   4.8 true 13   510 96 timeout 900   9700 13000 true 13   520 96
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call true .61  140 7.1  true .13  27   1.4  error (42) 850    14000 6600   true 2.0   10    26     true 6.7  340 48   true 4.3 280 39 true 10   280 110 out of memory 240    15000 2500   timeout 900     960 11000    timeout 900     7200 9800    true .40  49 4.4  true 2.0  77   27   timeout (timeout) 900    110   10000   true 12   520 89 timeout 900   12000 11000 true 12   550 86
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_netcell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call true .30  46 2.6  true .087 24   1.2  error (42) 850    3800 4600   true 2.0   9.8  23     true 5.5  330 45   true 3.9 270 35 true 8.1 280 71 true 130    4900 1500   timeout 900     1100 9800