Smt_external.TranslateSourceval 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
val assign :
?wild:bool ->
Binsec.Dba.LValue.t ->
Binsec.Dba.Expr.t ->
Smt_symbolic.State.t ->
Smt_symbolic.State.tval havoc :
?naming_hint:string ->
?wild:bool ->
Binsec.Dba.LValue.t ->
Smt_symbolic.State.t ->
Smt_symbolic.State.t