Module Concrete_eval

module Concrete_eval: sig .. end

val eval_expr : Dba.expr ->
Region_bitvector.t Concrete_state.SubEnv.t Static_types.Env.t ->
Smt_bitvectors.smtBvExprAlt list ->
Dba_types.Caddress.Set.t -> Region_bitvector.t
val eval_cond : Dba.cond ->
Region_bitvector.t Concrete_state.SubEnv.t Static_types.Env.t ->
Smt_bitvectors.smtBvExprAlt list -> Dba_types.Caddress.Set.t -> bool
val write : Static_types.extended_variable ->
Bigint.t ->
Region_bitvector.t ->
Region_bitvector.t Concrete_state.SubEnv.t Static_types.Env.t ->
Smt_bitvectors.smtBvExprAlt list ->
Dba_types.Caddress.Set.t ->
Region_bitvector.t Concrete_state.SubEnv.t Static_types.Env.t
val read : Static_types.extended_variable ->
Bigint.t ->
Region_bitvector.t Concrete_state.SubEnv.t Static_types.Env.t ->
Smt_bitvectors.smtBvExprAlt list ->
Dba_types.Caddress.Set.t -> Region_bitvector.t
val add_smt_cond : Dba.cond ->
Region_bitvector.t Concrete_state.SubEnv.t Static_types.Env.t ->
Smt_bitvectors.smtBvExprAlt list ->
Dba_types.Caddress.Set.t -> Smt_bitvectors.smtBvExprAlt list
val perm : Dba_types.permissions list Dba_types.Region.Map.t Pervasives.ref
val permis : Dba.cond Dba_types.Rights.t Pervasives.ref