Module Checkct.Ct_stateSource

Sourcetype load = ([ `Mem ], string, Libterm.Sexpr.Memory.t) Binsec.Term.t
Sourcetype t = {
  1. mutable constraints : Libterm.Sexpr.Expr.t list;
  2. mutable conjunction : Libterm.Sexpr.Expr.t;
  3. secrets : Libterm.Sexpr.Expr.t Libterm.Sexpr.BvTbl.t;
  4. mirror_e : Libterm.Sexpr.Expr.t Libterm.Sexpr.BvTbl.t;
  5. mirror_m : Libterm.Sexpr.Memory.t Libterm.Sexpr.AxTbl.t;
  6. mutable loads : load list;
  7. roots : Libterm.Sexpr.Memory.t Libterm.Sexpr.AxTbl.t;
  8. mutable models : (int * Libterm.Sexpr.Model.t) list;
}
Sourceval empty : unit -> t
Sourceval fork : t -> t
Sourceval mirror : Libterm.Sexpr.Expr.t -> t -> unit
Sourceval is_tainted : Libterm.Sexpr.Expr.t -> t -> bool
Sourceval is_tainted_memory : Libterm.Sexpr.Memory.t -> t -> bool
Sourceval make_context : Libterm.Sexpr.Expr.t list -> t -> unit