Frama-C API - Transfer_inout
type location = Loc.locationtype value = Val.ttype valuation = Eval.Valuation.tval register_logic_assign : Eva__.Position.t -> location Eva.Eval.logic_assign -> location -> Eva__.Inout_access.tregister_logc_assign pos clause location registers to Inout_access the read and written memory zones at pos for the logic assign clause to the location. The memory accessed by the logic assign is returned.
val register_assign_lval : Eva__.Position.t -> valuation -> Eva.Eva_ast.lval -> Eva.Eva_ast.exp -> Eva__.Inout_access.tregister_assign_lval pos valuation lval exp registers to Inout_access the read and written memory zones at pos for the assignment from exp to lval with a given valuation. The memory accessed by the assignment is returned.
val register_assign_var : Eva__.Position.t -> valuation -> Eva.Eva_ast.varinfo -> Eva.Eva_ast.exp -> Eva__.Inout_access.tregister_assign_var pos valuation vi exp registers to Inout_access the read and written memory zones at pos for the assignment from exp to vi with a given valuation. The memory accessed by the assignment is returned.
val register_read_exp : Eva__.Position.t -> valuation -> Eva.Eva_ast.exp -> Eva__.Inout_access.tregister_read_exp pos valuation exp registers to Inout_access the read memory zones at pos for reading the expression exp with a given valuation. The memory accessed by the read is returned.
val register_call_args : Eva__.Position.t -> valuation -> (location, value) Eva.Eval.call -> Eva__.Inout_access.tregister_call_args pos valuation call registers to Inout_access the read and written memory zones at pos for the arguments of the given call with a given valuation. The memory accessed by the call arguments is returned.