Skip to content

Commit

Permalink
Modular analysis: Simplify handling of index-offsets.
Browse files Browse the repository at this point in the history
  • Loading branch information
jerhard committed Dec 8, 2023
1 parent e73e370 commit 6f2483b
Showing 1 changed file with 10 additions and 14 deletions.
24 changes: 10 additions & 14 deletions src/cdomains/preValueDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,28 +4,24 @@ module IndexDomain = IntDomain.IntDomWithDefaultIkind (ID) (IntDomain.PtrDiffIki
module Offs = struct
include Offset.MakeLattice (IndexDomain)

(** Add the [additional_offset] to the [base_offset]. In case [additional_offset] starts with an index offset, merge this index with the last index occurring in [base_offset]. *)
(** Add the [additional_offset] to the [base_offset]. In case [additional_offset] starts with an index offset, merge this index with the index occurring at the end of [base_offset], if any. *)
let rec add_offset_merge_index_offset ~(base_offset: t) ~(additional_offset: t): t =
match additional_offset with
| `NoOffset -> base_offset
| `Field (f,o) -> add_offset base_offset additional_offset
| `Index (i,o) ->
let rec add_offset_index_merged o = match o with
| `NoOffset -> false, additional_offset
| `NoOffset -> additional_offset
| `Field (f1,o1) ->
let merged, offs = add_offset_index_merged o1 in
merged, `Field (f1, offs)
| `Index (i1,o1) ->
let merged, offs = add_offset_index_merged o1 in
let offs = if merged then
`Index (i, offs)
else
`Index (IndexDomain.add i1 i, o1)
in
true, offs
let offs = add_offset_index_merged o1 in
`Field (f1, offs)
| `Index (i1, `NoOffset) ->
`Index (IndexDomain.add i1 i, `NoOffset)
| `Index (i1, o1) ->
let offs = add_offset_index_merged o1 in
`Index (i, offs)
in
let _, offs = add_offset_index_merged base_offset in
offs
add_offset_index_merged base_offset
end

module Mval = Mval.MakeLattice (Offs)
Expand Down

0 comments on commit 6f2483b

Please sign in to comment.