Alias.API
External API of the plugin Alias
module LSet = Frama_c_kernel.Cil_datatype.LvalStructEq.Set
NB : 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.t
points_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.t
points_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.t
aliases_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.t
aliases_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) list
list 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 ->
'a
fold_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 ->
'a
fold_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 ->
'a
fold_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 ->
'a
fold_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 ->
'a
fold_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 ->
'a
fold_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 ->
bool
are_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 ->
'a
fold_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 ->
'a
fold_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
module Abstract_state : sig ... end
val get_state_before_stmt :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Abstract_state.t option
get_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 option
call_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.
val simplify_lval :
Frama_c_kernel.Cil_types.lval ->
Frama_c_kernel.Cil_types.lval
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