Wp.RegionAccess
val cc_lval : Region.map -> Frama_c_kernel.Cil_types.lval -> Region.region
val cc_read : Region.map -> Frama_c_kernel.Cil_types.exp -> unit
val cc_assign :
Region.map ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
Frama_c_kernel.Cil_types.exp ->
unit
val cc_init :
Region.map ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
Frama_c_kernel.Cil_types.init ->
unit
val cc_instr :
Region.map ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.instr ->
unit
val cc_fundec : Region.map -> Frama_c_kernel.Cil_types.fundec -> unit
val cc_pred : Region.map -> Frama_c_kernel.Cil_types.predicate -> unit
val cc_term : Region.map -> Frama_c_kernel.Cil_types.term -> unit
val cc_spec : Region.map -> Frama_c_kernel.Cil_types.spec -> unit
val cc_region : Region.map -> RegionAnnot.region_spec -> unit