Alias.APISourceExternal API of the plugin Alias
module LSet = Frama_c_kernel.Cil_datatype.LvalStructEq.SetNB : do the analysis BEFORE using any of those functions
val points_to_set_stmt :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
LSet.tpoints_to_set_stmt kf s lv returns the points-to set of lval lv before stmt in function kf.
val points_to_set_kf :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.lval ->
LSet.tpoints_to_set kf s lv returns the points-to set of lval lv at the end of function kf.
val aliases_stmt :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
LSet.taliases_stmt kf s lv return the alias set of lval lv before stmt in function kf.
val aliases_kf :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.lval ->
LSet.taliases_kf kf lv return the alias set of lval lv at the end of function kf.
val fundec_stmts :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.lval ->
(Frama_c_kernel.Cil_types.stmt * LSet.t) listlist of pairs s, e where e is the set of lval aliased to v after statement s in function kf.
val fold_points_to_set :
('a -> Frama_c_kernel.Cil_types.lval -> 'a) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
'afold_points_to_set f acc kf s lv folds f acc over all the lvals in the points-to set of the given lval lv right before stmt s in function kf.
val fold_aliases_stmt :
('a -> Frama_c_kernel.Cil_types.lval -> 'a) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
'afold_aliases_stmt f acc kf s lv folds f acc over all the aliases of the given lval lv right before stmt s in function kf.
val fold_new_aliases_stmt :
('a -> Frama_c_kernel.Cil_types.lval -> 'a) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
'afold_new_aliases_stmt f acc kf s lv folds f acc over all the aliases of the given lval lv created by stmt s in function kf.
val fold_points_to_set_kf :
('a -> Frama_c_kernel.Cil_types.lval -> 'a) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.lval ->
'afold_points_to_set_kf f acc kf lv folds f acc over the points-to set of lval lv at the end of function kf.
val fold_aliases_kf :
('a -> Frama_c_kernel.Cil_types.lval -> 'a) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.lval ->
'afold_aliases_kf f acc kf lv folds f acc over all the aliases of lval lv at the end of function kf.
val fold_fundec_stmts :
('a -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> 'a) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.lval ->
'afold_fundec_stmts f acc kf v folds f acc s e on the list of pairs s, e where e is the set of lval aliased to v after statement s in function kf.
val are_aliased :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
Frama_c_kernel.Cil_types.lval ->
boolare_aliased kf s lv1 lv2 returns true if and only if the two lvals lv1 and lv2 are aliased before stmt s in function kf.
val fold_vertex :
('a -> G.V.t -> Frama_c_kernel.Cil_types.lval -> 'a) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
'afold_vertex f acc kf s v folds f acc i lv to all lv in i, where i is the vertex that represents the equivalence class of v before statement s in function kf.
val fold_vertex_closure :
('a -> G.V.t -> Frama_c_kernel.Cil_types.lval -> 'a) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
'afold_vertex_closure f acc kf s v is the transitive closure of function fold_vertex.
direct access to the abstract state. See Abstract_state.mli
val get_state_before_stmt :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Abstract_state.t optionget_state_before_stmt f s gets the abstract state computed after statement s in function f. Returns None if the abstract state is bottom or not computed.
val call_function :
Abstract_state.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.lval option ->
Frama_c_kernel.Cil_types.exp list ->
Abstract_state.t optioncall_function a f Some(res) args computes the abstract state after the instruction res=f(args) where res is a lval. a is the abstract state before the call. If function f returns no value, use call_function a f None args instead. Returns None if the abstract state a is bottom or not computed.
simplify_lval lv returns a lval where every index of an array is replaced by 0, evey pointer arithmetic is simplified to an access to an array