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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct