Module Formula_utils

module Formula_utils: sig .. end
High level formula manipulation


Registers/Variables


val concretize_register : string -> Smtlib2.smt_bv_expr -> Path_pred_env.t -> unit
concretize_register name value env concretize the register name with the value value. This function solely add a constraint on the current register value.
val replace_register : string -> Smtlib2.smt_bv_expr -> Path_pred_env.t -> unit
Deprecated.use logicalize_register instead
replace the register value with the given smt_bv_expr
val logicalize_register : string -> Dba.expr -> Path_pred_env.t -> unit
convert the DBA expression in SMT and then call replace_register
val symbolize_register : string -> ?is_full_name:bool -> string -> Path_pred_env.t -> unit
symbolize_register name ~is_full_name prefix create a new symbol and assign it in the register name. ~is_full_name define only use prefix as symbol name otherwise concatenate prefix and name
val symbolize_and_then_concretize_register : string -> Smtlib2.smt_bv_expr -> string -> Path_pred_env.t -> unit
symbolize the register and then concretize it. It has in effect to constraint the new symbol with the concrete value. (reset history)

Memory


val replace_memory : int64 -> string -> Path_pred_env.t -> unit
Deprecated.use logicalize_memory instead
replace_memory addr data env perform a store operation of every bytes of data starting at addr
val concretize_memory : Dba.expr -> string -> Path_pred_env.t -> unit
concretize_memory dba_addr data env add constraints on the memory at the logical address dba_addr for every bytes of data
val symbolize_memory_one_octet : int64 -> string -> Path_pred_env.t -> unit
symbolize_memory_one_octet addr prefix env symbolize the the byte at address addr and prefix the new input symbol by prefix
val symbolize_memory : Dba.expr -> string -> ?i:int -> int -> Path_pred_env.t -> unit
symbolize_memory dba_addr prefix ~i size env symbolize the memory starting at the address dba_addr up to size. All input symbols created will be prefixed by prefix
val logicalize_memory : Dba.expr -> Dba.expr -> Path_pred_env.t -> unit
logicalize_memory addr content put content at addr by performing a logical store in memory