Frama-C:
Plug-ins:
Libraries:

Frama-C API - PreciseDepsOf

Dependencies of expressions and lvalues based on Precise_locs.precise_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.