Module Core.ChangeSource

Changes are used to log the statements executed during the computation of a post-state

Sourcetype change =
  1. | Change_empty
  2. | Change_block of Ast.Stmt.stmt list
  3. | Change_seq of change list
  4. | Change_join of change * change
  5. | Change_meet of change * change
Sourceval pp_change : Stdlib.Format.formatter -> change -> unit
Sourceval compare_change : change -> change -> int
Sourceval empty_change : change
Sourceval is_empty_change : change -> bool
Sourceval join_change : change -> change -> change
Sourceval meet_change : change -> change -> change
Sourceval add_stmt_to_change : Ast.Stmt.stmt -> change -> change

Join two changes

Sourceval concat_change : change -> change -> change

Meet two changes

Sourcetype change_map = change Path.PathMap.t
Sourceval pp_change_map : Stdlib.Format.formatter -> change Path.PathMap.t -> unit
Sourceval compare_change_map : change Path.PathMap.t -> change Path.PathMap.t -> int
Sourceval empty_change_map : 'a Path.PathMap.t
Sourceval singleton_change_map : Path.PathMap.key -> 'a -> 'a Path.PathMap.t
Sourceval is_empty_change_map : change Path.PathMap.t -> bool

Generic merge

*****************

Sourcetype change_vars = {
  1. modified : Ast.Var.VarSet.t;
  2. removed : Ast.Var.VarSet.t;
}

Change of a statement in terms of modified and removed variables

Sourceval compare_change_vars : change_vars -> change_vars -> int
Sourceval is_empty_change_vars : change_vars -> bool
Sourceval get_stmt_change_vars : custom:(Ast.Stmt.stmt -> change_vars option) -> Ast.Stmt.stmt -> change_vars

Get the changes of a statement

Sourceval get_change_vars : custom:(Ast.Stmt.stmt -> change_vars option) -> change -> change_vars
Sourceval apply_change_vars : change_vars -> add:(Ast.Var.VarSet.elt -> 'b -> 'a -> 'a) -> remove:(Ast.Var.VarSet.elt -> 'a -> 'a) -> find:(Ast.Var.VarSet.elt -> 'a -> 'b) -> 'a -> 'a -> 'a

Apply changes on an abstract element

Sourceval generic_merge : add:(Ast.Var.VarSet.elt -> 'a -> 'b -> 'b) -> find:(Ast.Var.VarSet.elt -> 'b -> 'a) -> remove:(Ast.Var.VarSet.elt -> 'b -> 'b) -> ?custom:(Ast.Stmt.stmt -> change_vars option) -> ('b * change) -> ('b * change) -> 'b * 'b

Generic merge operator for non-relational domains

Sourceval opt_change_tracker_enabled : bool Stdlib.ref
Sourceval enable_change_tracker : unit -> unit
Sourceval disable_change_tracker : unit -> unit
Sourceval is_change_tracker_enabled : unit -> bool
Sourceval set_change_tracker_state : bool -> unit
Sourceval with_change_tracker : (unit -> 'a) -> 'a