Skip to content
Snippets Groups Projects
Commit ae875544 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Updates alternative test oracles on octagon tests.

parent e8db19c3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 47 additions and 313 deletions
tests/value/oracle_apron/octagons-pointers-simple.res.oracle
+ 15
− 23
View file @ ae875544
18c18 39a40,53
< size - index ∈ [3..--] > [eva] octagons-pointers-simple.c:43: starting to merge loop iterations
--- > [eva] octagons-pointers-simple.c:46:
> size - index ∈ {433} > Frama_C_dump_each:
19a20 > # octagon:
> size + cmdLen ∈ [--..867] > {[ buffer - cmd ∈ [-436..-6]
21a23 > cmd->cmdLen - cmdLen ∈ {0}
> index - cmdLen ∈ [-428..--] > index + cmdLen ∈ [--..434]
33a36 > cmd->cmdLen + index ∈ [--..434]
> size + index ∈ [442..872] > ]}
35a39 > ==END OF DUMP==
> size + cmdLen ∈ [--..864] > [eva] computing for function cmdRead <- main.
36a41,42 > Called from octagons-pointers-simple.c:47.
> index + cmdLen ∈ [--..864] > [eva] Recording results for cmdRead
> index - cmdLen ∈ [-422..--] > [eva] Done for function cmdRead
38c44
< size - index ∈ [3..--]
---
> size - index ∈ [3..430]
39a46,48
> index - cmdLen ∈ [-422..--]
> index + index ∈ [12..869]
> index - index ∈ [--..430]
tests/value/oracle_apron/octagons-pointers.res.oracle deleted 100644 → 0
+ 0
− 57
View file @ e8db19c3
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]
tests/value/oracle_apron/octagons.res.oracle
+ 1
− 75
View file @ ae875544
239a240 371,374c371,374
> 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
< a ∈ [-1024..2147483647] < a ∈ [-1024..2147483647]
< b ∈ [-1023..2147483647] < b ∈ [-1023..2147483647]
< c ∈ [-1023..2147483647] < c ∈ [-1023..2147483647]
......
tests/value/oracle_equality/octagons.res.oracle
+ 1
− 47
View file @ ae875544
...@@ -2,53 +2,7 @@ ...@@ -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: [-128..127], [-128..127]
--- ---
> [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-118..114], [6..127] > [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-118..114], [6..127]
239a240 358c358
> 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
< ct ∈ [--..--] or UNINITIALIZED < ct ∈ [--..--] or UNINITIALIZED
--- ---
> ct ∈ [6..127] or UNINITIALIZED > ct ∈ [6..127] or UNINITIALIZED
tests/value/oracle_gauges/octagons-pointers-intermediate.res.oracle
+ 8
− 9
View file @ ae875544
28a29,36 23a24,30
> [eva] computing for function cmdRead <- main. > [eva] octagons-pointers-intermediate.c:42: starting to merge loop iterations
> Called from octagons-pointers-intermediate.c:45. > [eva] octagons-pointers-intermediate.c:45:
> [eva] Recording results for cmdRead > Reusing old results for call to cmdRead
> [eva] Done for function cmdRead > [eva] octagons-pointers-intermediate.c:45:
> [eva] computing for function cmdRead <- main. > Reusing old results for call to cmdRead
> Called from octagons-pointers-intermediate.c:45. > [eva] octagons-pointers-intermediate.c:45:
> [eva] Recording results for cmdRead > Reusing old results for call to cmdRead
> [eva] Done for function cmdRead
tests/value/oracle_gauges/octagons-pointers-simple.res.oracle
+ 14
− 15
View file @ ae875544
65a66,97 39a40,70
> [eva] octagons-pointers-simple.c:43: starting to merge loop iterations
> [eva] octagons-pointers-simple.c:46: > [eva] octagons-pointers-simple.c:46:
> Frama_C_dump_each: > Frama_C_dump_each:
> # octagon: > # octagon:
> {[ buffer - cmd ∈ [-436..-6] > {[ buffer - cmd ∈ [-436..-6]
> cmd->cmdLen - cmdLen ∈ {0} > cmd->cmdLen - cmdLen ∈ {0}
> size - cmdLen ∈ [8..--]
> size - cmd->cmdLen ∈ [8..--]
> size - index ∈ [3..--]
> index + cmdLen ∈ [--..434] > index + cmdLen ∈ [--..434]
> cmd->cmdLen + index ∈ [--..434] > cmd->cmdLen + index ∈ [--..434]
> ]} > ]}
> ==END OF DUMP== > ==END OF DUMP==
> [eva] computing for function cmdRead <- main. > [eva] octagons-pointers-simple.c:47: Reusing old results for call to cmdRead
> Called from octagons-pointers-simple.c:47.
> [eva] Recording results for cmdRead
> [eva] Done for function cmdRead
> [eva] octagons-pointers-simple.c:46: > [eva] octagons-pointers-simple.c:46:
> Frama_C_dump_each: > Frama_C_dump_each:
> # octagon: > # octagon:
> {[ buffer - cmd ∈ [-436..-6] > {[ buffer - cmd ∈ [-436..-6]
> cmd->cmdLen - cmdLen ∈ {0} > cmd->cmdLen - cmdLen ∈ {0}
> size - cmdLen ∈ [8..--]
> size - cmd->cmdLen ∈ [8..--]
> size - index ∈ [3..--]
> index + cmdLen ∈ [--..434] > index + cmdLen ∈ [--..434]
> cmd->cmdLen + index ∈ [--..434] > cmd->cmdLen + index ∈ [--..434]
> ]} > ]}
> ==END OF DUMP== > ==END OF DUMP==
> [eva] computing for function cmdRead <- main. > [eva] octagons-pointers-simple.c:47: Reusing old results for call to cmdRead
> Called from octagons-pointers-simple.c:47. > [eva] octagons-pointers-simple.c:46:
> [eva] Recording results for cmdRead > Frama_C_dump_each:
> [eva] Done for function cmdRead > # 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
tests/value/oracle_gauges/octagons-pointers.res.oracle
+ 6
− 79
View file @ ae875544
150a151,248 83a84,108
> [eva] octagons-pointers.c:43: starting to merge loop iterations
> [eva] octagons-pointers.c:46: > [eva] octagons-pointers.c:46:
> Frama_C_dump_each: > Frama_C_dump_each:
> # octagon: > # octagon:
> {[ buffer - cmd ∈ [-436..-6] > {[ buffer - cmd ∈ [-436..-6]
> size - cmd->cmdLen ∈ [8..--]
> size - index ∈ [3..--]
> cmd->cmdLen + index ∈ [--..434] > cmd->cmdLen + index ∈ [--..434]
> ]} > ]}
> ==END OF DUMP== > ==END OF DUMP==
> [eva] computing for function cmdRead <- main. > [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead
> 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:46: > [eva] octagons-pointers.c:46:
> Frama_C_dump_each: > Frama_C_dump_each:
> # octagon: > # octagon:
> {[ buffer - cmd ∈ [-436..-6] > {[ buffer - cmd ∈ [-436..-6]
> size - cmd->cmdLen ∈ [8..--]
> size - index ∈ [3..--]
> cmd->cmdLen + index ∈ [--..434] > cmd->cmdLen + index ∈ [--..434]
> ]} > ]}
> ==END OF DUMP== > ==END OF DUMP==
> [eva] computing for function cmdRead <- main. > [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead
> Called from octagons-pointers.c:47. > [eva] octagons-pointers.c:46:
> [eva] octagons-pointers.c:31:
> Frama_C_dump_each: > Frama_C_dump_each:
> # octagon: > # octagon:
> {[ buffer - cmd ∈ [-436..-6] > {[ buffer - cmd ∈ [-436..-6]
> size - cmd->cmdLen ∈ [8..--]
> buffer - cmd ∈ [-433..-6]
> cmd - cmd ∈ [-430..427]
> size - index ∈ [3..--]
> cmd->cmdLen + index ∈ [--..434] > 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== > ==END OF DUMP==
> [eva] Recording results for cmdRead > [eva] octagons-pointers.c:47: Reusing old results for call to cmdRead
> [eva] Done for function cmdRead
tests/value/oracle_gauges/octagons.res.oracle
+ 2
− 2
View file @ ae875544
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
< [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1] < [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1]
--- ---
> [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2468..1] > [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2468..1]
417,420c409,412 371,374c363,366
< a ∈ [-1024..2147483647] < a ∈ [-1024..2147483647]
< b ∈ [-1023..2147483647] < b ∈ [-1023..2147483647]
< c ∈ [-1023..2147483647] < c ∈ [-1023..2147483647]
...@@ -21,7 +21,7 @@ ...@@ -21,7 +21,7 @@
> b ∈ [-181..1867] > b ∈ [-181..1867]
> c ∈ [-602..1446] > c ∈ [-602..1446]
> d ∈ [-190..1874] > d ∈ [-190..1874]
422c414 376c368
< d2 ∈ [-2147483648..1] < d2 ∈ [-2147483648..1]
--- ---
> d2 ∈ [-2468..1] > d2 ∈ [-2468..1]
tests/value/oracle_symblocs/octagons-pointers.res.oracle deleted 100644 → 0
+ 0
− 6
View file @ e8db19c3
34,35c34,35
< cmd - len ∈ {0}
< len - code ∈ {-2}
---
> len - cmd ∈ {0}
> code - len ∈ {2}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment