Frama-C API - PreciseDepsOf
Dependencies of expressions and lvalues based on Precise_locs.precise_location.
type location = Frama_c_kernel.Precise_locs.precise_locationval zone_of_exp : (Eva_ast_types.lval -> location) -> Eva_ast_types.exp -> Frama_c_kernel.Locations.Zone.tGiven a function computing the location of lvalues, computes the memory zone on which the value of an expression depends.
val zone_of_lval : (Eva_ast_types.lval -> location) -> Eva_ast_types.lval -> Frama_c_kernel.Locations.Zone.tGiven 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_ast_types.lval -> location) -> Eva_ast_types.lval -> Frama_c_kernel.Locations.Zone.tGiven 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_ast_types.lval -> location) -> Eva_ast_types.exp -> Deps.tGiven a function computing the location of lvalues, computes the memory dependencies of an expression.
val deps_of_lval : (Eva_ast_types.lval -> location) -> Eva_ast_types.lval -> Deps.tGiven a function computing the location of lvalues, computes the memory dependencies of an lvalue.