Module Path_pred_env

module Path_pred_env: sig .. end
DSE Environment

type t = {
   mutable formula : Formula_type.formula; (*
Formula containing path predicate
*)
   addr_size : int; (*
Size of addresses (in bits!)
*)
   mutable toplevel : bool; (*
Switch sometime used to perform an action once on env
*)
   mutable config : Config_piqi.configuration; (*
configuration sent to the analysis
*)
   mutable analysis : dse_analysis_sig_t;
}
Environment type
type dse_analysis_sig_t = <
   compute : int;
   concretize_cond : Dba.cond -> t -> bool;
   concretize_expr_bv : Dba.expr -> ?is_lhs:bool -> t -> Bitvector.t;
   exec : Dba_types.Statement.t -> t -> unit;
   expr_to_smt : Dba.expr ->
?apply_cs:bool ->
t -> Smtlib2.smt_bv_expr * Smtlib2.smt_expr list
;
   get_current_concrete_infos : unit -> Trace_type.trace_concrete_infos list;
   get_current_dbacodeaddress : unit -> Dba.address;
   get_taint : unit -> Tainting.tainting_engine;
   is_taint_computed : unit -> bool;
   solve_predicate : Smtlib2.smt_expr ->
?print_stat:bool ->
?name:string ->
?push:bool ->
?pop:bool ->
?prek:int ->
?pruning:bool ->
?get_model:bool ->
t -> Smtlib2.smt_result * Smt_model.t * float
;
>
signature that should implement an analysis contained in the analysis field
val new_env : dse_analysis_sig_t ->
Config_piqi.configuration ->
?cst_pro:bool ->
?rebase:bool ->
?row:bool -> ?row_plus:bool -> ?eq_prop:bool -> int -> t
Create a new environment new_env analysis conf addr_size. All the new arguments are the optimisations to perform on the formula