From 1200858bafe75e52b6cfed069d5362aaefeb9d11 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 3 Jan 2019 12:42:48 +0100
Subject: [PATCH] [Ival] Dust off bitwise tests
---
tests/value/bitwise.i | 108 ++++++++--
tests/value/bitwise_or.c | 56 -----
tests/value/oracle/bitwise.res.oracle | 262 ++++++++++++++++-------
tests/value/oracle/bitwise_or.res.oracle | 72 -------
4 files changed, 274 insertions(+), 224 deletions(-)
delete mode 100644 tests/value/bitwise_or.c
delete mode 100644 tests/value/oracle/bitwise_or.res.oracle
diff --git a/tests/value/bitwise.i b/tests/value/bitwise.i
index 765c7bcb82a..7803ea7f36d 100644
--- a/tests/value/bitwise.i
+++ b/tests/value/bitwise.i
@@ -1,6 +1,80 @@
+/* run.config*
+ STDOPT: +"-big-ints-hex 256"
+*/
+
+/*@ assigns \result \from min, max;
+ ensures min <= \result <= max ;
+ */
+int Frama_C_interval(int min, int max);
+
+
volatile long v;
-
-void main_and_or_rel(void)
+volatile unsigned char input[3];
+
+
+extern unsigned short s;
+
+void test1(void) {
+ int or1, or2, or3, or4, or5;
+ int and1, and2, and3, and4, xor1, xor2;
+ unsigned int uand1, uand2, uand3, uand4, uand5;
+ int a,b,c,d,e;
+
+ a = Frama_C_interval(3,17);
+ b = Frama_C_interval(-3,17);
+ c = Frama_C_interval(13,27);
+ or1 = a | b;
+ or2 = a | c;
+ or3 = b | c;
+
+ and1 = a & b;
+ and2 = a & c;
+ and3 = b & c;
+
+ uand4 = 0xFFFFFFF8U & (unsigned int) c;
+
+ xor1 = a ^ a;
+ xor2 = a ^ b;
+
+ unsigned i1 = s * 2;
+ unsigned i2 = s * 4;
+ unsigned v1 = i1 & i2;
+ unsigned v2 = i1 | i2;
+
+ unsigned mask07 = (16 * s + 13) & 0x7;
+ unsigned mask0f = (16 * s + 13) & 0xF;
+ unsigned mask1f = (16 * s + 13) & 0x1F;
+}
+
+void test2(void) {
+ int x = Frama_C_interval(62,110) & ~(7);
+}
+
+void test3(void) {
+ int x = (input[0] & 0x10 ? -1^255 : 0) | input[1];
+ int y = (input[0] & 0x20 ? -1^255 : 0) | input[2];
+}
+
+int test4(void)
+{
+ unsigned something = v;
+ //@ slevel 2;
+ //@ assert something >= 0x80000000 || something < 0x80000000;
+ unsigned topBitOnly = something & 0x80000000;
+ Frama_C_show_each_1(something,topBitOnly);
+ something ^= topBitOnly;
+ Frama_C_show_each_2(something,something & 0x80000000,topBitOnly);
+ if (something & 0x80000000) {
+ Frama_C_show_each_true(something);
+ return 0;
+ }
+ else {
+ Frama_C_show_each_false(something);
+ return 1;
+ }
+}
+
+void and_or_rel(void)
{
long x, r1, r2, r3;
@@ -19,13 +93,13 @@ void main_and_or_rel(void)
}
-void main_bitwise() {
+void double_neg() {
unsigned int i = 5;
unsigned int j = ~i;
int k = ~(int)i;
}
-void main_bug1()
+void bug1()
{
unsigned char msb = 3 << 1;
unsigned char lsb = 3;
@@ -35,22 +109,22 @@ void main_bug1()
par = (unsigned char)(((int)par & 0x0F) ^ ((int)par >> 4));
}
-void main_bug2() {
+void bug2() {
int t = v ? 1 : 2;
if ((t & 7) == 1) { Frama_C_show_each_then(); } else { Frama_C_show_each_else(); }
}
/* See issue Value/Value#82 on the bitwise domain. */
-void main_bug3 () {
+void bug3 () {
unsigned long l_1180 = 10022045811482781039u;
unsigned long foo = ~ (l_1180 ^ (unsigned long)(l_1180 != 0UL));
- Frama_C_dump_each();
+ Frama_C_show_each(l_1180, foo);
foo ^= 0;
}
/* Due to signedness mismatches, the bitwise domain incorrectly returned
Bottom on one of the branches. */
-void main_bug4() {
+void bug4() {
int g_2 = v ? -1 : 0;
short tmp = -0x1578;
if ((g_2 | (int)tmp) & 1) {
@@ -60,11 +134,15 @@ void main_bug4() {
}
}
-void main() {
- main_and_or_rel();
- main_bitwise();
- main_bug1();
- main_bug2();
- main_bug3();
- main_bug4();
+void main(void) {
+ test1();
+ test2();
+ test3();
+ test4();
+ and_or_rel();
+ double_neg();
+ bug1();
+ bug2();
+ bug3();
+ bug4();
}
diff --git a/tests/value/bitwise_or.c b/tests/value/bitwise_or.c
deleted file mode 100644
index 0a89e7c3010..00000000000
--- a/tests/value/bitwise_or.c
+++ /dev/null
@@ -1,56 +0,0 @@
-/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -big-ints-hex 256 -eva @VALUECONFIG@ -journal-disable
-*/
-#include "__fc_builtin.h"
-
-extern unsigned short s;
-
-void f1(void) {
- int or1, or2, or3, or4, or5;
- int and1, and2, and3, and4, xor1, xor2;
- unsigned int uand1, uand2, uand3, uand4, uand5;
- int a,b,c,d,e;
-
- a = Frama_C_interval(3,17);
- b = Frama_C_interval(-3,17);
- c = Frama_C_interval(13,27);
- or1 = a | b;
- or2 = a | c;
- or3 = b | c;
-
- and1 = a & b;
- and2 = a & c;
- and3 = b & c;
-
- uand4 = 0xFFFFFFF8U & (unsigned int) c;
-
- xor1 = a ^ a;
- xor2 = a ^ b;
-
- unsigned i1 = s * 2;
- unsigned i2 = s * 4;
- unsigned v1 = i1 & i2;
- unsigned v2 = i1 | i2;
-
- unsigned mask07 = (16 * s + 13) & 0x7;
- unsigned mask0f = (16 * s + 13) & 0xF;
- unsigned mask1f = (16 * s + 13) & 0x1F;
-}
-
-void f2(void) {
- int x = Frama_C_interval(62,110) & ~(7);
-}
-
-volatile unsigned char t[3];
-
-void f3(void) {
- int x = (t[0] & 0x10 ? -1^255 : 0) | t[1];
- int y = (t[0] & 0x20 ? -1^255 : 0) | t[2];
-}
-
-void main(void) {
- f1();
- f2();
- f3();
-}
-
diff --git a/tests/value/oracle/bitwise.res.oracle b/tests/value/oracle/bitwise.res.oracle
index 029bed27175..29d9bbe2322 100644
--- a/tests/value/oracle/bitwise.res.oracle
+++ b/tests/value/oracle/bitwise.res.oracle
@@ -4,126 +4,226 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
-[eva] computing for function main_and_or_rel <- main.
- Called from tests/value/bitwise.i:64.
-[eva:alarm] tests/value/bitwise.i:13: Warning: assertion got status unknown.
-[eva] Recording results for main_and_or_rel
-[eva] Done for function main_and_or_rel
-[eva] computing for function main_bitwise <- main.
- Called from tests/value/bitwise.i:65.
-[eva] Recording results for main_bitwise
-[eva] Done for function main_bitwise
-[eva] computing for function main_bug1 <- main.
- Called from tests/value/bitwise.i:66.
-[eva] Recording results for main_bug1
-[eva] Done for function main_bug1
-[eva] computing for function main_bug2 <- main.
- Called from tests/value/bitwise.i:67.
-[eva] tests/value/bitwise.i:40: Frama_C_show_each_then:
-[eva] tests/value/bitwise.i:40: Frama_C_show_each_else:
-[eva] Recording results for main_bug2
-[eva] Done for function main_bug2
-[eva] computing for function main_bug3 <- main.
- Called from tests/value/bitwise.i:68.
-[eva] tests/value/bitwise.i:47:
- Frama_C_dump_each:
- # Cvalue domain:
- v ∈ [--..--]
- l_1180 ∈ {69166447}
- foo ∈ {4225800849}
- ==END OF DUMP==
-[eva] Recording results for main_bug3
-[eva] Done for function main_bug3
-[eva] computing for function main_bug4 <- main.
- Called from tests/value/bitwise.i:69.
-[eva] tests/value/bitwise.i:57: Frama_C_show_each_then:
-[eva] tests/value/bitwise.i:59: Frama_C_show_each_else:
-[eva] Recording results for main_bug4
-[eva] Done for function main_bug4
+ input[0..2] ∈ [--..--]
+ s ∈ [--..--]
+[eva] computing for function test1 <- main.
+ Called from tests/value/bitwise.i:138.
+[eva] computing for function Frama_C_interval <- test1 <- main.
+ Called from tests/value/bitwise.i:23.
+[eva] using specification for function Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test1 <- main.
+ Called from tests/value/bitwise.i:24.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test1 <- main.
+ Called from tests/value/bitwise.i:25.
+[eva] Done for function Frama_C_interval
+[eva] Recording results for test1
+[eva] Done for function test1
+[eva] computing for function test2 <- main.
+ Called from tests/value/bitwise.i:139.
+[eva] computing for function Frama_C_interval <- test2 <- main.
+ Called from tests/value/bitwise.i:50.
+[eva] Done for function Frama_C_interval
+[eva] Recording results for test2
+[eva] Done for function test2
+[eva] computing for function test3 <- main.
+ Called from tests/value/bitwise.i:140.
+[eva] Recording results for test3
+[eva] Done for function test3
+[eva] computing for function test4 <- main.
+ Called from tests/value/bitwise.i:141.
+[eva] tests/value/bitwise.i:62: assertion got status valid.
+[eva] tests/value/bitwise.i:64: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
+[eva] tests/value/bitwise.i:64:
+ Frama_C_show_each_1: [0x80000000..0xFFFFFFFF], {0x80000000}
+[eva] tests/value/bitwise.i:66: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
+[eva] tests/value/bitwise.i:66:
+ Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0x80000000}
+[eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
+[eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
+[eva] Recording results for test4
+[eva] Done for function test4
+[eva] computing for function and_or_rel <- main.
+ Called from tests/value/bitwise.i:142.
+[eva:alarm] tests/value/bitwise.i:87: Warning: assertion got status unknown.
+[eva] Recording results for and_or_rel
+[eva] Done for function and_or_rel
+[eva] computing for function double_neg <- main.
+ Called from tests/value/bitwise.i:143.
+[eva] Recording results for double_neg
+[eva] Done for function double_neg
+[eva] computing for function bug1 <- main.
+ Called from tests/value/bitwise.i:144.
+[eva] Recording results for bug1
+[eva] Done for function bug1
+[eva] computing for function bug2 <- main.
+ Called from tests/value/bitwise.i:145.
+[eva] tests/value/bitwise.i:114: Frama_C_show_each_then:
+[eva] tests/value/bitwise.i:114: Frama_C_show_each_else:
+[eva] Recording results for bug2
+[eva] Done for function bug2
+[eva] computing for function bug3 <- main.
+ Called from tests/value/bitwise.i:146.
+[eva] tests/value/bitwise.i:121: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
+[eva] Recording results for bug3
+[eva] Done for function bug3
+[eva] computing for function bug4 <- main.
+ Called from tests/value/bitwise.i:147.
+[eva] tests/value/bitwise.i:131: Frama_C_show_each_then:
+[eva] tests/value/bitwise.i:133: Frama_C_show_each_else:
+[eva] Recording results for bug4
+[eva] Done for function bug4
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main_and_or_rel:
+[eva:final-states] Values at end of function and_or_rel:
x ∈ [20..40]
r1 ∈ [17..63] or UNINITIALIZED
r2 ∈ [20..40] or UNINITIALIZED
r3 ∈ [24..37] or UNINITIALIZED
-[eva:final-states] Values at end of function main_bitwise:
- i ∈ {5}
- j ∈ {4294967290}
- k ∈ {-6}
-[eva:final-states] Values at end of function main_bug1:
+[eva:final-states] Values at end of function bug1:
msb ∈ {6}
lsb ∈ {3}
par ∈ {5}
p1 ∈ {5}
p2 ∈ {0}
-[eva:final-states] Values at end of function main_bug2:
+[eva:final-states] Values at end of function bug2:
t ∈ {1; 2}
-[eva:final-states] Values at end of function main_bug3:
- l_1180 ∈ {69166447}
- foo ∈ {4225800849}
-[eva:final-states] Values at end of function main_bug4:
+[eva:final-states] Values at end of function bug3:
+ l_1180 ∈ {0x41F656F}
+ foo ∈ {0xFBE09A91}
+[eva:final-states] Values at end of function bug4:
g_2 ∈ {-1; 0}
- tmp_0 ∈ {-5496}
+ tmp_0 ∈ {-0x1578}
+[eva:final-states] Values at end of function double_neg:
+ i ∈ {5}
+ j ∈ {0xFFFFFFFA}
+ k ∈ {-6}
+[eva:final-states] Values at end of function test1:
+ or1 ∈ [-3..31]
+ or2 ∈ [13..31]
+ or3 ∈ [-3..31]
+ and1 ∈ [0..17]
+ and2 ∈ [0..17]
+ and3 ∈ [0..27]
+ xor1 ∈ [0..31]
+ xor2 ∈ [-20..31]
+ uand4 ∈ {8; 16; 24}
+ a ∈ [3..17]
+ b ∈ [-3..17]
+ c ∈ [13..27]
+ i1 ∈ [0..0x1FFFE],0%2
+ i2 ∈ [0..0x3FFFC],0%4
+ v1 ∈ [0..0x1FFFC],0%4
+ v2 ∈ [0..0x3FFFE],0%2
+ mask07 ∈ {5}
+ mask0f ∈ {13}
+ mask1f ∈ {13; 29}
+[eva:final-states] Values at end of function test2:
+ x ∈ {56; 64; 72; 80; 88; 96; 104}
+[eva:final-states] Values at end of function test3:
+ x ∈ [-256..255]
+ y ∈ [-256..255]
+[eva:final-states] Values at end of function test4:
+ something ∈ [0..0x7FFFFFFF]
+ topBitOnly ∈ {0; 0x80000000}
+ __retres ∈ {1}
[eva:final-states] Values at end of function main:
-[from] Computing for function main_and_or_rel
-[from] Done for function main_and_or_rel
-[from] Computing for function main_bitwise
-[from] Done for function main_bitwise
-[from] Computing for function main_bug1
-[from] Done for function main_bug1
-[from] Computing for function main_bug2
-[from] Done for function main_bug2
-[from] Computing for function main_bug3
-[from] Done for function main_bug3
-[from] Computing for function main_bug4
-[from] Done for function main_bug4
+[from] Computing for function and_or_rel
+[from] Done for function and_or_rel
+[from] Computing for function bug1
+[from] Done for function bug1
+[from] Computing for function bug2
+[from] Done for function bug2
+[from] Computing for function bug3
+[from] Done for function bug3
+[from] Computing for function bug4
+[from] Done for function bug4
+[from] Computing for function double_neg
+[from] Done for function double_neg
+[from] Computing for function test1
+[from] Computing for function Frama_C_interval <-test1
+[from] Done for function Frama_C_interval
+[from] Done for function test1
+[from] Computing for function test2
+[from] Done for function test2
+[from] Computing for function test3
+[from] Done for function test3
+[from] Computing for function test4
+[from] Done for function test4
[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 main_and_or_rel:
+[from] Function Frama_C_interval:
+ \result FROM min; max
+[from] Function and_or_rel:
+ NO EFFECTS
+[from] Function bug1:
+ NO EFFECTS
+[from] Function bug2:
+ NO EFFECTS
+[from] Function bug3:
NO EFFECTS
-[from] Function main_bitwise:
+[from] Function bug4:
NO EFFECTS
-[from] Function main_bug1:
+[from] Function double_neg:
NO EFFECTS
-[from] Function main_bug2:
+[from] Function test1:
NO EFFECTS
-[from] Function main_bug3:
+[from] Function test2:
NO EFFECTS
-[from] Function main_bug4:
+[from] Function test3:
NO EFFECTS
+[from] Function test4:
+ \result FROM v
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main_and_or_rel:
+[inout] Out (internal) for function and_or_rel:
x; r1; r2; r3
-[inout] Inputs for function main_and_or_rel:
+[inout] Inputs for function and_or_rel:
v
-[inout] Out (internal) for function main_bitwise:
- i; j; k
-[inout] Inputs for function main_bitwise:
- \nothing
-[inout] Out (internal) for function main_bug1:
+[inout] Out (internal) for function bug1:
msb; lsb; par; p1; p2
-[inout] Inputs for function main_bug1:
+[inout] Inputs for function bug1:
\nothing
-[inout] Out (internal) for function main_bug2:
+[inout] Out (internal) for function bug2:
t; tmp
-[inout] Inputs for function main_bug2:
+[inout] Inputs for function bug2:
v
-[inout] Out (internal) for function main_bug3:
+[inout] Out (internal) for function bug3:
l_1180; foo
-[inout] Inputs for function main_bug3:
+[inout] Inputs for function bug3:
\nothing
-[inout] Out (internal) for function main_bug4:
+[inout] Out (internal) for function bug4:
g_2; tmp; tmp_0
-[inout] Inputs for function main_bug4:
+[inout] Inputs for function bug4:
+ v
+[inout] Out (internal) for function double_neg:
+ i; j; k
+[inout] Inputs for function double_neg:
+ \nothing
+[inout] Out (internal) for function test1:
+ or1; or2; or3; and1; and2; and3; xor1; xor2; uand4; a; b; c; i1; i2;
+ v1; v2; mask07; mask0f; mask1f
+[inout] Inputs for function test1:
+ s
+[inout] Out (internal) for function test2:
+ x; tmp
+[inout] Inputs for function test2:
+ \nothing
+[inout] Out (internal) for function test3:
+ x; tmp; y; tmp_0
+[inout] Inputs for function test3:
+ input[0..2]
+[inout] Out (internal) for function test4:
+ something; topBitOnly; __retres
+[inout] Inputs for function test4:
v
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
- v
+ v; input[0..2]; s
diff --git a/tests/value/oracle/bitwise_or.res.oracle b/tests/value/oracle/bitwise_or.res.oracle
deleted file mode 100644
index 3a0e350f43a..00000000000
--- a/tests/value/oracle/bitwise_or.res.oracle
+++ /dev/null
@@ -1,72 +0,0 @@
-[kernel] Parsing tests/value/bitwise_or.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- s ∈ [--..--]
- t[0..2] ∈ [--..--]
-[eva] computing for function f1 <- main.
- Called from tests/value/bitwise_or.c:52.
-[eva] computing for function Frama_C_interval <- f1 <- main.
- Called from tests/value/bitwise_or.c:14.
-[eva] using specification for function Frama_C_interval
-[eva] tests/value/bitwise_or.c:14:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- f1 <- main.
- Called from tests/value/bitwise_or.c:15.
-[eva] tests/value/bitwise_or.c:15:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- f1 <- main.
- Called from tests/value/bitwise_or.c:16.
-[eva] tests/value/bitwise_or.c:16:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] Recording results for f1
-[eva] Done for function f1
-[eva] computing for function f2 <- main.
- Called from tests/value/bitwise_or.c:53.
-[eva] computing for function Frama_C_interval <- f2 <- main.
- Called from tests/value/bitwise_or.c:41.
-[eva] tests/value/bitwise_or.c:41:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] Recording results for f2
-[eva] Done for function f2
-[eva] computing for function f3 <- main.
- Called from tests/value/bitwise_or.c:54.
-[eva] Recording results for f3
-[eva] Done for function f3
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f1:
- Frama_C_entropy_source ∈ [--..--]
- or1 ∈ [-3..31]
- or2 ∈ [13..31]
- or3 ∈ [-3..31]
- and1 ∈ [0..17]
- and2 ∈ [0..17]
- and3 ∈ [0..27]
- xor1 ∈ [0..31]
- xor2 ∈ [-20..31]
- uand4 ∈ {8; 16; 24}
- a ∈ [3..17]
- b ∈ [-3..17]
- c ∈ [13..27]
- i1 ∈ [0..0x1FFFE],0%2
- i2 ∈ [0..0x3FFFC],0%4
- v1 ∈ [0..0x1FFFC],0%4
- v2 ∈ [0..0x3FFFE],0%2
- mask07 ∈ {5}
- mask0f ∈ {13}
- mask1f ∈ {13; 29}
-[eva:final-states] Values at end of function f2:
- Frama_C_entropy_source ∈ [--..--]
- x ∈ {56; 64; 72; 80; 88; 96; 104}
-[eva:final-states] Values at end of function f3:
- x ∈ [-256..255]
- y ∈ [-256..255]
-[eva:final-states] Values at end of function main:
- Frama_C_entropy_source ∈ [--..--]
--
GitLab