package binsec
Module Smt_external.TranslateSource
Source
val expr :
Smt_symbolic.State.t ->
Binsec.Dba.Expr.t ->
Binsec.Formula.bv_term * Smt_symbolic.State.tmissing bitvectors are implicitely declared so this returns a new symbolic state
Source
val assign :
?wild:bool ->
Binsec.Dba.LValue.t ->
Binsec.Dba.Expr.t ->
Smt_symbolic.State.t ->
Smt_symbolic.State.tSource
val havoc :
?naming_hint:string ->
?wild:bool ->
Binsec.Dba.LValue.t ->
Smt_symbolic.State.t ->
Smt_symbolic.State.t