diff --git a/tests/value/domains.i b/tests/value/domains.i index cbb0f5f20a9dee7d263eff606510a57ba775fb5b..defe295b671a8d02072cef7f0ba5962ce1f40674 100644 --- a/tests/value/domains.i +++ b/tests/value/domains.i @@ -50,4 +50,9 @@ void main (int a) { Frama_C_domain_show_each(a, i, j, k, r); Frama_C_dump_each(); 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); } diff --git a/tests/value/oracle/domains.res.oracle b/tests/value/oracle/domains.res.oracle index b18995538801113b434bfd61172445ea64c4403d..55968e3431b11513fcc643d7834169af391b5f10 100644 --- a/tests/value/oracle/domains.res.oracle +++ b/tests/value/oracle/domains.res.oracle @@ -62,6 +62,7 @@ [65..99] ∈ [--..--] or UNINITIALIZED b1 ∈ {0; 1} b2 ∈ {0; 1} + scalar ∈ UNINITIALIZED # equality: {k = ((i - j) + 1) + j} # symbolic-locations: @@ -117,10 +118,24 @@ }, {}) b1 -> ({0; 1}, {}) - b2 -> ({0; 1}, {}) ]}, + b2 -> ({0; 1}, {}) + scalar -> (UNINITIALIZED, {}) ]}, None) ==END OF DUMP== [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] Done for function main [eva] ====== VALUES COMPUTED ====== @@ -135,6 +150,9 @@ [65..99] ∈ [--..--] or UNINITIALIZED b1 ∈ {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] Done for function main [from] ====== DEPENDENCIES COMPUTED ====== @@ -143,6 +161,6 @@ NO EFFECTS [from] ====== END OF DEPENDENCIES ====== [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: nondet diff --git a/tests/value/oracle/domains_dump_0 b/tests/value/oracle/domains_dump_0 index 243759089da3fcd59305557fa40fab8634a5e850..69dce4193ff046e66371f19194c77cb6cdfbbc42 100644 --- a/tests/value/oracle/domains_dump_0 +++ b/tests/value/oracle/domains_dump_0 @@ -11,6 +11,7 @@ t[0..63] ∈ [--..--] or UNINITIALIZED [65..99] ∈ [--..--] or UNINITIALIZED b1 ∈ {0; 1} b2 ∈ {0; 1} +scalar ∈ UNINITIALIZED # equality: {k = ((i - j) + 1) + j} # symbolic-locations: @@ -66,5 +67,6 @@ a[bits 0 to 2] ∈ {0} }, {}) b1 -> ({0; 1}, {}) - b2 -> ({0; 1}, {}) ]}, + b2 -> ({0; 1}, {}) + scalar -> (UNINITIALIZED, {}) ]}, None)