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

[Eva] Adds tests for the emission of overflow alarms on division and modulo.

parent 5766f031
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/value/div.i
+ 52
− 2
View file @ 041e1634
......@@ -2,13 +2,13 @@
STDOPT: #""
*/
volatile int nondet;
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
int a,b,d1,d2,d0,e;
int t[5]={1,2,3};
int *p;
void main (void) {
void test (void) {
int i;
volatile int c=0;
while (c+1)
......@@ -36,3 +36,53 @@ void main (void) {
d0 = 100 / (int)(&X);
e = - (int) &X;
}
/* Tests the emission of overflow alarms on a division x/y only if [x] may be
equal to MIN_INT and [y] may be equal to -1. Also tests the reduction of the
possible values of [x] or [y] when possible. Similar test in file modulo.i. */
void test_overflow_alarms (void) {
int min_int = -2147483648;
int min_one = -1;
int a = nondet ? min_int : 10;
int b = nondet ? -1 : 2;
int x = nondet;
int y = nondet;
int r = 0;
if (nondet) {
r = a / b; // Overflow alarm.
// No reduction as [a] and [b] cannot be reduced simultaneously.
Frama_C_show_each(a, b);
}
if (nondet) {
r = a / min_one; // Overflow alarm.
r = a / min_one; // No alarm if [a] has been reduced.
Frama_C_show_each_ten(a); // Check the reduction of [a].
}
if (nondet) {
r = min_int / b; // Overflow alarm.
r = min_int / b; // No alarm if [b] has been reduced.
Frama_C_show_each_two(b); // Check the reduction of [b]
}
if (nondet) {
r = x / min_one; // Overflow alarm.
r = x / min_one; // No alarm if [x] has been reduced.
Frama_C_show_each(x); // All integers except MIN_INT.
}
if (nondet) {
r = min_int / x; // Overflow alarm and division by zero alarm.
// All integers except -1 and 0, but not representable as an interval.
Frama_C_show_each(x);
}
if (nondet) {
r = min_int / min_one; // Invalid alarm.
Frama_C_show_each_BOTTOM(min_int, min_one);
}
// Overflow alarm and division by zero alarm,
// no possible reduction: [x] and [y] must be top_int as the end.
r = x / y;
}
void main (void) {
test();
test_overflow_alarms();
}
tests/value/modulo.i
+ 43
− 0
View file @ 041e1634
......@@ -161,6 +161,48 @@ void address_modulo(void) {
r = uaddr % i;
}
/* Tests the emission of overflow alarms on operation x%y only if [x] may be
equal to MIN_INT and [y] may be equal to -1. Also tests the reduction of the
possible values of [x] or [y] when possible. Similar test in file div.i. */
void test_overflow_alarms (void) {
int min_int = -2147483648;
int min_one = -1;
int a = v ? min_int : 10;
int b = v ? -1 : 2;
int x = v;
int y = v;
int r = 0;
if (v) {
r = a % b; // Overflow alarm.
// No reduction as [a] and [b] cannot be reduced simultaneously.
Frama_C_show_each(a, b);
}
if (v) {
r = a % min_one; // Overflow alarm.
r = a % min_one; // No alarm if [a] has been reduced.
Frama_C_show_each_ten(a); // Check the reduction of [a].
}
if (v) {
r = min_int % b; // Overflow alarm.
r = min_int % b; // No alarm if [b] has been reduced.
Frama_C_show_each_two(b); // Check the reduction of [b]
}
if (v) {
r = x % min_one; // Overflow alarm.
r = x % min_one; // No alarm if [x] has been reduced.
Frama_C_show_each(x); // All integers except MIN_INT.
}
if (v) {
r = min_int % x; // Overflow alarm and division by zero alarm.
// All integers except -1 and 0, but not representable as an interval.
Frama_C_show_each(x);
}
if (v) {
r = min_int % min_one; // Invalid alarm.
Frama_C_show_each_BOTTOM(min_int, min_one);
}
}
void main() {
if (v) { pgcd1(a, b); }
if (v) { pgcd2(a, b); }
......@@ -172,4 +214,5 @@ void main() {
extract_bits_modulo();
pos_rem();
address_modulo();
test_overflow_alarms();
}
tests/value/oracle/div.res.oracle
+ 90
− 3
View file @ 041e1634
......@@ -3,6 +3,7 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
X ∈ {0}
Y ∈ {0}
Z1 ∈ {0}
......@@ -24,6 +25,8 @@
[2] ∈ {3}
[3..4] ∈ {0}
p ∈ {0}
[eva] computing for function test <- main.
Called from div.i:86.
[eva:alarm] div.i:14: Warning: signed overflow. assert c + 1 ≤ 2147483647;
[eva:alarm] div.i:17: Warning: signed overflow. assert c + 2 ≤ 2147483647;
[eva] div.i:14: starting to merge loop iterations
......@@ -58,11 +61,37 @@
signed overflow. assert -((int)(&X)) ≤ 2147483647;
[eva:garbled-mix:write] div.i:37:
Assigning imprecise value to e because of arithmetic operation on addresses.
[eva] Recording results for test
[eva] Done for function test
[eva] computing for function test_overflow_alarms <- main.
Called from div.i:87.
[eva:alarm] div.i:52: Warning: signed overflow. assert a_0 / b_0 ≤ 2147483647;
[eva] div.i:54: Frama_C_show_each: {-2147483648; 10}, {-1; 2}
[eva:alarm] div.i:57: Warning:
signed overflow. assert a_0 / min_one ≤ 2147483647;
[eva] div.i:59: Frama_C_show_each_ten: {10}
[eva:alarm] div.i:62: Warning:
signed overflow. assert min_int / b_0 ≤ 2147483647;
[eva] div.i:64: Frama_C_show_each_two: {2}
[eva:alarm] div.i:67: Warning:
signed overflow. assert x / min_one ≤ 2147483647;
[eva] div.i:69: Frama_C_show_each: [-2147483647..2147483647]
[eva:alarm] div.i:72: Warning: division by zero. assert x ≢ 0;
[eva:alarm] div.i:72: Warning:
signed overflow. assert min_int / x ≤ 2147483647;
[eva] div.i:74: Frama_C_show_each: [-2147483648..2147483647]
[eva:alarm] div.i:77: Warning:
signed overflow. assert min_int / min_one ≤ 2147483647;
[eva:alarm] div.i:82: Warning: division by zero. assert y ≢ 0;
[eva:alarm] div.i:82: Warning: signed overflow. assert x / y ≤ 2147483647;
[eva] Recording results for test_overflow_alarms
[eva] Done for function test_overflow_alarms
[eva] Recording results for main
[eva] Done for function main
[eva] div.i:77: assertion 'Eva,signed_overflow' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
[eva:final-states] Values at end of function test:
X ∈ [--..--]
Y ∈ [-126..333],9%27
Z1 ∈ [-42..111],3%9
......@@ -81,10 +110,60 @@
e ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:37}) }}
p ∈ {{ &t[3] }}
c ∈ [--..--]
[eva:final-states] Values at end of function test_overflow_alarms:
min_int ∈ {-2147483648}
min_one ∈ {-1}
a_0 ∈ {-2147483648; 10}
b_0 ∈ {-1; 2}
x ∈ [--..--]
y ∈ [--..--]
r ∈ [--..--]
[eva:final-states] Values at end of function main:
X ∈ [--..--]
Y ∈ [-126..333],9%27
Z1 ∈ [-42..111],3%9
Z2 ∈ [-25..66]
T ∈ [34..493],7%27
U1 ∈ [11..164],2%9
U2 ∈ [6..98]
V ∈ [-125..334],10%27
W1 ∈ [-41..111]
W2 ∈ [-25..66]
a ∈ [-40000..40000]
b ∈ {{ garbled mix of &{Z2} (origin: Arithmetic {div.i:33}) }}
d1 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:35}) }}
d2 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:34}) }}
d0 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:36}) }}
e ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:37}) }}
p ∈ {{ &t[3] }}
[from] Computing for function test
[from] Done for function test
[from] Computing for function test_overflow_alarms
[from] Done for function test_overflow_alarms
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function test:
X FROM X (and SELF)
Y FROM X
Z1 FROM X
Z2 FROM X
T FROM X
U1 FROM X
U2 FROM X
V FROM X
W1 FROM X
W2 FROM X
a FROM X
b FROM X
d1 FROM \nothing
d2 FROM \nothing
d0 FROM \nothing
e FROM \nothing
p FROM \nothing
[from] Function test_overflow_alarms:
NO EFFECTS
[from] Function main:
X FROM X (and SELF)
Y FROM X
......@@ -104,7 +183,15 @@
e FROM \nothing
p FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
[inout] Out (internal) for function test:
X; Y; Z1; Z2; T; U1; U2; V; W1; W2; a; b; d1; d2; d0; e; p; c
[inout] Inputs for function main:
[inout] Inputs for function test:
X; Y; Z2; T; V
[inout] Out (internal) for function test_overflow_alarms:
min_int; min_one; a_0; tmp; b_0; tmp_0; x; y; r
[inout] Inputs for function test_overflow_alarms:
nondet
[inout] Out (internal) for function main:
X; Y; Z1; Z2; T; U1; U2; V; W1; W2; a; b; d1; d2; d0; e; p
[inout] Inputs for function main:
nondet; X; Y; Z2; T; V
tests/value/oracle/modulo.res.oracle
+ 51
− 12
View file @ 041e1634
......@@ -26,8 +26,8 @@
b ∈ [--..--]
i2 ∈ [--..--]
[eva] computing for function pgcd1 <- main.
Called from modulo.i:165.
[eva:alarm] modulo.i:165: Warning:
Called from modulo.i:207.
[eva:alarm] modulo.i:207: Warning:
function pgcd1: precondition got status unknown.
[eva] modulo.i:37: loop invariant got status valid.
[eva] modulo.i:38: loop invariant got status valid.
......@@ -40,8 +40,8 @@
[eva] Recording results for pgcd1
[eva] Done for function pgcd1
[eva] computing for function pgcd2 <- main.
Called from modulo.i:166.
[eva:alarm] modulo.i:166: Warning:
Called from modulo.i:208.
[eva:alarm] modulo.i:208: Warning:
function pgcd2: precondition got status unknown.
[eva] modulo.i:50: loop invariant got status valid.
[eva] modulo.i:53: Frama_C_show_each_2: [-10..10], [1..10], [-9..9]
......@@ -49,15 +49,15 @@
[eva] Recording results for pgcd2
[eva] Done for function pgcd2
[eva] computing for function pgcd3 <- main.
Called from modulo.i:167.
[eva:alarm] modulo.i:167: Warning:
Called from modulo.i:209.
[eva:alarm] modulo.i:209: Warning:
function pgcd3: precondition got status unknown.
[eva:alarm] modulo.i:63: Warning: division by zero. assert b_0 ≢ 0;
[eva] modulo.i:64: Frama_C_show_each_3: [-10..10], [-10..10], [-9..9]
[eva] Recording results for pgcd3
[eva] Done for function pgcd3
[eva] computing for function main2 <- main.
Called from modulo.i:169.
Called from modulo.i:211.
[eva:alarm] modulo.i:9: Warning: signed overflow. assert -2147483648 ≤ 4 * i;
[eva:alarm] modulo.i:9: Warning: signed overflow. assert 4 * i ≤ 2147483647;
[eva:alarm] modulo.i:10: Warning: signed overflow. assert -2147483648 ≤ 4 * i;
......@@ -69,12 +69,12 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function simultaneous_congruences <- main.
Called from modulo.i:170.
Called from modulo.i:212.
[eva:alarm] modulo.i:76: Warning: assertion got status unknown.
[eva] Recording results for simultaneous_congruences
[eva] Done for function simultaneous_congruences
[eva] computing for function shift_modulo <- main.
Called from modulo.i:171.
Called from modulo.i:213.
[eva:alarm] modulo.i:100: Warning: assertion got status unknown.
[eva:alarm] modulo.i:103: Warning:
signed overflow. assert (int)((int)(i * 12) + 5) << 25 ≤ 2147483647;
......@@ -83,19 +83,19 @@
[eva] Recording results for shift_modulo
[eva] Done for function shift_modulo
[eva] computing for function extract_bits_modulo <- main.
Called from modulo.i:172.
Called from modulo.i:214.
[eva:alarm] modulo.i:109: Warning: assertion got status unknown.
[eva] Recording results for extract_bits_modulo
[eva] Done for function extract_bits_modulo
[eva] computing for function pos_rem <- main.
Called from modulo.i:173.
Called from modulo.i:215.
[eva:alarm] modulo.i:137: Warning: assertion got status unknown.
[eva:alarm] modulo.i:142: Warning: assertion got status unknown.
[eva:alarm] modulo.i:146: Warning: assertion got status unknown.
[eva] Recording results for pos_rem
[eva] Done for function pos_rem
[eva] computing for function address_modulo <- main.
Called from modulo.i:174.
Called from modulo.i:216.
[eva:garbled-mix:write] modulo.i:158:
Assigning imprecise value to r because of arithmetic operation on addresses.
[eva:alarm] modulo.i:159: Warning: division by zero. assert i ≢ 0;
......@@ -111,8 +111,31 @@
Assigning imprecise value to r because of arithmetic operation on addresses.
[eva] Recording results for address_modulo
[eva] Done for function address_modulo
[eva] computing for function test_overflow_alarms <- main.
Called from modulo.i:217.
[eva:alarm] modulo.i:176: Warning:
signed overflow. assert a_0 / b_0 ≤ 2147483647;
[eva] modulo.i:178: Frama_C_show_each: {-2147483648; 10}, {-1; 2}
[eva:alarm] modulo.i:181: Warning:
signed overflow. assert a_0 / min_one ≤ 2147483647;
[eva] modulo.i:183: Frama_C_show_each_ten: {10}
[eva:alarm] modulo.i:186: Warning:
signed overflow. assert min_int / b_0 ≤ 2147483647;
[eva] modulo.i:188: Frama_C_show_each_two: {2}
[eva:alarm] modulo.i:191: Warning:
signed overflow. assert x / min_one ≤ 2147483647;
[eva] modulo.i:193: Frama_C_show_each: [-2147483647..2147483647]
[eva:alarm] modulo.i:196: Warning: division by zero. assert x ≢ 0;
[eva:alarm] modulo.i:196: Warning:
signed overflow. assert min_int / x ≤ 2147483647;
[eva] modulo.i:198: Frama_C_show_each: [-2147483648..2147483647]
[eva:alarm] modulo.i:201: Warning:
signed overflow. assert min_int / min_one ≤ 2147483647;
[eva] Recording results for test_overflow_alarms
[eva] Done for function test_overflow_alarms
[eva] Recording results for main
[eva] Done for function main
[eva] modulo.i:201: assertion 'Eva,signed_overflow' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function address_modulo:
......@@ -187,6 +210,14 @@
o1 ∈ [11..268435451],11%24
o2 ∈ [11..268435451],11%24
o3 ∈ [11..268435451],11%24
[eva:final-states] Values at end of function test_overflow_alarms:
min_int ∈ {-2147483648}
min_one ∈ {-1}
a_0 ∈ {-2147483648; 10}
b_0 ∈ {-1; 2}
x ∈ [--..--]
y ∈ [--..--]
r ∈ [-2147483647..0]
[eva:final-states] Values at end of function main:
A ∈ {0}
B ∈ {-3; 1}
......@@ -223,6 +254,8 @@
[from] Done for function shift_modulo
[from] Computing for function simultaneous_congruences
[from] Done for function simultaneous_congruences
[from] Computing for function test_overflow_alarms
[from] Done for function test_overflow_alarms
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
......@@ -261,6 +294,8 @@
NO EFFECTS
[from] Function simultaneous_congruences:
NO EFFECTS
[from] Function test_overflow_alarms:
NO EFFECTS
[from] Function main:
A FROM v
B FROM v
......@@ -317,6 +352,10 @@
n1; n2; n3; m1; m2; o1; o2; o3
[inout] Inputs for function simultaneous_congruences:
i2
[inout] Out (internal) for function test_overflow_alarms:
min_int; min_one; a_0; tmp; b_0; tmp_0; x; y; r
[inout] Inputs for function test_overflow_alarms:
v
[inout] Out (internal) for function main:
A; B; C; D; E; F; G; H; I; J; K; L; M; N; O; P; Q
[inout] Inputs for function main:
......
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