diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml index 4c112fc3608dd65d45c17e6b7fbe283ffc7922c5..50ef904b996e0e165ccedc234f7c12f795673fa9 100644 --- a/src/kernel_services/abstract_interp/abstract_memory.ml +++ b/src/kernel_services/abstract_interp/abstract_memory.ml @@ -885,8 +885,9 @@ struct let hash (b,_a) = Bound.hash b let compare (b1,_a1) (b2,_a2) = Bound.compare b1 b2 - let equal (b1,_a1) (b2,_a2) = + let equal_regardless_age (b1,_a1) (b2,_a2) = Bound.equal b1 b2 + let equal = equal_regardless_age let _of_integer i a = Bound.of_integer i, a let _of_exp e a = Bound.of_exp e, a let _succ (b,a) = (Bound.succ b, a) @@ -954,6 +955,8 @@ struct padding: bit; (* padding at the left and right of the segmentation *) } + type segments = (M.t * B.t) list + let _pretty_debug fmt (l,s) : unit = Format.fprintf fmt " {%a} " B.pretty l; let pp fmt (v,u) = @@ -1311,6 +1314,24 @@ struct aging >>-: limit_size ~oracle + let remove_empty_segments m = + let unify_head_age (b' : B.t) : segments -> segments = function + | [] -> [] (* Start of segmentation, age is 0, do nothing *) + | (v,b) :: t -> (v, B.unify_age ~other:b' b) :: t + in + let rec aux l acc = function + | [] -> List.rev acc + | (v,u) :: t -> + (* Oracle cannot be used in case of incr here as it represents the + value of the bounds before the instruction, while we iterate + here over a segmentation interpreted after the instruction. *) + if B.equal_regardless_age l u then (* empty segment, remove v *) + aux l (unify_head_age u acc) t + else + aux u ((v,u) :: acc) t + in + { m with segments = check_segments (aux m.start [] m.segments) } + let incr_bound ~oracle vi x m = let incr = B.incr_or_constantify ~oracle vi x in let rec aux acc = function @@ -1337,7 +1358,8 @@ struct and v = M.smash ~oracle (M.of_raw m.padding) v in l, (v,u) :: t in - { m with start ; segments = check_segments (List.rev (aux [] segments)) } + { m with start ; segments = check_segments (List.rev (aux [] segments)) } |> + remove_empty_segments let map f m = { m with segments = check_segments (List.map (fun (v,u) -> f v, u) m.segments) } diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle index fb4bb1d3533963d673aaff3181e56d9f3bb0a472..4267d1cea2a92dd692e1a1bb3a90098978150e52 100644 --- a/tests/value/oracle/multidim.res.oracle +++ b/tests/value/oracle/multidim.res.oracle @@ -92,7 +92,7 @@ [eva] multidim.c:59: Frama_C_domain_show_each: t : # cvalue: {0; 1} - # multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} } + # multidim: [0 .. 9] = {1} [eva] Recording results for main2 [eva] Done for function main2 [eva] computing for function main3 <- main. @@ -154,12 +154,7 @@ Frama_C_domain_show_each: t : # cvalue: [0..9] ∈ {0; 1} [10..19] ∈ {0; 2} - # multidim: { - [0 .. 17] = {1; 2}, - [18] = {1; 2}, - [19] = {2}, - [20 .. 19] = {0} - } + # multidim: { [0 .. 17] = {1; 2}, [18] = {1; 2}, [19] = {2} } [eva] Recording results for main5 [eva] Done for function main5 [eva] computing for function main6 <- main. @@ -195,12 +190,9 @@ Frama_C_domain_show_each: t : # cvalue: [0].typ ∈ {1; 2} or UNINITIALIZED {[0].val; [1..999]} ∈ [--..--] or UNINITIALIZED - # multidim: { - [0 .. 999] = { - { .typ = {1}, .val.i = {42} } or - { .typ = {2}, .val.f = {42.} } - }, - [1000 .. 999] = UNINITIALIZED + # multidim: [0 .. 999] = { + { .typ = {1}, .val.i = {42} } or + { .typ = {2}, .val.f = {42.} } } [eva] computing for function Frama_C_interval <- main7 <- main. Called from multidim.c:147. @@ -219,7 +211,7 @@ [eva] multidim.c:169: Frama_C_domain_show_each: t : # cvalue: {0; 1} - # multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} } + # multidim: [0 .. 9] = {1} [eva] Recording results for main8 [eva] Done for function main8 [eva] computing for function main9 <- main.