| Example | AProVE |
|---|
| c/unsigned/juggernaut/loop1.c | max(7 + 7 * x, 14) | 6.328 |
| c/unsigned/juggernaut/loop2.c | max(18, 10 + 8 * N + -8 * x) | 6.496 |
| c/unsigned/juggernaut/loop3.c | max(17, 9 + 8 * x) | 7.931 |
| c/unsigned/juggernaut/loop5.c | 481 + 32 * |a| + 32 * |b| + 139 * |b_smax_32| + 15 * (|b_smax_32| * |b_smax_32|) | 296.934 |
| c/unsigned/juggernaut/loop6.c | max(7 + 9 * x, 16) | 12.968 |
| c/unsigned/juggernaut/loop10.c | min(40 + 7 * |b_umax_32|, max(21, 14 + 7 * b_umax_32 + -7 * x)) | 56.475 |
| c/unsigned/juggernaut/loop43.c | 41 + 22 * |x| | 8.908 |
| c/unsigned/juggernaut/loop45.c | 345 + 238 * |b_smax_32| + 40 * (|y| * |b_smax_32|) + 86 * |y| | 297.020 |
| c/unsigned/juggernaut/loop46.c | min(max(21 + 13 * m, 34, 10 + 13 * m + -13 * x), 114 + 26 * |b_umax_32|) | 66.316 |
| c/unsigned/juggernaut/loop48.c | max(17, 9 + 8 * x) | 6.984 |
| c/unsigned/juggernaut-paper/a.c | max(7 + 9 * x, 16) | 14.358 |
| c/unsigned/juggernaut-paper/c.c | min(max(21, 14 + 7 * b_umax_32 + -7 * x), 40 + 7 * |b_umax_32|) | 58.040 |
| c/unsigned/juggernaut-paper/g.c | max(18, 7 + 11 * x) | 8.147 |
| c/unsigned/juggernaut-paper/h.c | max(17, 9 + 8 * x) | 7.401 |
| c/unsigned/juggernaut-paper/i.c | 648 + 164 * |b_umax_32| + 46 * |z| | 297.125 |
| c/unsigned/mult/m01.c | Ο(ω) | -- |
| c/unsigned/mult/m02.c | Ο(ω) | -- |
| c/unsigned/mult/m03.c | Ο(ω) | -- |
| c/unsigned/mult/m04.c | Ο(ω) | 3.061 |
| c/unsigned/pointer/p01.c | 11 | 5.203 |
| c/unsigned/pointer/p02.c | 19 | 7.153 |
| c/unsigned/pointer/p03.c | Ο(ω) | 26.842 |
| c/unsigned/pointer/p04.c | 26 | 4.015 |
| c/unsigned/wdk-no-signed-overflow/allocsup1.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/cachesup.c | 117 | 8.192 |
| c/unsigned/wdk-no-signed-overflow/cddata.c | max(15, 9 + 6 * ByteCount) | 5.831 |
| c/unsigned/wdk-no-signed-overflow/comm.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/cseries.c | 27 + 8 * |b_umax_64| | 6.167 |
| c/unsigned/wdk-no-signed-overflow/cvsndrcv.c | 185560 + 12011 * |len| | 296.917 |
| c/unsigned/wdk-no-signed-overflow/easup.c | max(50, -14 + 16 * Name_Length, -30 + 16 * Name_Length, 18 + 16 * (Name_Length / 2), 11 + 16 * Name_Length, 43 + 16 * (Name_Length / 2) + -16 * (3 / 2), 11 + 16 * (Name_Length / 2), 43 + 16 * Name_Length + -16 * (5 / 2), 43 + 16 * Name_Length + -16 * (7 / 2)) | 25.242 |
| c/unsigned/wdk-no-signed-overflow/eeprom.c | Ο(ω) | 3.523 |
| c/unsigned/wdk-no-signed-overflow/gart.c | max(20 + 12 * NumberOfPages, 11 + 12 * NumberOfPages, 47) | 15.635 |
| c/unsigned/wdk-no-signed-overflow/gsm610.c | Ο(ω) | 201.627 |
| c/unsigned/wdk-no-signed-overflow/gsm6102.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/gsm6103.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/hw_ccmp.c | Ο(ω) | 3.007 |
| c/unsigned/wdk-no-signed-overflow/hwsim.c | max(20 + 29 * m_ScatterGatherMappingsQueued, 17 + 29 * m_ScatterGatherMappingsQueued, 75) | 83.271 |
| c/unsigned/wdk-no-signed-overflow/image.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/init.c | Ο(ω) | 2.434 |
| c/unsigned/wdk-no-signed-overflow/intrface.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/io.c | max(70 + 16 * (numSamplesThisPacket / 400) + -16 * (701 / 400), 70) | 11.798 |
| c/unsigned/wdk-no-signed-overflow/isochapi.c | Ο(ω) | 14.299 |
| c/unsigned/wdk-no-signed-overflow/miniport.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/miniport2.c | 269 | 21.759 |
| c/unsigned/wdk-no-signed-overflow/moudep.c | max(2 + 12 * Attempts, 26, 10 + 12 * Attempts) | 9.025 |
| c/unsigned/wdk-no-signed-overflow/mp_dbg.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/mpu.c | max(11 + -17 * context_BytesRead + 17 * context_Length, max(36, 20 + -8 * context_BytesRead + 8 * context_Length) + max(17, nat(-18 + -9 * context_BytesRead + 9 * context_Length) + max(17, -9 + -13 * context_BytesRead + 13 * context_Length)), 61, max(57, 33 + -8 * context_BytesRead + 8 * context_Length) + max(-55 + -17 * context_BytesRead + 17 * context_Length, nat(-27 + -9 * context_BytesRead + 9 * context_Length) + max(-55 + -17 * context_BytesRead + 17 * context_Length, nat(-39 + -13 * context_BytesRead + 13 * context_Length) + max(-55 + -17 * context_BytesRead + 17 * context_Length, 13), 13), 13), 58 + -30 * context_BytesRead + 30 * context_Length + -30 * (14 / 5), 41 + -30 * context_BytesRead + 30 * context_Length + -30 * (9 / 5)) | 28.205 |
| c/unsigned/wdk-no-signed-overflow/namelookup.c | max(7 + 11 * i, 10 + 11 * i, 32) | 22.648 |
| c/unsigned/wdk-no-signed-overflow/namesup2.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/nic_init.c | 31 | 3.715 |
| c/unsigned/wdk-no-signed-overflow/notify.c | max(7 + 7 * length, 14) | 7.154 |
| c/unsigned/wdk-no-signed-overflow/physet.c | 323 | 4.579 |
| c/unsigned/wdk-no-signed-overflow/queue.c | 42 + 11 * |ix| | 6.716 |
| c/unsigned/wdk-no-signed-overflow/rtstream.c | 52 + 18 * |b_umax_64| | 296.638 |
| c/unsigned/wdk-no-signed-overflow/S5933DK1.c | max(36, 36 + 14 * (Item_u_DmaWork_nbytes / 4) + -14 * (7 / 4)) | 13.470 |
| c/unsigned/wdk-no-signed-overflow/smbxchng.c | Ο(ω) | 3.181 |
| c/unsigned/wdk-no-signed-overflow/st_aplst.c | max(1 + nat(-36 + 9 * APCount) * nat(-3 + APCount) + max(69, 51 + 9 * APCount) + nat(-108 + 36 * APCount), 79) | 21.804 |
| c/unsigned/wdk-no-signed-overflow/st_misc.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/swap.c | Ο(ω) | -- |
| c/unsigned/wdk-no-signed-overflow/TpiParam.c | min(85 + 16 * |in2_Length|, max(35, 14 + 16 * in2_Length, 19 + 16 * out_MaximumLength)) | 8.631 |
| c/unsigned/wdk-no-signed-overflow/write.c | max(21, 1 + 10 * (Len / 8192)) | 7.579 |