Skip to content
Snippets Groups Projects
Commit 76c3e581 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Merge branch 'feature/eva/bitwise-endianess' into 'master' 

[Eva] Bitwise domain: fixes interpretation of shift and cast on big-endian architectures

Closes #1201

See merge request frama-c/frama-c!4015
parents 6d0b4df0 fab82035
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 613 additions and 114 deletions
src/plugins/eva/values/offsm_value.ml
+ 50
− 59
View file @ 76c3e581
......@@ -274,71 +274,61 @@ let bitwise_and = CacheAnd.merge bitwise_and
let bitwise_xor = CacheXor.merge bitwise_xor
(** Sign extension *)
let offsm_sign_extension sign_bit size =
let i = match sign_bit with
| `Zero -> Ival.zero
| `One -> Ival.minus_one
| `ZeroOne -> Ival.(join zero minus_one)
in
let v_extend = V_Or_Uninitialized.initialized (V.inject_ival i) in
V_Offsetmap.create ~size v_extend ~size_v:size
(** Shifts *)
type shift = SLeft of Int.t | SRight of Int.t * bool
(* Shift implemented as an an offsetmap copy then paste. *)
let shift size o shift =
let r = default size in
match shift with
| SLeft n ->
if Int.lt n size then
let size_copy = Int.sub size n in
let data = basic_copy ~size:size_copy o in
basic_paste ~start:n ~src:data ~size_src:size_copy r
else r (* Guaranteed undefined behavior ; we don't care about the result. *)
| SRight (n, signed) ->
if Int.lt n size then
let size_copy = Int.sub size n in
let data = basic_copy ~start:n ~size:size_copy o in
let o' = basic_paste ~src:data ~size_src:size_copy r in
if signed then
let sign_bit = read_bit o (Int.pred size) in
if sign_bit <> `Zero then
(* We need to preserve the sign. Add {-1} or {0; -1} on the leftmost
bits *)
let size_ext = Int.sub size size_copy in
let ext = offsm_sign_extension sign_bit size_ext in
basic_paste ~start:size_copy ~src:ext ~size_src:size_ext o'
else
o'
else
o'
else r (* Guaranteed undefined behavior ; we don't care about the result. *)
type shift_direction = Left | Right
(* The value of the sign bit, expressed as a cvalue. *)
let sign_bit size offsm =
let sign_bit =
if Cil.theMachine.theMachine.little_endian
then Int.pred size
else Int.zero
in
let sign_v = basic_find ~start:sign_bit ~size:Integer.one offsm in
Cvalue.V_Or_Uninitialized.get_v sign_v
(* Creates an offsetmap of size [size] filled with the sign bit of [offsm]. *)
let signed_default ~size ~size_offsm offsm =
let default_v = sign_bit size_offsm offsm in
let v = V_Or_Uninitialized.initialized default_v in
V_Offsetmap.create ~size ~size_v:Int.one v
let shift ~size ~signed offsm shift_direction n =
let result =
if signed && shift_direction = Right
then signed_default ~size ~size_offsm:size offsm
else default size
in
if Int.lt n Int.zero || Int.ge n size
then result (* Undefined behavior: we don't care about the result. *)
else
let size_copy = Int.sub size n in
let little_endian = Cil.theMachine.theMachine.little_endian in
let start_copy, start_paste =
if (shift_direction = Left) = little_endian
then Int.zero, n
else n, Int.zero
in
let data = basic_copy ~start:start_copy ~size:size_copy offsm in
basic_paste ~start:start_paste ~src:data ~size_src:size_copy result
(** Casts *)
let cast ~old_size ~new_size ~signed o =
if Int.equal old_size new_size then o
let cast ~old_size ~new_size ~signed offsm =
let little_endian = Cil.theMachine.theMachine.little_endian in
if Int.equal old_size new_size then offsm
else if Int.lt new_size old_size then (* Truncation *)
basic_copy ~size:new_size o
let start = if little_endian then Int.zero else Int.sub old_size new_size in
basic_copy ~start ~size:new_size offsm
else (* Extension *)
if signed then (* need to check the sign and extend accordingly *)
(* Original bits, extended with zeros *)
let r = default new_size in
let r_o = basic_paste ~src:o ~size_src:old_size r in
(* Bits of sign extension *)
let sign_bit = read_bit o (Int.pred old_size) in
let size_ext = Int.sub new_size old_size in
let ext = offsm_sign_extension sign_bit size_ext in
basic_paste ~start:old_size ~src:ext ~size_src:size_ext r_o
else
let r = default new_size in
basic_paste ~src:o ~size_src:old_size r
let result =
if signed
then signed_default ~size:new_size ~size_offsm:old_size offsm
else default new_size
in
let start = if little_endian then Int.zero else Int.sub new_size old_size in
basic_paste ~start ~src:offsm ~size_src:old_size result
(** Binary not *)
......@@ -539,9 +529,10 @@ module CvalueOffsm : Abstract.Value.Internal with type t = V.t * offsm_or_top
try
let i = V.project_ival v_r in
let i = Ival.project_int i in
let size = size typ in
let signed = Bit_utils.is_signed_int_enum_pointer typ in
let shiftn = if op = Shiftlt then SLeft i else SRight (i, signed) in
let o = shift (size typ) (to_offsm typ l) shiftn in
let dir = if op = Shiftlt then Left else Right in
let o = shift ~size ~signed (to_offsm typ l) dir i in
Main_values.CVal.forward_binop typ op v_l v_r >>-: fun v ->
v, O o
with V.Not_based_on_null | Ival.Not_Singleton_Int ->
......
tests/value/bitwise.i
+ 1
− 0
View file @ 76c3e581
/* run.config*
STDOPT: +"-big-ints-hex 256"
STDOPT: +"-big-ints-hex 256 -machdep ppc_32"
*/
/*@ assigns \result \from a, b;
......
tests/value/bitwise_pointer.i
+ 1
− 1
View file @ 76c3e581
/* run.config*
STDOPT: #"-inout"
STDOPT: #"-inout -machdep ppc_32"
*/
char t[100]={0,1,2,3,4,5,6,7,8,9};
......
tests/value/bitwise_reduction.i
+ 1
− 0
View file @ 76c3e581
/* run.config*
STDOPT: +"-big-ints-hex 255"
STDOPT: +"-big-ints-hex 255 -machdep ppc_32"
*/
volatile v;
......
tests/value/oracle/bitwise.res.oracle → tests/value/oracle/bitwise.0.res.oracle
+ 39
− 39
View file @ 76c3e581
......@@ -7,15 +7,10 @@
input[0..2] ∈ [--..--]
s ∈ [--..--]
[eva] computing for function test1 <- main.
Called from bitwise.i:177.
[eva] computing for function Frama_C_interval <- test1 <- main.
Called from bitwise.i:28.
[eva] using specification for function Frama_C_interval
[eva] bitwise.i:28:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
Called from bitwise.i:178.
[eva] computing for function Frama_C_interval <- test1 <- main.
Called from bitwise.i:29.
[eva] using specification for function Frama_C_interval
[eva] bitwise.i:29:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
......@@ -24,85 +19,90 @@
[eva] bitwise.i:30:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test1 <- main.
Called from bitwise.i:31.
[eva] bitwise.i:31:
function Frama_C_interval: precondition 'order' got status valid.
[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 bitwise.i:178.
Called from bitwise.i:179.
[eva] computing for function Frama_C_interval <- test2 <- main.
Called from bitwise.i:55.
[eva] bitwise.i:55:
Called from bitwise.i:56.
[eva] bitwise.i:56:
function Frama_C_interval: precondition 'order' got status valid.
[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 bitwise.i:179.
Called from bitwise.i:180.
[eva] Recording results for test3
[eva] Done for function test3
[eva] computing for function test4 <- main.
Called from bitwise.i:180.
[eva] bitwise.i:67: assertion got status valid.
[eva] bitwise.i:69: Frama_C_show_each_1: [0x80000000..0xFFFFFFFF], {0x80000000}
[eva] bitwise.i:69: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
[eva] bitwise.i:71: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0x80000000}
[eva] bitwise.i:71: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
[eva] bitwise.i:77: Frama_C_show_each_false: [0..0x7FFFFFFF]
[eva] bitwise.i:77: Frama_C_show_each_false: [0..0x7FFFFFFF]
Called from bitwise.i:181.
[eva] bitwise.i:68: assertion got status valid.
[eva] bitwise.i:70: Frama_C_show_each_1: [0x80000000..0xFFFFFFFF], {0x80000000}
[eva] bitwise.i:70: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
[eva] bitwise.i:72: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0x80000000}
[eva] bitwise.i:72: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
[eva] bitwise.i:78: Frama_C_show_each_false: [0..0x7FFFFFFF]
[eva] bitwise.i:78: Frama_C_show_each_false: [0..0x7FFFFFFF]
[eva] Recording results for test4
[eva] Done for function test4
[eva] computing for function test5 <- main.
Called from bitwise.i:181.
Called from bitwise.i:182.
[eva] computing for function Frama_C_nondet <- test5 <- main.
Called from bitwise.i:84.
Called from bitwise.i:85.
[eva] using specification for function Frama_C_nondet
[eva] Done for function Frama_C_nondet
[eva] computing for function Frama_C_nondet <- test5 <- main.
Called from bitwise.i:85.
Called from bitwise.i:86.
[eva] Done for function Frama_C_nondet
[eva] Recording results for test5
[eva] Done for function test5
[eva] computing for function and_or_rel <- main.
Called from bitwise.i:182.
[eva:alarm] bitwise.i:101: Warning: assertion got status unknown.
Called from bitwise.i:183.
[eva:alarm] bitwise.i:102: 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 bitwise.i:183.
Called from bitwise.i:184.
[eva] Recording results for double_neg
[eva] Done for function double_neg
[eva] computing for function bug1 <- main.
Called from bitwise.i:184.
Called from bitwise.i:185.
[eva] Recording results for bug1
[eva] Done for function bug1
[eva] computing for function bug2 <- main.
Called from bitwise.i:185.
[eva] bitwise.i:128: Frama_C_show_each_then:
[eva] bitwise.i:128: Frama_C_show_each_else:
Called from bitwise.i:186.
[eva] bitwise.i:129: Frama_C_show_each_then:
[eva] bitwise.i:129: Frama_C_show_each_else:
[eva] Recording results for bug2
[eva] Done for function bug2
[eva] computing for function bug3 <- main.
Called from bitwise.i:186.
[eva] bitwise.i:135: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
Called from bitwise.i:187.
[eva] bitwise.i:136: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
[eva] Recording results for bug3
[eva] Done for function bug3
[eva] computing for function bug4 <- main.
Called from bitwise.i:187.
[eva] bitwise.i:145: Frama_C_show_each_then:
[eva] bitwise.i:147: Frama_C_show_each_else:
Called from bitwise.i:188.
[eva] bitwise.i:146: Frama_C_show_each_then:
[eva] bitwise.i:148: Frama_C_show_each_else:
[eva] Recording results for bug4
[eva] Done for function bug4
[eva] computing for function bug5 <- main.
Called from bitwise.i:188.
[eva] bitwise.i:158: Frama_C_show_each_dead: {0}
Called from bitwise.i:189.
[eva] bitwise.i:159: Frama_C_show_each_dead: {0}
[eva] Recording results for bug5
[eva] Done for function bug5
[eva] computing for function bug6 <- main.
Called from bitwise.i:189.
Called from bitwise.i:190.
[eva] computing for function set_zero <- bug6 <- main.
Called from bitwise.i:167.
Called from bitwise.i:168.
[eva] Recording results for set_zero
[eva] Done for function set_zero
[eva] bitwise.i:172: Reusing old results for call to set_zero
[eva] bitwise.i:173: Reusing old results for call to set_zero
[eva] Recording results for bug6
[eva] Done for function bug6
[eva] Recording results for main
......
tests/value/oracle/bitwise.1.res.oracle 0 → 100644
+ 308
− 0
View file @ 76c3e581
[kernel] Parsing bitwise.i (no 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
v ∈ [--..--]
input[0..2] ∈ [--..--]
s ∈ [--..--]
[eva] computing for function test1 <- main.
Called from bitwise.i:178.
[eva] computing for function Frama_C_interval <- test1 <- main.
Called from bitwise.i:29.
[eva] using specification for function Frama_C_interval
[eva] bitwise.i:29:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test1 <- main.
Called from bitwise.i:30.
[eva] bitwise.i:30:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test1 <- main.
Called from bitwise.i:31.
[eva] bitwise.i:31:
function Frama_C_interval: precondition 'order' got status valid.
[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 bitwise.i:179.
[eva] computing for function Frama_C_interval <- test2 <- main.
Called from bitwise.i:56.
[eva] bitwise.i:56:
function Frama_C_interval: precondition 'order' got status valid.
[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 bitwise.i:180.
[eva] Recording results for test3
[eva] Done for function test3
[eva] computing for function test4 <- main.
Called from bitwise.i:181.
[eva] bitwise.i:68: assertion got status valid.
[eva] bitwise.i:70: Frama_C_show_each_1: [0x80000000..0xFFFFFFFF], {0x80000000}
[eva] bitwise.i:70: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
[eva] bitwise.i:72: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0x80000000}
[eva] bitwise.i:72: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
[eva] bitwise.i:78: Frama_C_show_each_false: [0..0x7FFFFFFF]
[eva] bitwise.i:78: Frama_C_show_each_false: [0..0x7FFFFFFF]
[eva] Recording results for test4
[eva] Done for function test4
[eva] computing for function test5 <- main.
Called from bitwise.i:182.
[eva] computing for function Frama_C_nondet <- test5 <- main.
Called from bitwise.i:85.
[eva] using specification for function Frama_C_nondet
[eva] Done for function Frama_C_nondet
[eva] computing for function Frama_C_nondet <- test5 <- main.
Called from bitwise.i:86.
[eva] Done for function Frama_C_nondet
[eva] Recording results for test5
[eva] Done for function test5
[eva] computing for function and_or_rel <- main.
Called from bitwise.i:183.
[eva:alarm] bitwise.i:102: 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 bitwise.i:184.
[eva] Recording results for double_neg
[eva] Done for function double_neg
[eva] computing for function bug1 <- main.
Called from bitwise.i:185.
[eva] Recording results for bug1
[eva] Done for function bug1
[eva] computing for function bug2 <- main.
Called from bitwise.i:186.
[eva] bitwise.i:129: Frama_C_show_each_then:
[eva] bitwise.i:129: Frama_C_show_each_else:
[eva] Recording results for bug2
[eva] Done for function bug2
[eva] computing for function bug3 <- main.
Called from bitwise.i:187.
[eva] bitwise.i:136: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
[eva] Recording results for bug3
[eva] Done for function bug3
[eva] computing for function bug4 <- main.
Called from bitwise.i:188.
[eva] bitwise.i:146: Frama_C_show_each_then:
[eva] bitwise.i:148: Frama_C_show_each_else:
[eva] Recording results for bug4
[eva] Done for function bug4
[eva] computing for function bug5 <- main.
Called from bitwise.i:189.
[eva] bitwise.i:159: Frama_C_show_each_dead: {0}
[eva] Recording results for bug5
[eva] Done for function bug5
[eva] computing for function bug6 <- main.
Called from bitwise.i:190.
[eva] computing for function set_zero <- bug6 <- main.
Called from bitwise.i:168.
[eva] Recording results for set_zero
[eva] Done for function set_zero
[eva] bitwise.i:173: Reusing old results for call to set_zero
[eva] Recording results for bug6
[eva] Done for function bug6
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[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 bug1:
msb ∈ {6}
lsb ∈ {3}
par ∈ {5}
p1 ∈ {5}
p2 ∈ {0}
[eva:final-states] Values at end of function bug2:
t ∈ {1; 2}
[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 ∈ {-0x1578}
[eva:final-states] Values at end of function bug5:
x ∈ [-0x7FFFFFFE..0x7FFFFFFF]
[eva:final-states] Values at end of function double_neg:
i ∈ {5}
j ∈ {0xFFFFFFFA}
k ∈ {-6}
[eva:final-states] Values at end of function set_zero:
a ∈ {0}
[eva:final-states] Values at end of function bug6:
a ∈ {1}
[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 test5:
x ∈ {-1; 0}
y ∈ {-1; 0}
a ∈ {-1; 0}
b ∈ {-1; 0}
c ∈ {-1; 0}
[eva:final-states] Values at end of function main:
[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 bug5
[from] Done for function bug5
[from] Computing for function double_neg
[from] Done for function double_neg
[from] Computing for function set_zero
[from] Done for function set_zero
[from] Computing for function bug6
[from] Done for function bug6
[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 test5
[from] Computing for function Frama_C_nondet <-test5
[from] Done for function Frama_C_nondet
[from] Done for function test5
[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 Frama_C_interval:
\result FROM min; max
[from] Function Frama_C_nondet:
\result FROM a; b
[from] Function and_or_rel:
NO EFFECTS
[from] Function bug1:
NO EFFECTS
[from] Function bug2:
NO EFFECTS
[from] Function bug3:
NO EFFECTS
[from] Function bug4:
NO EFFECTS
[from] Function bug5:
NO EFFECTS
[from] Function double_neg:
NO EFFECTS
[from] Function set_zero:
a FROM c
[from] Function bug6:
NO EFFECTS
[from] Function test1:
NO EFFECTS
[from] Function test2:
NO EFFECTS
[from] Function test3:
NO EFFECTS
[from] Function test4:
\result FROM v
[from] Function test5:
NO EFFECTS
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function and_or_rel:
x; r1; r2; r3
[inout] Inputs for function and_or_rel:
v
[inout] Out (internal) for function bug1:
msb; lsb; par; p1; p2
[inout] Inputs for function bug1:
\nothing
[inout] Out (internal) for function bug2:
t; tmp
[inout] Inputs for function bug2:
v
[inout] Out (internal) for function bug3:
l_1180; foo
[inout] Inputs for function bug3:
\nothing
[inout] Out (internal) for function bug4:
g_2; tmp; tmp_0
[inout] Inputs for function bug4:
v
[inout] Out (internal) for function bug5:
x
[inout] Inputs for function bug5:
v
[inout] Out (internal) for function double_neg:
i; j; k
[inout] Inputs for function double_neg:
\nothing
[inout] Out (internal) for function set_zero:
a
[inout] Inputs for function set_zero:
\nothing
[inout] Out (internal) for function bug6:
a
[inout] Inputs for function bug6:
\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 test5:
x; y; a; b; c
[inout] Inputs for function test5:
\nothing
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
v; input[0..2]; s
tests/value/oracle/bitwise_pointer.1.res.oracle 0 → 100644
+ 99
− 0
View file @ 76c3e581
[kernel] Parsing bitwise_pointer.i (no 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
t[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {2}
[3] ∈ {3}
[4] ∈ {4}
[5] ∈ {5}
[6] ∈ {6}
[7] ∈ {7}
[8] ∈ {8}
[9] ∈ {9}
[10..99] ∈ {0}
p ∈ {0}
x ∈ {0}
t1[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {2}
[3] ∈ {3}
[4] ∈ {4}
[5] ∈ {5}
[6] ∈ {6}
[7] ∈ {7}
[8] ∈ {8}
[9] ∈ {9}
[10..99] ∈ {0}
p1 ∈ {0}
x1 ∈ {0}
[eva:alarm] bitwise_pointer.i:18: Warning:
pointer downcast. assert (unsigned int)(&t[7]) ≤ 2147483647;
[eva] bitwise_pointer.i:18:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {bitwise_pointer.i:18}
[eva:alarm] bitwise_pointer.i:19: Warning:
out of bounds write. assert \valid(p);
[eva:alarm] bitwise_pointer.i:22: Warning:
pointer downcast. assert (unsigned int)(&t1[mask]) ≤ 2147483647;
[eva] bitwise_pointer.i:22:
Assigning imprecise value to p1.
The imprecision originates from Arithmetic {bitwise_pointer.i:22}
[eva:alarm] bitwise_pointer.i:23: Warning:
out of bounds write. assert \valid(p1);
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t[0] ∈ {0; 5}
[1] ∈ {1; 5}
[2] ∈ {2; 5}
[3] ∈ {3; 5}
[4] ∈ {4; 5}
[5] ∈ {5}
[6] ∈ {5; 6}
[7] ∈ {5; 7}
[8] ∈ {5; 8}
[9] ∈ {5; 9}
[10..99] ∈ {0; 5}
p ∈ {{ &t + [0..99] }}
x ∈ [0..9]
t1[0] ∈ {0; 5}
[1] ∈ {1; 5}
[2] ∈ {2; 5}
[3] ∈ {3; 5}
[4] ∈ {4; 5}
[5] ∈ {5}
[6] ∈ {5; 6}
[7] ∈ {5; 7}
[8] ∈ {5; 8}
[9] ∈ {5; 9}
[10..99] ∈ {0; 5}
p1 ∈ {{ &t1 + [0..99] }}
x1 ∈ [0..9]
mask ∈ {7}
[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:
t[0..99] FROM \nothing (and SELF)
p FROM \nothing
x FROM t[0..99]
t1[0..99] FROM \nothing (and SELF)
p1 FROM \nothing
x1 FROM t1[0..99]
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
t[0..99]; p; x; t1[0..99]; p1; x1; mask
[inout] Inputs for function main:
t[0..99]; p; t1[0..99]; p1
[inout] InOut (internal) for function main:
Operational inputs:
t[0..99]; t1[0..99]
Operational inputs on termination:
t[0..99]; t1[0..99]
Sure outputs:
p; x; p1; x1; mask
tests/value/oracle/bitwise_reduction.res.oracle → tests/value/oracle/bitwise_reduction.0.res.oracle
+ 11
− 11
View file @ 76c3e581
......@@ -5,27 +5,27 @@
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
[eva] computing for function main1 <- main.
Called from bitwise_reduction.i:33.
[eva:alarm] bitwise_reduction.i:10: Warning: assertion got status unknown.
Called from bitwise_reduction.i:34.
[eva:alarm] bitwise_reduction.i:11: Warning: assertion got status unknown.
[eva:alarm] bitwise_reduction.i:14: Warning:
[eva:alarm] bitwise_reduction.i:12: Warning: assertion got status unknown.
[eva:alarm] bitwise_reduction.i:15: Warning:
accessing out of bounds index. assert 0 ≤ i;
[eva:alarm] bitwise_reduction.i:14: Warning:
[eva:alarm] bitwise_reduction.i:15: Warning:
accessing out of bounds index. assert i < 2;
[eva] bitwise_reduction.i:15: Frama_C_show_each_then1: {1}, {0; 1}
[eva] bitwise_reduction.i:17:
[eva] bitwise_reduction.i:16: Frama_C_show_each_then1: {1}, {0; 1}
[eva] bitwise_reduction.i:18:
Frama_C_show_each_else1:
{0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
[eva] bitwise_reduction.i:19:
[eva] bitwise_reduction.i:20:
Frama_C_show_each_else_then1:
{0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
[eva:alarm] bitwise_reduction.i:23: Warning:
[eva:alarm] bitwise_reduction.i:24: Warning:
out of bounds read. assert \valid_read(p);
[eva] bitwise_reduction.i:24: Frama_C_show_each_then2: {{ &t + {4} }}, {0; 1}
[eva] bitwise_reduction.i:26:
[eva] bitwise_reduction.i:25: Frama_C_show_each_then2: {{ &t + {4} }}, {0; 1}
[eva] bitwise_reduction.i:27:
Frama_C_show_each_else2:
{{ &t + {0; 4} }}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
[eva] bitwise_reduction.i:28:
[eva] bitwise_reduction.i:29:
Frama_C_show_each_else_then2:
{0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
[eva] Recording results for main1
......
tests/value/oracle/bitwise_reduction.1.res.oracle 0 → 100644
+ 61
− 0
View file @ 76c3e581
[kernel] Parsing bitwise_reduction.i (no 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
v ∈ [--..--]
[eva] computing for function main1 <- main.
Called from bitwise_reduction.i:34.
[eva:alarm] bitwise_reduction.i:11: Warning: assertion got status unknown.
[eva:alarm] bitwise_reduction.i:12: Warning: assertion got status unknown.
[eva:alarm] bitwise_reduction.i:15: Warning:
accessing out of bounds index. assert 0 ≤ i;
[eva:alarm] bitwise_reduction.i:15: Warning:
accessing out of bounds index. assert i < 2;
[eva] bitwise_reduction.i:16: Frama_C_show_each_then1: {1}, {0; 1}
[eva] bitwise_reduction.i:18:
Frama_C_show_each_else1:
{0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
[eva] bitwise_reduction.i:20:
Frama_C_show_each_else_then1:
{0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
[eva:alarm] bitwise_reduction.i:24: Warning:
out of bounds read. assert \valid_read(p);
[eva] bitwise_reduction.i:25: Frama_C_show_each_then2: {{ &t + {4} }}, {0; 1}
[eva] bitwise_reduction.i:27:
Frama_C_show_each_else2:
{{ &t + {0; 4} }}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
[eva] bitwise_reduction.i:29:
Frama_C_show_each_else_then2:
{0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
[eva] Recording results for main1
[eva] Done for function main1
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
t[0] ∈ {0xF000; 0xFF00}
[1] ∈ {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000}
i ∈ {0; 1}
p ∈ {{ &t{[0], [1]} }}
[eva:final-states] Values at end of function main:
[from] Computing for function main1
[from] Done for function main1
[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 main1:
NO EFFECTS
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main1:
t[0..1]; i; p
[inout] Inputs for function main1:
v
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
v
tests/value/oracle_apron/bitwise.res.oracle → tests/value/oracle_apron/bitwise.0.res.oracle
+ 2
− 2
View file @ 76c3e581
105c105,108
< [eva] bitwise.i:172: Reusing old results for call to set_zero
< [eva] bitwise.i:173: Reusing old results for call to set_zero
---
> [eva] computing for function set_zero <- bug6 <- main.
> Called from bitwise.i:172.
> Called from bitwise.i:173.
> [eva] Recording results for set_zero
> [eva] Done for function set_zero
tests/value/oracle_apron/bitwise.1.res.oracle 0 → 100644
+ 7
− 0
View file @ 76c3e581
105c105,108
< [eva] bitwise.i:173: Reusing old results for call to set_zero
---
> [eva] computing for function set_zero <- bug6 <- main.
> Called from bitwise.i:173.
> [eva] Recording results for set_zero
> [eva] Done for function set_zero
tests/value/oracle_bitwise/bitwise.res.oracle → tests/value/oracle_bitwise/bitwise.0.res.oracle
+ 2
− 2
View file @ 76c3e581
96c96,99
< [eva] bitwise.i:158: Frama_C_show_each_dead: {0}
< [eva] bitwise.i:159: Frama_C_show_each_dead: {0}
---
> [eva] bitwise.i:156:
> [eva] bitwise.i:157:
> The evaluation of the expression x & 2
> led to bottom without alarms:
> at this point the product of states has no possible concretization.
tests/value/oracle_bitwise/bitwise.1.res.oracle 0 → 100644
+ 7
− 0
View file @ 76c3e581
96c96,99
< [eva] bitwise.i:159: Frama_C_show_each_dead: {0}
---
> [eva] bitwise.i:157:
> The evaluation of the expression x & 2
> led to bottom without alarms:
> at this point the product of states has no possible concretization.
tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle 0 → 100644
+ 12
− 0
View file @ 76c3e581
34,36c34
< [eva] bitwise_pointer.i:18:
< Assigning imprecise value to p.
< The imprecision originates from Arithmetic {bitwise_pointer.i:18}
---
> [eva] bitwise_pointer.i:18: Assigning imprecise value to p.
41,43c39
< [eva] bitwise_pointer.i:22:
< Assigning imprecise value to p1.
< The imprecision originates from Arithmetic {bitwise_pointer.i:22}
---
> [eva] bitwise_pointer.i:22: Assigning imprecise value to p1.
tests/value/oracle_multidim/bitwise_reduction.1.res.oracle 0 → 100644
+ 12
− 0
View file @ 76c3e581
18c18
< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
---
> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
21c21
< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
---
> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
30c30
< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
---
> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
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