Eva_ast.DepsOf
Dependencies of expressions and lvalues based on type location
.
val zone_of_exp :
((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
Eva__.Eva_ast_types.tag ->
location) ->
Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
Frama_c_kernel.Locations.Zone.t
Given a function computing the location of lvalues, computes the memory zone on which the value of an expression depends.
val zone_of_lval :
((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
Eva__.Eva_ast_types.tag ->
location) ->
(Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
Eva__.Eva_ast_types.tag ->
Frama_c_kernel.Locations.Zone.t
Given a function computing the location of lvalues, computes the memory zone on which the value of an lvalue depends.
val indirect_zone_of_lval :
((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
Eva__.Eva_ast_types.tag ->
location) ->
(Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
Eva__.Eva_ast_types.tag ->
Frama_c_kernel.Locations.Zone.t
Given a function computing the location of lvalues, computes the memory zone on which the offset and the pointer expression (if any) of an lvalue depend.
val deps_of_exp :
((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
Eva__.Eva_ast_types.tag ->
location) ->
Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
Deps.t
Given a function computing the location of lvalues, computes the memory dependencies of an expression.
val deps_of_lval :
((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
Eva__.Eva_ast_types.tag ->
location) ->
(Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
Eva__.Eva_ast_types.tag ->
Deps.t
Given a function computing the location of lvalues, computes the memory dependencies of an lvalue.