Skip to content
Snippets Groups Projects
Commit 638c7d98 authored by David Bühler's avatar David Bühler Committed by Andre Maroneze
Browse files

[Eva] Adds test printing the offsetmap of a scalar variable.

parent c4026863
No related branches found
No related tags found
No related merge requests found
...@@ -50,4 +50,9 @@ void main (int a) { ...@@ -50,4 +50,9 @@ void main (int a) {
Frama_C_domain_show_each(a, i, j, k, r); Frama_C_domain_show_each(a, i, j, k, r);
Frama_C_dump_each(); Frama_C_dump_each();
Frama_C_dump_each_file_domains_dump(); Frama_C_dump_each_file_domains_dump();
/* Tests printing offsetmap of scalar value. */
int scalar = 65537;
*(((char *)&scalar)+1) = 42;
Frama_C_domain_show_each(scalar);
} }
...@@ -62,6 +62,7 @@ ...@@ -62,6 +62,7 @@
[65..99] ∈ [--..--] or UNINITIALIZED [65..99] ∈ [--..--] or UNINITIALIZED
b1 ∈ {0; 1} b1 ∈ {0; 1}
b2 ∈ {0; 1} b2 ∈ {0; 1}
scalar ∈ UNINITIALIZED
# equality: # equality:
{k = ((i - j) + 1) + j} {k = ((i - j) + 1) + j}
# symbolic-locations: # symbolic-locations:
...@@ -117,10 +118,24 @@ ...@@ -117,10 +118,24 @@
}, },
{}) {})
b1 -> ({0; 1}, {}) b1 -> ({0; 1}, {})
b2 -> ({0; 1}, {}) ]}, b2 -> ({0; 1}, {})
scalar -> (UNINITIALIZED, {}) ]},
None) None)
==END OF DUMP== ==END OF DUMP==
[eva] domains.i:52: Dumping state in file 'domains_dump_0' [eva] domains.i:52: Dumping state in file 'domains_dump_0'
[eva] domains.i:57:
Frama_C_domain_show_each:
scalar : # cvalue: [bits 0 to 7]# ∈ {65537}%32, bits 0 to 7
[bits 8 to 15] ∈ {42}
[bits 16 to 31]# ∈ {65537}%32, bits 16 to 31
This amounts to: {76289}
# equality:
# symbolic-locations: (not implemented)
# octagon: (not implemented)
# gauges: (not implemented)
# sign: -0+
# bitwise: (not implemented)
# multidim: T
[eva] Recording results for main [eva] Recording results for main
[eva] Done for function main [eva] Done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
...@@ -135,6 +150,9 @@ ...@@ -135,6 +150,9 @@
[65..99] ∈ [--..--] or UNINITIALIZED [65..99] ∈ [--..--] or UNINITIALIZED
b1 ∈ {0; 1} b1 ∈ {0; 1}
b2 ∈ {0; 1} b2 ∈ {0; 1}
scalar[bits 0 to 7]# ∈ {65537}%32, bits 0 to 7
[bits 8 to 15] ∈ {42}
[bits 16 to 31]# ∈ {65537}%32, bits 16 to 31
[from] Computing for function main [from] Computing for function main
[from] Done for function main [from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ====== [from] ====== DEPENDENCIES COMPUTED ======
...@@ -143,6 +161,6 @@ ...@@ -143,6 +161,6 @@
NO EFFECTS NO EFFECTS
[from] ====== END OF DEPENDENCIES ====== [from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main: [inout] Out (internal) for function main:
a; i; j; k; r; t[0..99]; b1; b2 a; i; j; k; r; t[0..99]; b1; b2; scalar
[inout] Inputs for function main: [inout] Inputs for function main:
nondet nondet
...@@ -11,6 +11,7 @@ t[0..63] ∈ [--..--] or UNINITIALIZED ...@@ -11,6 +11,7 @@ t[0..63] ∈ [--..--] or UNINITIALIZED
[65..99] ∈ [--..--] or UNINITIALIZED [65..99] ∈ [--..--] or UNINITIALIZED
b1 ∈ {0; 1} b1 ∈ {0; 1}
b2 ∈ {0; 1} b2 ∈ {0; 1}
scalar ∈ UNINITIALIZED
# equality: # equality:
{k = ((i - j) + 1) + j} {k = ((i - j) + 1) + j}
# symbolic-locations: # symbolic-locations:
...@@ -66,5 +67,6 @@ a[bits 0 to 2] ∈ {0} ...@@ -66,5 +67,6 @@ a[bits 0 to 2] ∈ {0}
}, },
{}) {})
b1 -> ({0; 1}, {}) b1 -> ({0; 1}, {})
b2 -> ({0; 1}, {}) ]}, b2 -> ({0; 1}, {})
scalar -> (UNINITIALIZED, {}) ]},
None) None)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment