diff --git a/tests/builtins/oracle_octagon/realloc.res.oracle b/tests/builtins/oracle_octagon/realloc.res.oracle deleted file mode 100644 index c6980b05984478ea2b30126a9ddb18da0eefae4e..0000000000000000000000000000000000000000 --- a/tests/builtins/oracle_octagon/realloc.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -627a628,630 -> [eva] realloc.c:152: Call to builtin realloc -> [eva:malloc] bases_to_realloc: {__realloc_w_main10_l152} -> [eva:malloc] realloc.c:152: weak free on bases: {__realloc_w_main10_l152} diff --git a/tests/value/oracle_octagon/CruiseControl.res.oracle b/tests/value/oracle_octagon/CruiseControl.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..7c3d8d711cfb271a197c462226160719fc31b075 --- /dev/null +++ b/tests/value/oracle_octagon/CruiseControl.res.oracle @@ -0,0 +1,8 @@ +979c979 +< [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1} +--- +> [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1} +1217c1217 +< [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1} +--- +> [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1} diff --git a/tests/value/oracle_octagon/builtins_split.res.oracle b/tests/value/oracle_octagon/builtins_split.res.oracle index 4f5a68d6cdb893ccd920cc33c02545f5580bb89d..09146749136af8ba9b8d1975d16dc9d93d042e86 100644 --- a/tests/value/oracle_octagon/builtins_split.res.oracle +++ b/tests/value/oracle_octagon/builtins_split.res.oracle @@ -6,7 +6,8 @@ > [eva] builtins_split.c:104: Call to builtin Frama_C_builtin_split_all > [eva] builtins_split.c:104: Call to builtin Frama_C_builtin_split_all > [eva] builtins_split.c:104: Call to builtin Frama_C_builtin_split_all -75a83,89 +75a83,90 +> [eva] builtins_split.c:112: Call to builtin Frama_C_builtin_split_all > [eva] builtins_split.c:112: Call to builtin Frama_C_builtin_split_all > [eva] builtins_split.c:112: Call to builtin Frama_C_builtin_split_all > [eva] builtins_split.c:112: Call to builtin Frama_C_builtin_split_all diff --git a/tests/value/oracle_octagon/equality.res.oracle b/tests/value/oracle_octagon/equality.res.oracle index 05c8486c527d39c5a0fb2f2967b82a1d155a1a0f..24564fbdf1425ff856a02a0ec9fe194fbaa53932 100644 --- a/tests/value/oracle_octagon/equality.res.oracle +++ b/tests/value/oracle_octagon/equality.res.oracle @@ -1,16 +1,10 @@ -42,43c42,43 -< [eva:alarm] equality.c:57: Warning: -< function sqrtf: precondition 'arg_positive' got status unknown. +60c60 +< [eva] equality.c:99: Frama_C_show_each_10_19: [10..42] --- -> [eva] equality.c:57: -> function sqrtf: precondition 'arg_positive' got status valid. +> [eva] equality.c:99: Frama_C_show_each_10_19: [10..19] 75,76c75,76 < y ∈ [0..42] or UNINITIALIZED < w ∈ [0..42] or UNINITIALIZED --- > y ∈ [0..42] > w ∈ [0..42] -87c87 -< res ∈ [-0. .. 3.16227769852] or UNINITIALIZED ---- -> res ∈ [3.74339206651e-23 .. 3.16227769852] or UNINITIALIZED diff --git a/tests/value/oracle_octagon/from_termin.res.oracle b/tests/value/oracle_octagon/from_termin.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..d03d84f92d569928f2f9156ff651c33acd1a291b --- /dev/null +++ b/tests/value/oracle_octagon/from_termin.res.oracle @@ -0,0 +1,2 @@ +9a10 +> [eva] from_termin.i:8: starting to merge loop iterations diff --git a/tests/value/oracle_octagon/gauges.res.oracle b/tests/value/oracle_octagon/gauges.res.oracle index 3bd3c265780ea7b9be6d67f03047adcaca64da7a..a5e47e28258fe4726d31ff83cb80079321750697 100644 --- a/tests/value/oracle_octagon/gauges.res.oracle +++ b/tests/value/oracle_octagon/gauges.res.oracle @@ -1,24 +1,17 @@ -196,197d195 -< [eva:alarm] gauges.c:156: Warning: -< signed overflow. assert -2147483648 ≤ toCopy - 1; -259,260d256 +259,260d258 < [eva:alarm] gauges.c:201: Warning: < signed overflow. assert -2147483648 ≤ numNonZero - 1; -282,286d277 +282,286d279 < [eva] gauges.c:218: Frama_C_show_each: < [eva] gauges.c:218: Frama_C_show_each: < [eva] gauges.c:218: Frama_C_show_each: < [eva:alarm] gauges.c:220: Warning: < signed overflow. assert -2147483648 ≤ n - 1; -767c758 +767c760 < numNonZero ∈ [-2147483648..8] --- > numNonZero ∈ {-1} -778c769 +778c771 < n ∈ [-2147483648..99] --- > n ∈ {-1} -839c830 -< toCopy ∈ [-2147483648..99] ---- -> toCopy ∈ {-1} diff --git a/tests/value/oracle_octagon/incompatible_states.res.oracle b/tests/value/oracle_octagon/incompatible_states.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..426fe5da2c9673132a9b84c5b02e570002c8ede6 --- /dev/null +++ b/tests/value/oracle_octagon/incompatible_states.res.oracle @@ -0,0 +1,4 @@ +58c58 +< t[0] ∈ {0; 1} +--- +> t[0] ∈ {0} diff --git a/tests/value/oracle_octagon/redundant_alarms.res.oracle b/tests/value/oracle_octagon/redundant_alarms.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..913f8ab9f773d1c9ba23e01b0551932c560dbeaa --- /dev/null +++ b/tests/value/oracle_octagon/redundant_alarms.res.oracle @@ -0,0 +1,2 @@ +46a47 +> [eva] redundant_alarms.c:39: starting to merge loop iterations diff --git a/tests/value/oracle_octagon/relations.res.oracle b/tests/value/oracle_octagon/relations.res.oracle index d629b85b3f675099e332d6bd6de8f9ec597de8d0..1aba9b820f8395e34b9d9534ab68f1098fd62045 100644 --- a/tests/value/oracle_octagon/relations.res.oracle +++ b/tests/value/oracle_octagon/relations.res.oracle @@ -1,16 +1,68 @@ -38,41d37 +34,49d33 +< [eva:alarm] relations.i:41: Warning: +< signed overflow. assert -2147483648 ≤ u[5] - u[0]; +< [eva:alarm] relations.i:41: Warning: +< signed overflow. assert u[5] - u[0] ≤ 2147483647; < [eva:alarm] relations.i:46: Warning: < signed overflow. assert -2147483648 ≤ u[10] - u[11]; < [eva:alarm] relations.i:46: Warning: < signed overflow. assert u[10] - u[11] ≤ 2147483647; -72c68 +< [eva:alarm] relations.i:48: Warning: +< signed overflow. assert -2147483648 ≤ u[1] - u[0]; +< [eva:alarm] relations.i:48: Warning: +< signed overflow. assert u[1] - u[0] ≤ 2147483647; +< [eva:alarm] relations.i:52: Warning: +< signed overflow. assert -2147483648 ≤ u[5] - u[1]; +< [eva:alarm] relations.i:52: Warning: +< signed overflow. assert u[5] - u[1] ≤ 2147483647; +60,61c44 +< u[0] ∈ [-2147483648..2147483646] +< [1] ∈ [--..--] +--- +> u[0..1] ∈ [-2147483648..2147483646] +67,78c50,60 +< R1 ∈ [--..--] +< R2 ∈ [--..--] +< R3 ∈ [-2147483648..2147483646] +< R4 ∈ [--..--] +< R5 ∈ [--..--] < R6 ∈ [--..--] +< R7 ∈ {0; 1} +< A7 ∈ [--..--] +< R8 ∈ {0; 1} +< A8 ∈ [--..--] +< S1 ∈ {-1; 0; 1} +< S2 ∈ {0; 1} --- +> R1 ∈ {0; 3} +> R2 ∈ {0; 3} +> R3 ∈ {0; 2} +> R4 ∈ {0; 2} +> R5 ∈ {1} > R6 ∈ {0} -80,81c76,78 +> R7 ∈ {1} +> A7 ∈ {0} +> A8 ∈ {1} +> S1 ∈ {0} +> S2 ∈ {1} +80,81c62,64 < e ∈ [--..--] < f ∈ [--..--] --- > e ∈ {1} > f[bits 0 to 7] ∈ {1; 4} > [bits 8 to 31] ∈ [--..--] +102c85 +< R7 FROM g (and SELF) +--- +> R7 FROM g +104d86 +< R8 FROM g (and SELF) +107c89 +< S2 FROM pCs; S_pCs[0]{.L0; .L1} (and SELF) +--- +> S2 FROM pCs; S_pCs[0]{.L0; .L1} +112c94 +< A7; R8; A8; S1; S2; c; e; f; tmp; tmp_0; S_pCs[0]{.T13; .T; .L8} +--- +> A7; A8; S1; S2; c; e; f; tmp; tmp_0; S_pCs[0]{.T13; .T; .L8} diff --git a/tests/value/oracle_octagon/struct2.res.oracle b/tests/value/oracle_octagon/struct2.res.oracle index 0422f2e21dd0d1c733352d3cab30a7e36443ca16..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 --- a/tests/value/oracle_octagon/struct2.res.oracle +++ b/tests/value/oracle_octagon/struct2.res.oracle @@ -1,7 +0,0 @@ -77,80d76 -< accessing out of bounds index. assert 0 ≤ (int)(i + j); -< [eva:alarm] struct2.i:185: Warning: -< accessing out of bounds index. assert (int)(i + j) < 2; -< [eva:alarm] struct2.i:185: Warning: -98d93 -< [scope:rm_asserts] removing 2 assertion(s) diff --git a/tests/value/oracle_octagon/taint.res.oracle b/tests/value/oracle_octagon/taint.res.oracle index 20cde28291166dccd71e3c6f77943d13a1804d4c..0fc62dbb2d3286ea6ce1457af4e564703f3eeb23 100644 --- a/tests/value/oracle_octagon/taint.res.oracle +++ b/tests/value/oracle_octagon/taint.res.oracle @@ -10,22 +10,3 @@ < y ∈ [2..11] --- > y ∈ {3; 5; 7; 9; 11} -229,232c229 -< Frama_C_entropy_source ∈ [--..--] -< tainted ∈ {2; 4; 6; 8; 10} -< l ∈ {0} -< __retres ∈ {0} ---- -> NON TERMINATING FUNCTION -255a253 -> [from] Non-terminating function main (no dependencies) -284,286c282 -< Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF) -< tainted FROM Frama_C_entropy_source -< \result FROM \nothing ---- -> NON TERMINATING - NO EFFECTS -325c321 -< Frama_C_entropy_source; tainted; l; __retres ---- -> Frama_C_entropy_source; tainted; l diff --git a/tests/value/oracle_octagon/unroll.res.oracle b/tests/value/oracle_octagon/unroll.res.oracle index c82ddd4f31807c175f11f4e55c96313f87a53446..b0b04dfe12a225825d9f1736faa4efc66d5f5b03 100644 --- a/tests/value/oracle_octagon/unroll.res.oracle +++ b/tests/value/oracle_octagon/unroll.res.oracle @@ -1,4 +1,6 @@ -20c20 +14a15 +> [eva] unroll.i:39: starting to merge loop iterations +20c21 < G ∈ [17739..2147483647] --- > G ∈ [17854..2147483647] diff --git a/tests/value/oracle_octagon/unroll_simple.res.oracle b/tests/value/oracle_octagon/unroll_simple.res.oracle index 8a48c42f84b464b622a56e6b0bdf325a1423af5f..0aead1b2497a8c7979e9bfe3c5945cdb38fb4408 100644 --- a/tests/value/oracle_octagon/unroll_simple.res.oracle +++ b/tests/value/oracle_octagon/unroll_simple.res.oracle @@ -1,4 +1,6 @@ -17c17 +11a12 +> [eva] unroll_simple.i:16: starting to merge loop iterations +17c18 < G ∈ [8772..2147483647] --- > G ∈ [8896..2147483647]