package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

External API of the plugin Alias

module G : Graph.Sig.G
val vid : G.V.t -> int

NB : do the analysis BEFORE using any of those functions

points_to_set_stmt kf s lv returns the points-to set of lval lv before stmt in function kf.

points_to_set kf s lv returns the points-to set of lval lv at the end of function kf.

aliases_stmt kf s lv return the alias set of lval lv before stmt in function kf.

aliases_kf kf lv return the alias set of lval lv at the end of function kf.

list of pairs s, e where e is the set of lval aliased to v after statement s in function kf.

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.

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.

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.

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.

fold_aliases_kf f acc kf lv folds f acc over all the aliases of lval lv at the end of function kf.

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.

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.

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.

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

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.

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.

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