diff --git a/tests/value/oracle_apron/octagons-pointers-simple.res.oracle b/tests/value/oracle_apron/octagons-pointers-simple.res.oracle index ff90c5f6bbdc359ecf4988ec05ea4d08609f94b0..c976f8080e08fd8a1562ddb133889ddac757a32f 100644 --- a/tests/value/oracle_apron/octagons-pointers-simple.res.oracle +++ b/tests/value/oracle_apron/octagons-pointers-simple.res.oracle @@ -1,23 +1,15 @@ -18c18 -< size - index ∈ [3..--] ---- -> size - index ∈ {433} -19a20 -> size + cmdLen ∈ [--..867] -21a23 -> index - cmdLen ∈ [-428..--] -33a36 -> size + index ∈ [442..872] -35a39 -> size + cmdLen ∈ [--..864] -36a41,42 -> index + cmdLen ∈ [--..864] -> index - cmdLen ∈ [-422..--] -38c44 -< size - index ∈ [3..--] ---- -> size - index ∈ [3..430] -39a46,48 -> index - cmdLen ∈ [-422..--] -> index + index ∈ [12..869] -> index - index ∈ [--..430] +39a40,53 +> [eva] octagons-pointers-simple.c:43: starting to merge loop iterations +> [eva] octagons-pointers-simple.c:46: +> Frama_C_dump_each: +> # octagon: +> {[ buffer - cmd ∈ [-436..-6] +> cmd->cmdLen - cmdLen ∈ {0} +> index + cmdLen ∈ [--..434] +> cmd->cmdLen + index ∈ [--..434] +> ]} +> ==END OF DUMP== +> [eva] computing for function cmdRead <- main. +> Called from octagons-pointers-simple.c:47. +> [eva] Recording results for cmdRead +> [eva] Done for function cmdRead diff --git a/tests/value/oracle_apron/octagons-pointers.res.oracle b/tests/value/oracle_apron/octagons-pointers.res.oracle deleted file mode 100644 index 92808f6680b2537e10a9c350274f847a7dfef787..0000000000000000000000000000000000000000 --- a/tests/value/oracle_apron/octagons-pointers.res.oracle +++ /dev/null @@ -1,57 +0,0 @@ -18c18,19 -< size - index ∈ [3..--] ---- -> size - index ∈ {433} -> size + cmd->cmdLen ∈ [--..867] -20a22 -> index - cmd->cmdLen ∈ [-428..--] -29c31,32 -< size - index ∈ [3..--] ---- -> size - index ∈ {433} -> size + cmd->cmdLen ∈ [--..867] -31a35 -> index - cmd->cmdLen ∈ [-428..--] -46a51 -> size + index ∈ [--..872] -47a53 -> size + cmd->cmdLen ∈ [--..864] -49c55,58 -< size - index ∈ [3..--] ---- -> index + cmd->cmdLen ∈ [--..864] -> size - index ∈ [3..430] -> index + index ∈ [--..869] -> index - index ∈ [--..430] -50a60 -> cmd->cmdLen - index ∈ [--..422] -58a69 -> size + index ∈ [--..872] -59a71 -> size + cmd->cmdLen ∈ [--..864] -60a73 -> index + cmd->cmdLen ∈ [--..864] -63c76,78 -< size - index ∈ [3..--] ---- -> size - index ∈ [3..430] -> index + index ∈ [--..869] -> index - index ∈ [--..430] -64a80 -> cmd->cmdLen - index ∈ [--..422] -105a122 -> size + cmd->cmdLen ∈ [--..864] -107c124 -< size - index ∈ [3..--] ---- -> size - index ∈ [3..430] -108a126 -> cmd->cmdLen - index ∈ [--..422] -116a135 -> size + cmd->cmdLen ∈ [--..864] -120c139 -< size - index ∈ [3..--] ---- -> size - index ∈ [3..430] -121a141 -> cmd->cmdLen - index ∈ [--..422] diff --git a/tests/value/oracle_apron/octagons.res.oracle b/tests/value/oracle_apron/octagons.res.oracle index 75df605d4717f0d203b314d1ee99561c98445bd8..1c3d249968164cc4519adfbf3661a2bbabe3a944 100644 --- a/tests/value/oracle_apron/octagons.res.oracle +++ b/tests/value/oracle_apron/octagons.res.oracle @@ -1,78 +1,4 @@ -239a240 -> a - neg_a ∈ [-24..39] -240a242 -> b - neg_b ∈ [-23..40] -242,256c244,265 -< a + r1 ∈ [-4..--] -< a - r1 ∈ [--..12] -< b + r1 ∈ [-4..--] -< b - r1 ∈ [--..12] -< neg_a + r1 ∈ [-12..--] -< neg_a - r1 ∈ [--..4] -< neg_b + r1 ∈ [-12..--] -< neg_b - r1 ∈ [--..4] -< a + r2 ∈ [-4..--] -< a - r2 ∈ [--..12] -< neg_b + r2 ∈ [-12..--] -< neg_b - r2 ∈ [--..20] -< b + r2 ∈ [-4..--] -< b - r2 ∈ [--..12] -< r1 + r2 ∈ [-16..--] ---- -> a - b ∈ [-16..16] -> b + neg_a ∈ [-16..16] -> a + neg_b ∈ [-16..16] -> a + r1 ∈ [-4..28] -> a - r1 ∈ [-20..12] -> b + r1 ∈ [-4..28] -> b - r1 ∈ [-20..12] -> neg_a + r1 ∈ [-12..20] -> neg_a - r1 ∈ [-28..4] -> neg_b + r1 ∈ [-12..20] -> neg_b - r1 ∈ [-28..4] -> neg_a + neg_b ∈ [-40..24] -> neg_a - neg_b ∈ [-16..16] -> a + r2 ∈ [-4..28] -> a - r2 ∈ [-20..12] -> neg_b + r2 ∈ [-12..20] -> neg_b - r2 ∈ [-28..4] -> b + r2 ∈ [-4..28] -> b - r2 ∈ [-20..12] -> neg_a + r2 ∈ [-12..20] -> neg_a - r2 ∈ [-28..4] -> r1 + r2 ∈ [-16..32] -258,268c267,275 -< neg_a + r2 ∈ [-12..--] -< neg_a - r2 ∈ [--..17] -< a + r3 ∈ [-4..--] -< a - r3 ∈ [--..12] -< b + r3 ∈ [-4..--] -< b - r3 ∈ [--..12] -< neg_a + r3 ∈ [-12..--] -< neg_a - r3 ∈ [--..4] -< neg_b + r3 ∈ [-12..--] -< neg_b - r3 ∈ [--..4] -< r1 + r3 ∈ [-16..--] ---- -> a + r3 ∈ [-4..28] -> a - r3 ∈ [-20..12] -> b + r3 ∈ [-4..28] -> b - r3 ∈ [-20..12] -> neg_a + r3 ∈ [-12..20] -> neg_a - r3 ∈ [-28..4] -> neg_b + r3 ∈ [-12..20] -> neg_b - r3 ∈ [-28..4] -> r1 + r3 ∈ [-16..32] -270c277 -< r2 + r3 ∈ [-16..--] ---- -> r2 + r3 ∈ [-16..32] -297c304,305 -< {[ k - tmp ∈ {0} ---- -> {[ k + tmp ∈ [-256..272] -> k - tmp ∈ {0} -417,420c425,428 +371,374c371,374 < a ∈ [-1024..2147483647] < b ∈ [-1023..2147483647] < c ∈ [-1023..2147483647] diff --git a/tests/value/oracle_equality/octagons.res.oracle b/tests/value/oracle_equality/octagons.res.oracle index b9c6fb2faa8cd7f3a4e839da43428b739f0aa0c0..3b1ca3ecba8569890b9c9fad8a1d7fe77e4b0226 100644 --- a/tests/value/oracle_equality/octagons.res.oracle +++ b/tests/value/oracle_equality/octagons.res.oracle @@ -2,53 +2,7 @@ < [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-128..127], [-128..127] --- > [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-118..114], [6..127] -239a240 -> a - neg_a ∈ [-24..--] -240a242 -> b - neg_b ∈ [-23..--] -242,245c244,252 -< a + r1 ∈ [-4..--] -< a - r1 ∈ [--..12] -< b + r1 ∈ [-4..--] -< b - r1 ∈ [--..12] ---- -> a - b ∈ [-16..16] -> b + neg_a ∈ [-16..16] -> b - neg_a ∈ [-22..--] -> a + neg_b ∈ [-16..16] -> a - neg_b ∈ [-24..--] -> a + r1 ∈ [-4..28] -> a - r1 ∈ [-20..12] -> b + r1 ∈ [-4..28] -> b - r1 ∈ [-20..12] -250,251c257,258 -< a + r2 ∈ [-4..--] -< a - r2 ∈ [--..12] ---- -> a + r2 ∈ [-4..28] -> a - r2 ∈ [-20..12] -254,255c261,262 -< b + r2 ∈ [-4..--] -< b - r2 ∈ [--..12] ---- -> b + r2 ∈ [-4..28] -> b - r2 ∈ [-20..12] -260,263c267,270 -< a + r3 ∈ [-4..--] -< a - r3 ∈ [--..12] -< b + r3 ∈ [-4..--] -< b - r3 ∈ [--..12] ---- -> a + r3 ∈ [-4..28] -> a - r3 ∈ [-20..12] -> b + r3 ∈ [-4..28] -> b - r3 ∈ [-20..12] -297c304,305 -< {[ k - tmp ∈ {0} ---- -> {[ k + tmp ∈ [-256..272] -> k - tmp ∈ {0} -404c412 +358c358 < ct ∈ [--..--] or UNINITIALIZED --- > ct ∈ [6..127] or UNINITIALIZED diff --git a/tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle b/tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle index e925f647f0e27e141be95a7f49fbf956427b53c5..993825158c77e1d611c02be27e37da1414ab72d1 100644 --- a/tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle +++ b/tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle @@ -1,9 +1,8 @@ -28a29,36 -> [eva] computing for function cmdRead <- main. -> Called from octagons-pointers-intermediate.c:45. -> [eva] Recording results for cmdRead -> [eva] Done for function cmdRead -> [eva] computing for function cmdRead <- main. -> Called from octagons-pointers-intermediate.c:45. -> [eva] Recording results for cmdRead -> [eva] Done for function cmdRead +23a24,30 +> [eva] octagons-pointers-intermediate.c:42: starting to merge loop iterations +> [eva] octagons-pointers-intermediate.c:45: +> Reusing old results for call to cmdRead +> [eva] octagons-pointers-intermediate.c:45: +> Reusing old results for call to cmdRead +> [eva] octagons-pointers-intermediate.c:45: +> Reusing old results for call to cmdRead diff --git a/tests/value/oracle_gauges/octagons-pointers-simple.res.oracle b/tests/value/oracle_gauges/octagons-pointers-simple.res.oracle index 6fd730a78a63bccaf83d44c6512c6ec1cd45ff52..1f0784eedc6dda45bb7958cdb87c4a3553ffd9b4 100644 --- a/tests/value/oracle_gauges/octagons-pointers-simple.res.oracle +++ b/tests/value/oracle_gauges/octagons-pointers-simple.res.oracle @@ -1,33 +1,32 @@ -65a66,97 +39a40,70 +> [eva] octagons-pointers-simple.c:43: starting to merge loop iterations > [eva] octagons-pointers-simple.c:46: > Frama_C_dump_each: > # octagon: > {[ buffer - cmd ∈ [-436..-6] > cmd->cmdLen - cmdLen ∈ {0} -> size - cmdLen ∈ [8..--] -> size - cmd->cmdLen ∈ [8..--] -> size - index ∈ [3..--] > index + cmdLen ∈ [--..434] > cmd->cmdLen + index ∈ [--..434] > ]} > ==END OF DUMP== -> [eva] computing for function cmdRead <- main. -> Called from octagons-pointers-simple.c:47. -> [eva] Recording results for cmdRead -> [eva] Done for function cmdRead +> [eva] octagons-pointers-simple.c:47: Reusing old results for call to cmdRead > [eva] octagons-pointers-simple.c:46: > Frama_C_dump_each: > # octagon: > {[ buffer - cmd ∈ [-436..-6] > cmd->cmdLen - cmdLen ∈ {0} -> size - cmdLen ∈ [8..--] -> size - cmd->cmdLen ∈ [8..--] -> size - index ∈ [3..--] > index + cmdLen ∈ [--..434] > cmd->cmdLen + index ∈ [--..434] > ]} > ==END OF DUMP== -> [eva] computing for function cmdRead <- main. -> Called from octagons-pointers-simple.c:47. -> [eva] Recording results for cmdRead -> [eva] Done for function cmdRead +> [eva] octagons-pointers-simple.c:47: Reusing old results for call to cmdRead +> [eva] octagons-pointers-simple.c:46: +> Frama_C_dump_each: +> # octagon: +> {[ buffer - cmd ∈ [-436..-6] +> cmd->cmdLen - cmdLen ∈ {0} +> index + cmdLen ∈ [--..434] +> cmd->cmdLen + index ∈ [--..434] +> ]} +> ==END OF DUMP== +> [eva] octagons-pointers-simple.c:47: Reusing old results for call to cmdRead diff --git a/tests/value/oracle_gauges/octagons-pointers.res.oracle b/tests/value/oracle_gauges/octagons-pointers.res.oracle index 7d34f5116703176f692a4b5bea83827a74554321..2c58a7bd206f37b42c9c11cda6d577546e1498e6 100644 --- a/tests/value/oracle_gauges/octagons-pointers.res.oracle +++ b/tests/value/oracle_gauges/octagons-pointers.res.oracle @@ -1,99 +1,26 @@ -150a151,248 +83a84,108 +> [eva] octagons-pointers.c:43: starting to merge loop iterations > [eva] octagons-pointers.c:46: > Frama_C_dump_each: > # octagon: > {[ buffer - cmd ∈ [-436..-6] -> size - cmd->cmdLen ∈ [8..--] -> size - index ∈ [3..--] > cmd->cmdLen + index ∈ [--..434] > ]} > ==END OF DUMP== -> [eva] computing for function cmdRead <- main. -> Called from octagons-pointers.c:47. -> [eva] octagons-pointers.c:31: -> Frama_C_dump_each: -> # octagon: -> {[ buffer - cmd ∈ [-436..-6] -> size - cmd->cmdLen ∈ [8..--] -> buffer - cmd ∈ [-433..-6] -> cmd - cmd ∈ [-430..427] -> size - index ∈ [3..--] -> cmd->cmdLen + index ∈ [--..434] -> cmd - len ∈ {0} -> len - cmd ∈ [-430..427] -> buffer - len ∈ [-433..-6] -> len - code ∈ {-2} -> cmd - code ∈ {-2} -> code - cmd ∈ [-428..429] -> buffer - code ∈ [-435..-8] -> code - elt1 ∈ {-1} -> cmd - elt1 ∈ {-3} -> len - elt1 ∈ {-3} -> elt1 - cmd ∈ [-427..430] -> buffer - elt1 ∈ [-436..-9] -> elt1 - elt2 ∈ {-4} -> cmd - elt2 ∈ {-7} -> len - elt2 ∈ {-7} -> code - elt2 ∈ {-5} -> elt2 - cmd ∈ [-423..434] -> buffer - elt2 ∈ [-440..-13] -> elt2 - elt3 ∈ {-2} -> cmd - elt3 ∈ {-9} -> len - elt3 ∈ {-9} -> code - elt3 ∈ {-7} -> elt1 - elt3 ∈ {-6} -> elt3 - cmd ∈ [-421..436] -> buffer - elt3 ∈ [-442..-15] -> ]} -> ==END OF DUMP== -> [eva] Recording results for cmdRead -> [eva] Done for function cmdRead +> [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead > [eva] octagons-pointers.c:46: > Frama_C_dump_each: > # octagon: > {[ buffer - cmd ∈ [-436..-6] -> size - cmd->cmdLen ∈ [8..--] -> size - index ∈ [3..--] > cmd->cmdLen + index ∈ [--..434] > ]} > ==END OF DUMP== -> [eva] computing for function cmdRead <- main. -> Called from octagons-pointers.c:47. -> [eva] octagons-pointers.c:31: +> [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead +> [eva] octagons-pointers.c:46: > Frama_C_dump_each: > # octagon: > {[ buffer - cmd ∈ [-436..-6] -> size - cmd->cmdLen ∈ [8..--] -> buffer - cmd ∈ [-433..-6] -> cmd - cmd ∈ [-430..427] -> size - index ∈ [3..--] > cmd->cmdLen + index ∈ [--..434] -> cmd - len ∈ {0} -> len - cmd ∈ [-430..427] -> buffer - len ∈ [-433..-6] -> len - code ∈ {-2} -> cmd - code ∈ {-2} -> code - cmd ∈ [-428..429] -> buffer - code ∈ [-435..-8] -> code - elt1 ∈ {-1} -> cmd - elt1 ∈ {-3} -> len - elt1 ∈ {-3} -> elt1 - cmd ∈ [-427..430] -> buffer - elt1 ∈ [-436..-9] -> elt1 - elt2 ∈ {-4} -> cmd - elt2 ∈ {-7} -> len - elt2 ∈ {-7} -> code - elt2 ∈ {-5} -> elt2 - cmd ∈ [-423..434] -> buffer - elt2 ∈ [-440..-13] -> elt2 - elt3 ∈ {-2} -> cmd - elt3 ∈ {-9} -> len - elt3 ∈ {-9} -> code - elt3 ∈ {-7} -> elt1 - elt3 ∈ {-6} -> elt3 - cmd ∈ [-421..436] -> buffer - elt3 ∈ [-442..-15] > ]} > ==END OF DUMP== -> [eva] Recording results for cmdRead -> [eva] Done for function cmdRead +> [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead diff --git a/tests/value/oracle_gauges/octagons.res.oracle b/tests/value/oracle_gauges/octagons.res.oracle index 59771def423208a95014d8677b7fede8839b604a..f07f5b7d9bc184727b1db9fd272ec66d12fae701 100644 --- a/tests/value/oracle_gauges/octagons.res.oracle +++ b/tests/value/oracle_gauges/octagons.res.oracle @@ -11,7 +11,7 @@ < [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1] --- > [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2468..1] -417,420c409,412 +371,374c363,366 < a ∈ [-1024..2147483647] < b ∈ [-1023..2147483647] < c ∈ [-1023..2147483647] @@ -21,7 +21,7 @@ > b ∈ [-181..1867] > c ∈ [-602..1446] > d ∈ [-190..1874] -422c414 +376c368 < d2 ∈ [-2147483648..1] --- > d2 ∈ [-2468..1] diff --git a/tests/value/oracle_symblocs/octagons-pointers.res.oracle b/tests/value/oracle_symblocs/octagons-pointers.res.oracle deleted file mode 100644 index 9dafd7775e8ba04b996c8380938d4daace1897e0..0000000000000000000000000000000000000000 --- a/tests/value/oracle_symblocs/octagons-pointers.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -34,35c34,35 -< cmd - len ∈ {0} -< len - code ∈ {-2} ---- -> len - cmd ∈ {0} -> code - len ∈ {2}