package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_analyzer/Mopsa_analyzer/MopsaLib/index.html
Module Mopsa_analyzer.MopsaLib
Source
Essential modules.
include module type of struct include Mopsa_utils end
module Bitfields = Mopsa_utils.Bitfields
module CongUtils = Mopsa_utils.CongUtils
module Containers = Mopsa_utils.Containers
module ItvUtils = Mopsa_utils.ItvUtils
include module type of struct include Framework.Core.All end
include module type of struct include Core.Ast.Semantic end
include module type of struct include Core.Ast.Constant end
type constant = Core.Ast.Constant.constant = ..
Extensible constants
compare_constant c1 c2
provides a total order between any pair c1
and c2
of registered constants
val pp_constant : Format.formatter -> constant -> unit
pp_constant fmt c
pretty-prints a registered constant c
with formatter fmt
Registration
val register_constant : constant Mopsa_utils.Core.TypeExt.info -> unit
register_constant info
registers a new constant with a comparison function info.compare
and a pretty-printer info.print
val register_constant_compare :
constant Mopsa_utils.Core.TypeExt.compare ->
unit
register_constant_compare compare
registers a new comparison function for constants
val register_constant_pp : constant Mopsa_utils.Core.TypeExt.print -> unit
register_constant_compare compare
registers a new pretty-printer for constants
Common constants
include module type of struct include Framework.Core.Ast.Expr end
type expr_kind = Framework.Core.Ast.Expr.expr_kind = ..
Extensible type of expression kinds
type expr = Framework.Core.Ast.Expr.expr = {
ekind : expr_kind;
(*kind of the expression
*)etyp : Framework.Core.Ast.Typ.typ;
(*type of the expression
*)erange : Mopsa_utils.Core.Location.range;
(*location range of the expression
*)etrans : expr Core.Ast.Semantic.SemanticMap.t;
(*translations of the expression into other semantics
*)ehistory : expr list;
(*History of preceding evaluations of the expression
*)esynthetic : bool;
(*whether the expression was generated dynamically during the analysis
*)
}
Expressions
compare_expr e1 e2
implements a total order between expressions
val pp_expr : Format.formatter -> expr -> unit
pp_expr fmt e
pretty-prints expression e
with format fmt
val etyp : expr -> Framework.Core.Ast.Typ.typ
Get the type of an expression
val erange : expr -> Mopsa_utils.Core.Location.range
Get the location of an expression
val etrans : expr -> expr Core.Ast.Semantic.SemanticMap.t
Get the translation map of an expression
val esynthetic : expr -> bool
Check if an expression is synthetic
val mk_expr :
?etyp:Framework.Core.Ast.Typ.typ ->
?etrans:expr Core.Ast.Semantic.SemanticMap.t ->
?ehistory:expr list ->
?esynthetic:bool ->
expr_kind ->
Mopsa_utils.Core.Location.range ->
expr
Construct an expression
val add_expr_translation : Core.Ast.Semantic.semantic -> expr -> expr -> expr
Add a translation of an expression
val get_expr_translations : expr -> expr Core.Ast.Semantic.SemanticMap.t
Get all translations of an expression
val get_expr_translation : Core.Ast.Semantic.semantic -> expr -> expr
Get the translation of an expression into a given semantic
Get the ancestor expression verifying a predicate
Registration
val register_expr : expr Mopsa_utils.Core.TypeExt.info -> unit
register_expr info
registers new expressions with their comparison function info.compare
and pretty-printer info.print
val register_expr_compare : expr Mopsa_utils.Core.TypeExt.compare -> unit
register_expr_compare compare
registers a new expression comparison
val register_expr_pp : expr Mopsa_utils.Core.TypeExt.print -> unit
register_expr_compare compare
registers a new expression printer
Some common expressions
Variable expressions
type expr_kind +=
| E_var of Framework.Core.Ast.Var.var * Framework.Core.Ast.Var.mode option
(*optional access mode overloading the variable's access mode
*)
Variables
val mk_var :
?esynthetic:bool ->
Framework.Core.Ast.Var.var ->
?mode:Framework.Core.Ast.Var.mode option ->
Mopsa_utils.Core.Location.range ->
expr
Create a variable expression
val var_mode :
Framework.Core.Ast.Var.var ->
Framework.Core.Ast.Var.mode option ->
Framework.Core.Ast.Var.mode
Get the overloaded access mode of a variable
Heap addresses expressions
type expr_kind +=
| E_addr of Framework.Core.Ast.Addr.addr * Framework.Core.Ast.Var.mode option
(*optional access mode overloading the address access mode
*)| E_alloc_addr of Framework.Core.Ast.Addr.addr_kind * Framework.Core.Ast.Var.mode
Heap addresses
val mk_addr :
?esynthetic:bool ->
Framework.Core.Ast.Addr.addr ->
?etyp:Framework.Core.Ast.Typ.typ ->
?mode:Framework.Core.Ast.Var.mode option ->
Mopsa_utils.Core.Location.range ->
expr
Create an address expression
val mk_alloc_addr :
?esynthetic:bool ->
?mode:Framework.Core.Ast.Var.mode ->
Framework.Core.Ast.Addr.addr_kind ->
Mopsa_utils.Core.Location.range ->
expr
Create an allocation expression
Constant expressions
Constants
val mk_constant :
?esynthetic:bool ->
?etyp:Framework.Core.Ast.Typ.typ ->
Core.Ast.Constant.constant ->
Mopsa_utils.Core.Location.range ->
expr
Create a constant expression
val mk_top :
?esynthetic:bool ->
Framework.Core.Ast.Typ.typ ->
Mopsa_utils.Core.Location.range ->
expr
Create ⊤ expression of a given type
Unary expressions
Unary operator expressions
val mk_unop :
?esynthetic:bool ->
?etyp:Framework.Core.Ast.Typ.typ ->
Framework.Core.Ast.Operator.operator ->
expr ->
Mopsa_utils.Core.Location.range ->
expr
Create a unary operator expression
val mk_not :
?esynthetic:bool ->
expr ->
Mopsa_utils.Core.Location.range ->
expr
mk_not e range
returns the negation of expression e
using the operator Operator.O_log_not
Binary expressions
Binary operator expressions
val mk_binop :
?esynthetic:bool ->
?etyp:Framework.Core.Ast.Typ.typ ->
expr ->
Framework.Core.Ast.Operator.operator ->
expr ->
Mopsa_utils.Core.Location.range ->
expr
Create a binary operator expression
Expressions containers
module ExprSet = Mopsa_analyzer.Framework.Core.All.ExprSet
Sets of expression
module ExprMap = Mopsa_analyzer.Framework.Core.All.ExprMap
Maps of expressions
include module type of struct include Framework.Core.Ast.Stmt end
type stmt_kind = Framework.Core.Ast.Stmt.stmt_kind = ..
Extensible kinds of statements
type stmt = Framework.Core.Ast.Stmt.stmt = {
skind : stmt_kind;
(*kind of the statement
*)srange : Mopsa_utils.Core.Location.range;
(*location range of the statement
*)ssynthetic : bool;
(*whether the statement is generated during the analysis
*)
}
Statements
val mk_stmt :
?ssynthetic:bool ->
stmt_kind ->
Mopsa_utils.Core.Location.range ->
stmt
Create a statement
val srange : stmt -> Mopsa_utils.Core.Location.range
Get the location range of a statement
val ssynthetic : stmt -> bool
Whether the statement is generated during the analysis
val pp_stmt : Format.formatter -> stmt -> unit
Pretty-printer of statements
Registration
val register_stmt : stmt Mopsa_utils.Core.TypeExt.info -> unit
register_stmt info
registers a new statement by registering its compare function info.compare
and pretty-printer info.print
val register_stmt_compare : stmt Mopsa_utils.Core.TypeExt.compare -> unit
Register a comparison function for statements
val register_stmt_pp : stmt Mopsa_utils.Core.TypeExt.print -> unit
Register a pretty-printer function for statements
Blocks
type block = stmt list
Blocks are sequences of statements
val pp_block : Format.formatter -> block -> unit
Pretty-printer for blocks
Common statements
type stmt_kind +=
| S_program of Core.Ast.Program.program * string list option
(*Command-line arguments as given to Mopsa after
*)--
Programs
Assignments
val mk_assign :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Framework.Core.Ast.Expr.expr ->
Mopsa_utils.Core.Location.range ->
stmt
mk_assign lhs rhs range
creates the assignment lhs = rhs;
Tests
val mk_assume :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Mopsa_utils.Core.Location.range ->
stmt
Create a test statement
type stmt_kind +=
| S_add of Framework.Core.Ast.Expr.expr
(*Add a dimension to the environment
*)| S_remove of Framework.Core.Ast.Expr.expr
(*Remove a dimension from the environment and invalidate all references to it
*)| S_invalidate of Framework.Core.Ast.Expr.expr
(*Invalidate all references to a dimension without removing it
*)| S_rename of Framework.Core.Ast.Expr.expr * Framework.Core.Ast.Expr.expr
(*new
*)| S_forget of Framework.Core.Ast.Expr.expr
(*Forget a dimension by putting ⊤ (all possible values) in it. Note that the dimension is not removed
*)| S_project of Framework.Core.Ast.Expr.expr list
(*Project the environment on the given list of dimensions. All other dimensions are removed
*)| S_expand of Framework.Core.Ast.Expr.expr * Framework.Core.Ast.Expr.expr list
(*Expand a dimension into a list of other dimensions. The expanded dimension is untouched
*)| S_fold of Framework.Core.Ast.Expr.expr * Framework.Core.Ast.Expr.expr list
(*Fold a list of dimensions into a single one. The folded dimensions are removed
*)| S_block of stmt list * Framework.Core.Ast.Var.var list
(*local variables declared within the block
*)| S_breakpoint of string
(*Trigger a breakpoint
*)
Dimensions
val mk_rename :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Framework.Core.Ast.Expr.expr ->
Mopsa_utils.Core.Location.range ->
stmt
Utility functions to create various statements for dimension management
val mk_rename_var :
?ssynthetic:bool ->
Framework.Core.Ast.Var.var ->
Framework.Core.Ast.Var.var ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_remove :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_remove_var :
?ssynthetic:bool ->
Framework.Core.Ast.Var.var ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_invalidate :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_invalidate_var :
?ssynthetic:bool ->
Framework.Core.Ast.Var.var ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_add :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_add_var :
?ssynthetic:bool ->
Framework.Core.Ast.Var.var ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_project :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr list ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_project_vars :
?ssynthetic:bool ->
Framework.Core.Ast.Var.var list ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_forget :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_forget_var :
?ssynthetic:bool ->
Framework.Core.Ast.Var.var ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_expand :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Framework.Core.Ast.Expr.expr list ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_expand_var :
?ssynthetic:bool ->
Framework.Core.Ast.Var.var ->
Framework.Core.Ast.Var.var list ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_fold :
?ssynthetic:bool ->
Framework.Core.Ast.Expr.expr ->
Framework.Core.Ast.Expr.expr list ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_fold_var :
?ssynthetic:bool ->
Framework.Core.Ast.Var.var ->
Framework.Core.Ast.Var.var list ->
Mopsa_utils.Core.Location.range ->
stmt
val mk_breakpoint :
?ssynthetic:bool ->
string ->
Mopsa_utils.Core.Location.range ->
stmt
Containers of statements
module StmtSet = Mopsa_analyzer.Framework.Core.All.StmtSet
Sets of statements
module StmtMap = Mopsa_analyzer.Framework.Core.All.StmtMap
Maps of statements
include module type of struct include Framework.Core.Ast.Typ end
type typ = Framework.Core.Ast.Typ.typ = ..
Extensible types
val pp_typ : Format.formatter -> typ -> unit
Pretty-print a type
Registration
val register_typ : typ Mopsa_utils.Core.TypeExt.info -> unit
Register a new type
val register_typ_compare : typ Mopsa_utils.Core.TypeExt.compare -> unit
Register a new type comparison
val register_typ_pp : typ Mopsa_utils.Core.TypeExt.print -> unit
Register a new type pretty-printer
Common types
include module type of struct include Core.Ast.Program end
type prog_kind = Core.Ast.Program.prog_kind = ..
Extensible type of program kinds
type program = Core.Ast.Program.program = {
prog_kind : prog_kind;
(*kind of the program
*)prog_range : Mopsa_utils.Core.Location.range;
(*program location
*)
}
Programs
val pp_program : Format.formatter -> program -> unit
Pretty-printer for programs
Registration
val register_program : program Mopsa_utils.Core.TypeExt.info -> unit
register_program info
registers a new program kind by registering its comparison function info.compare
and pretty-printer info.print
val register_program_compare : program Mopsa_utils.Core.TypeExt.compare -> unit
Register a comparison function between programs
val register_program_pp : program Mopsa_utils.Core.TypeExt.print -> unit
Register a pretty-printer for programs
include module type of struct include Core.Ast.Frontend end
type frontend = Core.Ast.Frontend.frontend = {
lang : string;
(*Language of the frontend
*)parse : string list -> Core.Ast.Program.program;
(*Parser function that translates a list of input source files into a Mopsa
*)Program.program
on_panic : exn -> string list -> float -> unit;
(*Function called when the analysis of a program terminates with an exception, and *when the output is in text mode*. Provided with the exception, list of files and analysis time. Current usecase: provide automated testcase reduction capabilities in the C analysis.
*)
}
Frontends
val register_frontend : frontend -> unit
Register a new frontend
val find_language_frontend : string -> frontend
Find the frontend of a given language
include module type of struct include Framework.Core.Ast.Operator end
type operator = Framework.Core.Ast.Operator.operator = ..
Extensible type of operators
val pp_operator : Format.formatter -> operator -> unit
Pretty-printer of operators
Registration
val register_operator : operator Mopsa_utils.Core.TypeExt.info -> unit
register_operator info
registers a new operator by registering its compare function info.compare
and pretty-printer info.print
val register_operator_compare :
operator Mopsa_utils.Core.TypeExt.compare ->
unit
Register a comparison function for operators
val register_operator_pp : operator Mopsa_utils.Core.TypeExt.print -> unit
Register a pretty-printer for operators
Some common operators
type operator +=
| O_eq
(*equality ==
*)| O_ne
(*inequality !=
*)| O_lt
(*less than <
*)| O_le
(*less or equal <=
*)| O_gt
(*greater than >
*)| O_ge
(*greater or equal >=
*)| O_log_not
(*logical negation
*)| O_log_or
(*logical disjunction ||
*)| O_log_and
(*logical conjunction &&
*)| O_log_xor
(*logical strict disjonction xor
*)| O_cast
(*type cast
*)
Common operators
val is_comparison_op : operator -> bool
Test whether an operator is a comparison operator
val is_logic_op : operator -> bool
Test whether an is a logical operator
include module type of struct include Framework.Core.Ast.Var end
val print_uniq_with_uid : bool ref
Access modes
type var_kind = Framework.Core.Ast.Var.var_kind = ..
Extensible kind of variables
type mode = Framework.Core.Ast.Var.mode =
Access mode of a variable
val pp_mode : Format.formatter -> mode -> unit
Pretty-print an access mode
Variables
type var = Framework.Core.Ast.Var.var = {
vname : string;
(*unique name of the variable
*)vkind : var_kind;
(*kind the variable
*)vtyp : Framework.Core.Ast.Typ.typ;
(*type of the variable
*)vmode : mode;
(*access mode of the variable
*)vsemantic : Core.Ast.Semantic.semantic;
(*semantic of the variable
*)
}
Variables
val vname : var -> string
Accessor function to the fields of a variable
val vtyp : var -> Framework.Core.Ast.Typ.typ
val vsemantic : var -> Core.Ast.Semantic.semantic
val mkv :
string ->
var_kind ->
?mode:mode ->
?semantic:Core.Ast.Semantic.semantic ->
Framework.Core.Ast.Typ.typ ->
var
Create a variable with a unique name, a kind, a type and an access mode (STRONG if not given)
val pp_var : Format.formatter -> var -> unit
Pretty-print a variable
Registration
val register_var : var Mopsa_utils.Core.TypeExt.info -> unit
Register a new kind of variables
val register_var_compare : var Mopsa_utils.Core.TypeExt.compare -> unit
Register a new variable comparison
val register_var_pp : var Mopsa_utils.Core.TypeExt.print -> unit
Register a new variable pretty-printer
Common variables
type var_kind +=
| V_uniq of string * int
(*Unique ID
*)| V_tmp of int
(*Unique ID
*)| V_var_attr of var * string
(*Attribute
*)| V_range_attr of Mopsa_utils.Core.Location.range * string
(*Attribute
*)
val mk_uniq_var :
string ->
int ->
?mode:mode ->
Framework.Core.Ast.Typ.typ ->
var
Create a unique variable
val mk_fresh_uniq_var :
string ->
?mode:mode ->
Framework.Core.Ast.Typ.typ ->
unit ->
var
Create a fresh variable with a fresh ID
val mktmp : ?typ:Framework.Core.Ast.Typ.typ -> ?mode:mode -> unit -> var
Create a fresh temporary variable
val mk_attr_var :
var ->
string ->
?mode:mode ->
?semantic:Core.Ast.Semantic.semantic ->
Framework.Core.Ast.Typ.typ ->
var
mk_attr_var v a t
creates a variable representing an attribute a
of another variable v
val mk_range_attr_var :
Mopsa_utils.Core.Location.range ->
string ->
?mode:mode ->
?semantic:Core.Ast.Semantic.semantic ->
Framework.Core.Ast.Typ.typ ->
var
mk_range_attr_var r a t
creates a variable representing an attribute a
of a program location r
Containers for variables
module VarSet = Mopsa_analyzer.Framework.Core.All.VarSet
Sets of variables
module VarMap = Mopsa_analyzer.Framework.Core.All.VarMap
Maps of variables
Deprecated
val get_orig_vname : var -> string
include module type of struct include Framework.Core.Ast.Addr end
type addr_kind = Framework.Core.Ast.Addr.addr_kind = ..
Kind of heap addresses, used to store extra information.
val addr_kind_pp_chain : (Format.formatter -> addr_kind -> unit) ref
val pp_addr_kind : Format.formatter -> addr_kind -> unit
val register_addr_kind : addr_kind Mopsa_utils.Core.TypeExt.info -> unit
type addr_partitioning = Framework.Core.Ast.Addr.addr_partitioning = ..
Addresses are grouped by static criteria to make them finite
val addr_partitioning_compare_chain :
(addr_partitioning -> addr_partitioning -> int) ref
val addr_partitioning_pp_chain :
(Format.formatter -> addr_partitioning -> unit) ref
val opt_hash_addr : bool ref
Command line option to use hashes as address format
val pp_addr_partitioning_hash : Format.formatter -> addr_partitioning -> unit
val pp_addr_partitioning :
?full:bool ->
Format.formatter ->
addr_partitioning ->
unit
Print a partitioning policy. Flag full
overloads the option opt_hash_addr
and displays the full partitioning string (not its hash, which is useful for creating unique names of addresses)
val pp_addr_partitioning_full : Format.formatter -> addr_partitioning -> unit
val compare_addr_partitioning : addr_partitioning -> addr_partitioning -> int
val register_addr_partitioning :
addr_partitioning Mopsa_utils.Core.TypeExt.info ->
unit
type addr = Framework.Core.Ast.Addr.addr = {
addr_kind : addr_kind;
(*Kind of the address.
*)addr_partitioning : addr_partitioning;
(*Partitioning policy of the address
*)addr_mode : Framework.Core.Ast.Var.mode;
(*Assignment mode of address (string or weak)
*)
}
Heap addresses.
val pp_addr : Format.formatter -> addr -> unit
val addr_uniq_name : addr -> string
Get the unique name of an address. This is safer and faster than calling Format.asprintf "%s" pp_addr a
when opt_hash_addr
is set.
val addr_mode :
addr ->
Framework.Core.Ast.Var.mode option ->
Framework.Core.Ast.Var.mode
Address variables
val mk_addr_attr :
addr ->
string ->
Framework.Core.Ast.Typ.typ ->
Framework.Core.Ast.Var.var
include module type of struct include Core.Ast.Visitor end
type parts = Core.Ast.Visitor.parts = {
exprs : Framework.Core.Ast.Expr.expr list;
(*sub-expressions
*)stmts : Framework.Core.Ast.Stmt.stmt list;
(*sub-statements
*)
}
Parts of a statement/expression
val structure_of_expr :
Framework.Core.Ast.Expr.expr ->
Framework.Core.Ast.Expr.expr structure
Get the structure of an expression
val structure_of_stmt :
Framework.Core.Ast.Stmt.stmt ->
Framework.Core.Ast.Stmt.stmt structure
Get the structure of a statement
val leaf : 'a -> 'a structure
Visitor for leaf statements/expressions that have no sub-elements
Registration
type 'a visit_info = 'a Core.Ast.Visitor.visit_info = {
compare : 'a Mopsa_utils.Core.TypeExt.compare;
(*Comparison function for
*)'a
print : 'a Mopsa_utils.Core.TypeExt.print;
(*Pretty-printer for
*)'a'
visit : ('a -> 'a structure) -> 'a -> 'a structure;
(*Visitor for
*)'a
}
Registration descriptor for visitors
val register_expr_with_visitor :
Framework.Core.Ast.Expr.expr visit_info ->
unit
Register an expression with its visitor
val register_expr_visitor :
((Framework.Core.Ast.Expr.expr -> Framework.Core.Ast.Expr.expr structure) ->
Framework.Core.Ast.Expr.expr ->
Framework.Core.Ast.Expr.expr structure) ->
unit
Register a visitor of an expression
val register_stmt_with_visitor :
Framework.Core.Ast.Stmt.stmt visit_info ->
unit
Register a statement with its visitor
val register_stmt_visitor :
((Framework.Core.Ast.Stmt.stmt -> Framework.Core.Ast.Stmt.stmt structure) ->
Framework.Core.Ast.Stmt.stmt ->
Framework.Core.Ast.Stmt.stmt structure) ->
unit
Register a visitor of a statement
Visiting iterators
type 'a visit_action = 'a Core.Ast.Visitor.visit_action =
Actions of a visiting iterator
val map_expr :
(Framework.Core.Ast.Expr.expr -> Framework.Core.Ast.Expr.expr visit_action) ->
(Framework.Core.Ast.Stmt.stmt -> Framework.Core.Ast.Stmt.stmt visit_action) ->
Framework.Core.Ast.Expr.expr ->
Framework.Core.Ast.Expr.expr
map_expr fe fs e
transforms the expression e
into a new one by applying visitor action fe
and fs
on its sub-expression and sub-statements respectively
val map_stmt :
(Framework.Core.Ast.Expr.expr -> Framework.Core.Ast.Expr.expr visit_action) ->
(Framework.Core.Ast.Stmt.stmt -> Framework.Core.Ast.Stmt.stmt visit_action) ->
Framework.Core.Ast.Stmt.stmt ->
Framework.Core.Ast.Stmt.stmt
Similar to map_expr
but on statements
val fold_expr :
('a -> Framework.Core.Ast.Expr.expr -> 'a visit_action) ->
('a -> Framework.Core.Ast.Stmt.stmt -> 'a visit_action) ->
'a ->
Framework.Core.Ast.Expr.expr ->
'a
fold_expr fe fs e
folds the accumulated result of visitors fe
and fs
on the structure of expression e
val fold_stmt :
('a -> Framework.Core.Ast.Expr.expr -> 'a visit_action) ->
('a -> Framework.Core.Ast.Stmt.stmt -> 'a visit_action) ->
'a ->
Framework.Core.Ast.Stmt.stmt ->
'a
Similar to fold_expr
but on statements
val fold_map_expr :
('a ->
Framework.Core.Ast.Expr.expr ->
('a * Framework.Core.Ast.Expr.expr) visit_action) ->
('a ->
Framework.Core.Ast.Stmt.stmt ->
('a * Framework.Core.Ast.Stmt.stmt) visit_action) ->
'a ->
Framework.Core.Ast.Expr.expr ->
'a * Framework.Core.Ast.Expr.expr
Combination of map and fold for expressions
val fold_map_stmt :
('a ->
Framework.Core.Ast.Expr.expr ->
('a * Framework.Core.Ast.Expr.expr) visit_action) ->
('a ->
Framework.Core.Ast.Stmt.stmt ->
('a * Framework.Core.Ast.Stmt.stmt) visit_action) ->
'a ->
Framework.Core.Ast.Stmt.stmt ->
'a * Framework.Core.Ast.Stmt.stmt
Combination of map and fold for statements
val exists_expr :
(Framework.Core.Ast.Expr.expr -> bool) ->
(Framework.Core.Ast.Stmt.stmt -> bool) ->
Framework.Core.Ast.Expr.expr ->
bool
val for_all_expr :
(Framework.Core.Ast.Expr.expr -> bool) ->
(Framework.Core.Ast.Stmt.stmt -> bool) ->
Framework.Core.Ast.Expr.expr ->
bool
val iter_expr :
(Framework.Core.Ast.Expr.expr -> unit) ->
(Framework.Core.Ast.Stmt.stmt -> unit) ->
Framework.Core.Ast.Expr.expr ->
unit
val exists_stmt :
(Framework.Core.Ast.Expr.expr -> bool) ->
(Framework.Core.Ast.Stmt.stmt -> bool) ->
Framework.Core.Ast.Stmt.stmt ->
bool
val for_all_stmt :
(Framework.Core.Ast.Expr.expr -> bool) ->
(Framework.Core.Ast.Stmt.stmt -> bool) ->
Framework.Core.Ast.Stmt.stmt ->
bool
val iter_stmt :
(Framework.Core.Ast.Expr.expr -> unit) ->
(Framework.Core.Ast.Stmt.stmt -> unit) ->
Framework.Core.Ast.Stmt.stmt ->
unit
val exists_child_expr :
(Framework.Core.Ast.Expr.expr -> bool) ->
(Framework.Core.Ast.Stmt.stmt -> bool) ->
Framework.Core.Ast.Expr.expr ->
bool
val for_all_child_expr :
(Framework.Core.Ast.Expr.expr -> bool) ->
(Framework.Core.Ast.Stmt.stmt -> bool) ->
Framework.Core.Ast.Expr.expr ->
bool
val exists_child_stmt :
(Framework.Core.Ast.Expr.expr -> bool) ->
(Framework.Core.Ast.Stmt.stmt -> bool) ->
Framework.Core.Ast.Stmt.stmt ->
bool
val for_all_child_stmt :
(Framework.Core.Ast.Expr.expr -> bool) ->
(Framework.Core.Ast.Stmt.stmt -> bool) ->
Framework.Core.Ast.Stmt.stmt ->
bool
Utility functions
val is_leaf_expr : Framework.Core.Ast.Expr.expr -> bool
Test whether an expression is a leaf expression
val is_atomic_expr : Framework.Core.Ast.Expr.expr -> bool
Test whether an expression has no sub-statement
val is_atomic_stmt : Framework.Core.Ast.Stmt.stmt -> bool
Test whether a statement has no sub-statement
val expr_vars : Framework.Core.Ast.Expr.expr -> Framework.Core.Ast.Var.var list
Get all variables present in an expression
val stmt_vars : Framework.Core.Ast.Stmt.stmt -> Framework.Core.Ast.Var.var list
Get all variables present in a statement
val is_var_in_expr :
Framework.Core.Ast.Var.var ->
Framework.Core.Ast.Expr.expr ->
bool
Check whether a variable appears in an expression
val is_var_in_stmt :
Framework.Core.Ast.Var.var ->
Framework.Core.Ast.Stmt.stmt ->
bool
Check whether a variable appears in a statement
Deprecated
val fold_sub_expr :
('a -> Framework.Core.Ast.Expr.expr -> 'a visit_action) ->
('a -> Framework.Core.Ast.Stmt.stmt -> 'a visit_action) ->
'a ->
Framework.Core.Ast.Expr.expr ->
'a
include module type of struct include Framework.Core.Alarm end
Checks
**********
Domains can add new checks by extending the type check
and registering them using register_check
. Note that checks should be simple variant constructs without any argument.
type check = Framework.Core.Alarm.check = ..
val pp_check : Format.formatter -> check -> unit
Print a check
val register_check :
((Format.formatter -> check -> unit) -> Format.formatter -> check -> unit) ->
unit
Register a check with its printer
Alarms
**********
Alarms are issues related to a check in a given range and a given callstack. Domains can add new kinds of alarms to store information related to the issue, such suspect values that raised the alarm. Nevertheless, domains can use the generic alarm A_generic of check
if they don't have addition static information to attach to the alarm.
type alarm_kind = Framework.Core.Alarm.alarm_kind = ..
type alarm = Framework.Core.Alarm.alarm = {
alarm_kind : alarm_kind;
alarm_check : check;
alarm_range : Mopsa_utils.Core.Location.range;
alarm_callstack : Mopsa_utils.Core.Callstack.callstack;
}
val mk_alarm :
alarm_kind ->
Mopsa_utils.Core.Callstack.callstack ->
Mopsa_utils.Core.Location.range ->
alarm
Create an alarm
val range_of_alarm : alarm -> Mopsa_utils.Core.Location.range
Return the range of an alarm
val callstack_of_alarm : alarm -> Mopsa_utils.Core.Callstack.callstack
Return the callstack of an alarm
val pp_alarm : Format.formatter -> alarm -> unit
Print an alarm
val compare_alarm_kind : alarm_kind -> alarm_kind -> int
Compare two kinds of alarms
val pp_alarm_kind : Format.formatter -> alarm_kind -> unit
Print an alarm kind
val join_alarm_kind : alarm_kind -> alarm_kind -> alarm_kind option
Join two alarm kinds by merging the static information attached to them
val register_alarm_compare :
((alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int) ->
unit
Register a comparison function for alarms
val register_alarm_pp :
((Format.formatter -> alarm_kind -> unit) ->
Format.formatter ->
alarm_kind ->
unit) ->
unit
Register a print function for alarms
val register_alarm_check :
((alarm_kind -> check) -> alarm_kind -> check) ->
unit
Register a function giving the check of an alarm
val register_alarm_join :
((alarm_kind -> alarm_kind -> alarm_kind option) ->
alarm_kind ->
alarm_kind ->
alarm_kind option) ->
unit
Register a join function for alarms
type alarm_info = Framework.Core.Alarm.alarm_info = {
check : (alarm_kind -> check) -> alarm_kind -> check;
compare : (alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int;
print : (Format.formatter -> alarm_kind -> unit) -> Format.formatter -> alarm_kind -> unit;
join : (alarm_kind -> alarm_kind -> alarm_kind option) -> alarm_kind -> alarm_kind -> alarm_kind option;
}
Registration record for a new kind of alarms
val register_alarm : alarm_info -> unit
Register a new kind of alarms
Diagnostic
**************
A diagnostic gives the status of all alarms raised at the program location for the same check
module AlarmSet = Mopsa_analyzer.Framework.Core.All.AlarmSet
Set of alarms
type diagnostic_kind = Framework.Core.Alarm.diagnostic_kind =
Kind of a diagnostic
type 'a diagnostic_ = 'a Framework.Core.Alarm.diagnostic_ = {
diag_range : Mopsa_utils.Core.Location.range;
diag_check : check;
diag_kind : diagnostic_kind;
diag_alarms : AlarmSet.t;
diag_callstack : 'a;
}
type diagnostic = Mopsa_utils.Core.Callstack.callstack diagnostic_
type diagnosticWoCs = unit diagnostic_
val mk_safe_diagnostic :
check ->
Mopsa_utils.Core.Callstack.callstack ->
Mopsa_utils.Core.Location.range ->
diagnostic
Create a diagnostic that says that a check is safe
val mk_error_diagnostic : alarm -> diagnostic
Create a diagnostic that says that a check is unsafe
val mk_warning_diagnostic :
check ->
Mopsa_utils.Core.Callstack.callstack ->
Mopsa_utils.Core.Location.range ->
diagnostic
Create a diagnostic that says that a check maybe unsafe
val mk_unreachable_diagnostic :
check ->
Mopsa_utils.Core.Callstack.callstack ->
Mopsa_utils.Core.Location.range ->
diagnostic
Create a diagnostic that says that a check is unreachable
val pp_diagnostic_kind : Format.formatter -> diagnostic_kind -> unit
Print a diagnostic kind
val pp_diagnostic : Format.formatter -> diagnostic -> unit
Print a diagnostic
val subset_diagnostic : diagnostic -> diagnostic -> bool
Check whether a diagnostic is covered by another
val join_diagnostic : diagnostic -> diagnostic -> diagnostic
Compute the union of two diagnostics
val meet_diagnostic : diagnostic -> diagnostic -> diagnostic
Compute the intersection of two diagnostics
val add_alarm_to_diagnostic : alarm -> diagnostic -> diagnostic
Add an alarm to a diagnostic
val compare_diagnostic : diagnostic -> diagnostic -> int
Compare two diagnostics
Soundness assumption
************************
When a domain can't ensure total soundness when analyzing a piece of code, it can emit assumptions under which the result is still sound.
type assumption_scope = Framework.Core.Alarm.assumption_scope =
| A_local of Mopsa_utils.Core.Location.range
(*Local assumptions concern a specific location range in the program
*)| A_global
(*Global assumptions can concern the entire program
*)
Scope of an assumption
type assumption_kind = Framework.Core.Alarm.assumption_kind = ..
Domains can add new kinds of assumptions by extending the type assumption_kind
Generic assumptions for specifying potential unsoundness due to unsupported statements/expressions
type assumption = Framework.Core.Alarm.assumption = {
assumption_scope : assumption_scope;
assumption_kind : assumption_kind;
}
val register_assumption : assumption_kind Mopsa_utils.Core.TypeExt.info -> unit
Register a new kind of assumptions
val pp_assumption_kind : Format.formatter -> assumption_kind -> unit
Print an assumption kind
val pp_assumption : Format.formatter -> assumption -> unit
Print an assumption
val compare_assumption_kind : assumption_kind -> assumption_kind -> int
Compare two assumption kinds
val compare_assumption : assumption -> assumption -> int
Compare two assumptions
val mk_global_assumption : assumption_kind -> assumption
Create a global assumption
val mk_local_assumption :
assumption_kind ->
Mopsa_utils.Core.Location.range ->
assumption
Create a local assumption
Analysis report
*******************
Alarms are organized in a report that maps each range and each check to a diagnostic. A report also contains the set of soundness assumptions made by the domains.
module RangeMap = Mopsa_analyzer.Framework.Core.All.RangeMap
module RangeCallStackMap = Mopsa_analyzer.Framework.Core.All.RangeCallStackMap
module CheckMap = Mopsa_analyzer.Framework.Core.All.CheckMap
module AssumptionSet = Mopsa_analyzer.Framework.Core.All.AssumptionSet
type report = Framework.Core.Alarm.report = {
report_diagnostics : diagnostic CheckMap.t RangeCallStackMap.t;
report_assumptions : AssumptionSet.t;
}
val empty_report : report
Return an empty report
val is_empty_report : report -> bool
Checks whether a report is empty
val is_safe_report : report -> bool
Checks whether a report is safe, i.e. it doesn't contain an error or a warning
val is_sound_report : report -> bool
Checks whether a report is sound
val pp_report : Format.formatter -> report -> unit
Print a report
subset_report r1 r2
checks whether report r1
is included in r2
val filter_report : (diagnostic -> bool) -> report -> report
filter_report p r
keeps only diagnostics in report r
that verify predicate p
add_alarm a r
adds alarm a
to a report r
. If a diagnostic exists for the same range and the same check as a
, join_diagnostic
is used to join it with an error diagnostic containing a
.
val set_diagnostic : diagnostic -> report -> report
set_diagnostic d r
adds diagnostic d
to r
. Any existing diagnostic for the same range and the same check as d
is removed.
val add_diagnostic : diagnostic -> report -> report
add_diagnostic d r
adds diagnostic d
to r
. If a diagnostic exists for the same range and the same check as d
, join_diagnostic
is used to join it with d
.
val remove_diagnostic : diagnostic -> report -> report
Remove a diagnostic from a report
val find_diagnostic :
(Mopsa_utils.Core.Location.range * Mopsa_utils.Core.Callstack.callstack) ->
check ->
report ->
diagnostic
find_diagnostic range chk r
finds the diagnostic of check chk
at location range
in report r
val exists_report : (diagnostic -> bool) -> report -> bool
Check whether any diagnostic verifies a predicate
val forall_report : (diagnostic -> bool) -> report -> bool
Check whether all diagnostics verify a predicate
val count_alarms : report -> int * int
Count the number of alarms and warnings in a report
module RangeDiagnosticWoCsMap =
Mopsa_analyzer.Framework.Core.All.RangeDiagnosticWoCsMap
module CallstackSet = Mopsa_analyzer.Framework.Core.All.CallstackSet
Set of callstacks
val group_diagnostics :
diagnostic CheckMap.t RangeCallStackMap.t ->
CallstackSet.t RangeDiagnosticWoCsMap.t
Group diagnostics by their range and diagnostic kind
val add_assumption : assumption -> report -> report
Add an assumption to a report
val add_global_assumption : assumption_kind -> report -> report
Add a global assumption to a report
val add_local_assumption :
assumption_kind ->
Mopsa_utils.Core.Location.range ->
report ->
report
Add a local assumption to a report
val map2zo_report :
(diagnostic -> diagnostic) ->
(diagnostic -> diagnostic) ->
(diagnostic -> diagnostic -> diagnostic) ->
report ->
report ->
report
val fold2zo_report :
(diagnostic -> 'b -> 'b) ->
(diagnostic -> 'b -> 'b) ->
(diagnostic -> diagnostic -> 'b -> 'b) ->
report ->
report ->
'b ->
'b
val exists2zo_report :
(diagnostic -> bool) ->
(diagnostic -> bool) ->
(diagnostic -> diagnostic -> bool) ->
report ->
report ->
bool
val fold_report : (diagnostic -> 'b -> 'b) -> report -> 'b -> 'b
module Alarm = Mopsa_analyzer.Framework.Core.All.Alarm
include module type of struct include Framework.Core.Context end
type ('a, _) ctx_key = ('a, _) Framework.Core.Context.ctx_key = ..
Key to access an element in the context
type 'a ctx = 'a Framework.Core.Context.ctx
The context
val empty_ctx : 'a ctx
Empty context
mem_ctx k ctx
returns true
when an element at key k
is in the context ctx
.
find_ctx k ctx
returns the element at key k
in the context ctx
. Raises Not_found
if no element is found.
find_ctx k ctx
returns the element of the key k
in the context ctx
. Returns None
if no element is found.
add_ctx k v ctx
add element v
at key k
in the context ctx
. The previous element is overwritten if present.
add_ctx k v ctx
removes the element at key k
in the context ctx
. If key k
was not in ctx
, ctx
is returned unchanged.
val pp_ctx :
(Framework.Core.Print.printer -> 'a -> unit) ->
Format.formatter ->
'a ctx ->
unit
Print a context
type ctx_pool = Framework.Core.Context.ctx_pool = {
ctx_pool_equal : 'a 'v 'w. ('a, 'v) ctx_key -> ('a, 'w) ctx_key -> ('v, 'w) Mopsa_utils.Core.Eq.eq option;
ctx_pool_print : 'a 'v. (Framework.Core.Print.printer -> 'a -> unit) -> Format.formatter -> ('a, 'v) ctx_key -> 'v -> unit;
}
Pool registered keys
type ctx_info = Framework.Core.Context.ctx_info = {
ctx_equal : 'a 'v 'w. ctx_pool -> ('a, 'v) ctx_key -> ('a, 'w) ctx_key -> ('v, 'w) Mopsa_utils.Core.Eq.eq option;
ctx_print : 'a 'v. ctx_pool -> (Framework.Core.Print.printer -> 'a -> unit) -> Format.formatter -> ('a, 'v) ctx_key -> 'v -> unit;
}
Registration information for a new key
val register_ctx : ctx_info -> unit
Register a new key
module GenContextKey = Mopsa_analyzer.Framework.Core.All.GenContextKey
Generate a new key
val control_ctx_key : ('a, Mopsa_utils.Core.ControlCtx.control_ctx) ctx_key
Key for storing the control context
module Context = Mopsa_analyzer.Framework.Core.All.Context
module Cases = Mopsa_analyzer.Framework.Core.All.Cases
type 'r case = 'r Cases.case
type ('a, 'r) cases = ('a, 'r) Cases.cases
val bind :
('a Cases.case -> 'b Core.Flow.flow -> ('b, 'c) Cases.cases) ->
('b, 'a) Cases.cases ->
('b, 'c) Cases.cases
val (>>=) :
('a, 'b) Cases.cases ->
('b Cases.case -> 'a Core.Flow.flow -> ('a, 'c) Cases.cases) ->
('a, 'c) Cases.cases
val bind_opt :
('a Cases.case -> 'b Core.Flow.flow -> ('b, 'c) Cases.cases option) ->
('b, 'a) Cases.cases ->
('b, 'c) Cases.cases option
val (>>=?) :
('a, 'b) Cases.cases ->
('b Cases.case -> 'a Core.Flow.flow -> ('a, 'c) Cases.cases option) ->
('a, 'c) Cases.cases option
val bind_result :
('a -> 'b Core.Flow.flow -> ('b, 'c) Cases.cases) ->
('b, 'a) Cases.cases ->
('b, 'c) Cases.cases
val (>>$) :
('a, 'b) Cases.cases ->
('b -> 'a Core.Flow.flow -> ('a, 'c) Cases.cases) ->
('a, 'c) Cases.cases
val bind_result_opt :
('a -> 'b Core.Flow.flow -> ('b, 'c) Cases.cases option) ->
('b, 'a) Cases.cases ->
('b, 'c) Cases.cases option
val (>>$?) :
('a, 'b) Cases.cases ->
('b -> 'a Core.Flow.flow -> ('a, 'c) Cases.cases option) ->
('a, 'c) Cases.cases option
val bind_list :
'a list ->
('a -> 'b Core.Flow.flow -> ('b, 'c) Cases.cases) ->
'b Core.Flow.flow ->
('b, 'c list) Cases.cases
val bind_list_opt :
'a list ->
('a -> 'b Core.Flow.flow -> ('b, 'c) Cases.cases option) ->
'b Core.Flow.flow ->
('b, 'c list) Cases.cases option
module Eval = Mopsa_analyzer.Framework.Core.All.Eval
type 'a eval = 'a Eval.eval
module Flow = Mopsa_analyzer.Framework.Core.All.Flow
type 'a flow = 'a Flow.flow
module Post = Mopsa_analyzer.Framework.Core.All.Post
type 'a post = 'a Post.post
val (>>%) :
'a Post.post ->
('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) ->
('a, 'b) Core.Cases.cases
val (>>%?) :
'a Post.post ->
('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases option) ->
('a, 'b) Core.Cases.cases option
module Path = Mopsa_analyzer.Framework.Core.All.Path
include module type of struct include Path end
type accessor = Core.Path.accessor = ..
type path = accessor list
val accessor_compare_chain : accessor Mopsa_utils.Core.TypeExt.compare_chain
val accessor_print_chain : accessor Mopsa_utils.Core.TypeExt.print_chain
val pp_accessor : Format.formatter -> accessor -> unit
val register_accessor : accessor Mopsa_utils.Core.TypeExt.info -> unit
val pp_path : Format.formatter -> accessor list -> unit
val empty_path : path
module PathMap = Mopsa_analyzer.Framework.Core.All.PathMap
module PathSet = Mopsa_analyzer.Framework.Core.All.PathSet
module Change = Mopsa_analyzer.Framework.Core.All.Change
include module type of struct include Change end
type change = Framework.Core.Change.change =
val pp_change : Format.formatter -> change -> unit
val empty_change : change
val is_empty_change : change -> bool
val add_stmt_to_change : Framework.Core.Ast.Stmt.stmt -> change -> change
Join two changes
type change_map = change Core.Path.PathMap.t
val pp_change_map : Format.formatter -> change Core.Path.PathMap.t -> unit
val compare_change_map :
change Core.Path.PathMap.t ->
change Core.Path.PathMap.t ->
int
val empty_change_map : 'a Core.Path.PathMap.t
val singleton_change_map :
Core.Path.PathMap.key ->
'a ->
'a Core.Path.PathMap.t
val is_empty_change_map : change Core.Path.PathMap.t -> bool
val concat_change_map :
change Core.Path.PathMap.t ->
change Core.Path.PathMap.t ->
change Core.Path.PathMap.t
val join_change_map :
change Core.Path.PathMap.t ->
change Core.Path.PathMap.t ->
change Core.Path.PathMap.t
val meet_change_map :
change Core.Path.PathMap.t ->
change Core.Path.PathMap.t ->
change Core.Path.PathMap.t
val get_change : Core.Path.PathMap.key -> change Core.Path.PathMap.t -> change
val add_stmt_to_change_map :
Framework.Core.Ast.Stmt.stmt ->
Core.Path.PathMap.key ->
change Core.Path.PathMap.t ->
change Core.Path.PathMap.t
Generic merge
*****************
type change_vars = Framework.Core.Change.change_vars = {
modified : Framework.Core.Ast.Var.VarSet.t;
removed : Framework.Core.Ast.Var.VarSet.t;
}
Change of a statement in terms of modified and removed variables
val compare_change_vars : change_vars -> change_vars -> int
val is_empty_change_vars : change_vars -> bool
val get_stmt_change_vars :
custom:(Framework.Core.Ast.Stmt.stmt -> change_vars option) ->
Framework.Core.Ast.Stmt.stmt ->
change_vars
Get the changes of a statement
val get_change_vars :
custom:(Framework.Core.Ast.Stmt.stmt -> change_vars option) ->
change ->
change_vars
val apply_change_vars :
change_vars ->
add:(Framework.Core.Ast.Var.VarSet.elt -> 'b -> 'a -> 'a) ->
remove:(Framework.Core.Ast.Var.VarSet.elt -> 'a -> 'a) ->
find:(Framework.Core.Ast.Var.VarSet.elt -> 'a -> 'b) ->
'a ->
'a ->
'a
Apply changes on an abstract element
val generic_merge :
add:(Framework.Core.Ast.Var.VarSet.elt -> 'a -> 'b -> 'b) ->
find:(Framework.Core.Ast.Var.VarSet.elt -> 'b -> 'a) ->
remove:(Framework.Core.Ast.Var.VarSet.elt -> 'b -> 'b) ->
?custom:(Framework.Core.Ast.Stmt.stmt -> change_vars option) ->
('b * change) ->
('b * change) ->
'b * 'b
Generic merge operator for non-relational domains
val opt_change_tracker_enabled : bool ref
include module type of struct include Framework.Core.Query end
type ('a, _) query = ('a, _) Framework.Core.Query.query = ..
Extensible type of queries
val join_query :
?ctx:'a Framework.Core.Context.ctx option ->
?lattice:'a Framework.Core.Lattice.lattice option ->
('a, 'r) query ->
'r ->
'r ->
'r
Join two queries
val meet_query :
?ctx:'a Framework.Core.Context.ctx option ->
?lattice:'a Framework.Core.Lattice.lattice option ->
('a, 'r) query ->
'r ->
'r ->
'r
Meet two queries
Registration
****************
type query_pool = Framework.Core.Query.query_pool = {
pool_join : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
pool_meet : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
}
Pool of registered queries
type query_info = Framework.Core.Query.query_info = {
join : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
meet : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
}
Registraction info for new queries
val register_query : query_info -> unit
Register a new query
type lattice_query_pool = Framework.Core.Query.lattice_query_pool = {
pool_join : 'a 'r. 'a Framework.Core.Context.ctx -> 'a Framework.Core.Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
pool_meet : 'a 'r. 'a Framework.Core.Context.ctx -> 'a Framework.Core.Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}
Pool of registered lattice queries. Lattice queries are queries that return elements of the global abstract state lattice. Join/meet operators are enriched with the lattice and the context so that we can compute join/meet over the abstract elements.
type lattice_query_info = Framework.Core.Query.lattice_query_info = {
join : 'a 'r. lattice_query_pool -> 'a Framework.Core.Context.ctx -> 'a Framework.Core.Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
meet : 'a 'r. lattice_query_pool -> 'a Framework.Core.Context.ctx -> 'a Framework.Core.Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}
Registration info for new lattice queries
val register_lattice_query : lattice_query_info -> unit
Register a new lattice query
Common queries
******************
type query +=
| Q_defined_variables : string option -> ('a, Framework.Core.Ast.Var.var list) query
(*Extract the list of defined variables, in a given function call site, or in all scopes
*)| Q_allocated_addresses : ('a, Framework.Core.Ast.Addr.addr list) query
(*Query to extract the list of addresses allocated in the heap
*)| Q_variables_linked_to : Framework.Core.Ast.Expr.expr -> ('a, Framework.Core.Ast.Var.VarSet.t) query
(*Query to extract the auxiliary variables related to an expression
*)
include module type of struct include Core.Token end
type token = Core.Token.token = ..
Flow tokens are used to distinguish between different control flows
val register_token : token Mopsa_utils.Core.TypeExt.info -> unit
Register a new token with its compare and print functions
val pp_token : Format.formatter -> token -> unit
Pretty printer of tokens
module TokenMap = Mopsa_analyzer.Framework.Core.All.TokenMap
include module type of struct include Core.Ast.Semantic end
val pp_semantic : Format.formatter -> semantic -> unit
val any_semantic : semantic
val is_any_semantic : semantic -> bool
module SemanticSet = Mopsa_analyzer.Framework.Core.All.SemanticSet
module SemanticMap = Mopsa_analyzer.Framework.Core.All.SemanticMap
include module type of struct include Core.Route end
type route = Core.Route.route =
| Below of domain
(*Sub-tree below a domain
*)| Semantic of Core.Ast.Semantic.semantic
(*Sub-tree identified by a semantic
*)
Routes
module DomainSet = Mopsa_analyzer.Framework.Core.All.DomainSet
val pp_route : Format.formatter -> route -> unit
Print a route
val toplevel : route
Toplevel tree
type routing_table = Core.Route.routing_table
Routing table providing the domains that are part of a route
val empty_routing_table : routing_table
Empty routing table
val resolve_route : route -> routing_table -> DomainSet.t
Resolve a route into domains
val add_route : route -> domain -> routing_table -> routing_table
Add a route between a route and a domain
val add_routes : route -> DomainSet.t -> routing_table -> routing_table
Add a set of routing_table linking a route and a set of domains
val get_routes : routing_table -> route list
Get all routing_table in a routing table
val join_routing_table : routing_table -> routing_table -> routing_table
Join two routing_table table
val pp_routing_table : Format.formatter -> routing_table -> unit
Print a routing table
include module type of struct include Framework.Core.Lattice end
module type LATTICE = Framework.Core.All.LATTICE
Signature of a lattice module.
type 'a lattice = 'a Framework.Core.Lattice.lattice = {
bottom : 'a;
top : 'a;
is_bottom : 'a -> bool;
subset : 'a Framework.Core.Context.ctx -> 'a -> 'a -> bool;
join : 'a Framework.Core.Context.ctx -> 'a -> 'a -> 'a;
meet : 'a Framework.Core.Context.ctx -> 'a -> 'a -> 'a;
widen : 'a Framework.Core.Context.ctx -> 'a -> 'a -> 'a;
merge : 'a -> ('a * Framework.Core.Change.change_map) -> ('a * Framework.Core.Change.change_map) -> 'a;
print : Framework.Core.Print.printer -> 'a -> unit;
}
Lattice operators
include module type of struct include Core.Id end
type _ id = _ Core.Id.id = ..
Identifiers
type witness = Core.Id.witness = {
eq : 'a 'b. 'a id -> 'b id -> ('a, 'b) Mopsa_utils.Core.Eq.eq option;
}
type witness_chain = Core.Id.witness_chain = {
eq : 'a 'b. witness -> 'a id -> 'b id -> ('a, 'b) Mopsa_utils.Core.Eq.eq option;
}
Equality witness of an identifier
val register_id : witness_chain -> unit
Register a new descriptor
val equal_id : 'a id -> 'b id -> ('a, 'b) Mopsa_utils.Core.Eq.eq option
Equality witness of identifiers
module GenDomainId = Mopsa_analyzer.Framework.Core.All.GenDomainId
Generator of a new domain identifier
module GenStatelessDomainId =
Mopsa_analyzer.Framework.Core.All.GenStatelessDomainId
Generator of a new identifier for stateless domains
module GenValueId = Mopsa_analyzer.Framework.Core.All.GenValueId
Generator of a new value identifier
include module type of struct include Framework.Core.Manager end
Managers
type ('a, 't) man = ('a, 't) Framework.Core.Manager.man = {
lattice : 'a Framework.Core.Lattice.lattice;
(*Access to lattice operators on the toplevel abstract element
*)'a
.get : Core.Token.token -> 'a Core.Flow.flow -> ('a, 't) Core.Cases.cases;
(*Returns the domain's abstract element
*)'t
. A disjunction of cases is returned when partitioning is used.set : Core.Token.token -> 't -> 'a Core.Flow.flow -> 'a Core.Post.post;
(*Sets the domain's abstract element
*)'t
.exec : ?route:Core.Route.route -> Framework.Core.Ast.Stmt.stmt -> 'a Core.Flow.flow -> 'a Core.Post.post;
(*
*)man.exec stmt flow
executesstmt
inflow
and returns the post state.eval : ?route:Core.Route.route -> ?translate:Core.Ast.Semantic.semantic -> ?translate_when: (Core.Ast.Semantic.semantic * (Framework.Core.Ast.Expr.expr -> bool)) list -> Framework.Core.Ast.Expr.expr -> 'a Core.Flow.flow -> 'a Framework.Core.Eval.eval;
(*man.eval expr flow
evaluatesexpr
inflow
and returns the result expression.There are two kinds of evaluations: within the same semantic (simplifications), or to another semantic (translations). Calling
*)man.eval expr flow
performs both kinds of evaluations. The resulte'
ofman.eval expr flow
is a simplification ofe
within the same semantic. To retrieve a translation to another semantic, one can use the?translate
parameter:man.eval expr flow ~translate:semantic
is a translation of the simplification ofe
insemantic
. A common use case is to translate expressions to Universal withman.eval expr flow ~translate:"Universal"
. It is possible to control when the translation is applied with?translate_when
.ask : 'r. ?route:Core.Route.route -> ('a, 'r) Framework.Core.Query.query -> 'a Core.Flow.flow -> ('a, 'r) Core.Cases.cases;
(*
*)man.ask query flow
performs a query to other domains. If no domain can answer the query,man.ask query flow
results in a runtime error.print_expr : ?route:Core.Route.route -> 'a Core.Flow.flow -> Framework.Core.Print.printer -> Framework.Core.Ast.Expr.expr -> unit;
(*
*)man.print_expr flow
is the expression printer for the type'a
.add_change : Framework.Core.Ast.Stmt.stmt -> Core.Path.path -> 'a Core.Flow.flow -> Framework.Core.Change.change_map -> Framework.Core.Change.change_map;
(*Add a statement to the changes map.
*)
}
Managers provide access to full analyzer.
'a
is the type of the toplevel abstract element, and 't
is the type of local abstract element (that is, the type of the domain that calls the manager).
module Hook = Mopsa_analyzer.Framework.Core.All.Hook
include module type of struct include Framework.Core.Print end
Print objects
Symbols for printing maps, lists and sets
type ('k, 'v) map = ('k, 'v) Mopsa_utils.Containers.MapExtPoly.t
Structured print objects
type 'v set = 'v Mopsa_utils.Containers.SetExtPoly.t
type print_object = Framework.Core.Print.print_object =
| Empty
| Bool of bool
| Int of Z.t
| Float of float
| String of string
| Var of Framework.Core.Ast.Var.var
| Map of (print_object, print_object) map * symbols
| List of print_object list * symbols
| Set of print_object set * symbols
Printers
type printer = Framework.Core.Print.printer
Printers encapsulate the structured objects to print along the history of printed expression
val empty_printer : unit -> printer
Create an empty printer
val get_printed_object : printer -> print_object
Get the structured print object of a printer
val get_printed_exprs : printer -> Framework.Core.Ast.Expr.expr list
Get the expressions that were already printed
val add_printed_expr : printer -> Framework.Core.Ast.Expr.expr -> unit
Mark an expression as printed
val mem_printed_expr : printer -> Framework.Core.Ast.Expr.expr -> bool
Check whether an expression was already printed
Print paths
type print_selector = Framework.Core.Print.print_selector =
| Key of string
| Index of int
| Obj of print_object
Selectors of print objects
type print_path = print_selector list
Path of a print object
val find_print_object : print_path -> print_object -> print_object
find_print_object path obj
returns the object placed at path
in obj
val match_print_object_keys : Str.regexp -> print_object -> print_object
match_print_object_keys re obj
slices obj
to paths containing keys that match re
Generic print functions
val pprint : ?path:print_path -> printer -> print_object -> unit
pprint ~path:p printer o
prints object o
at path p
in printer
.
val pbox : (printer -> 'a -> unit) -> 'a -> print_object
pbox f x
returns a boxed object created by f
when applied to x
. It is equivalent to
let printer = empty_printer () in
f printer x;
get_printed_object printer
val fbox : ('a, Format.formatter, unit, print_object) format4 -> 'a
fbox fmt
returns a string object of a formatted value
val sprint : (printer -> 'a -> unit) -> 'a -> string
sprint f x
returns the string representing the boxed object pbox f x
val fkey : ('a, Format.formatter, unit, print_selector) format4 -> 'a
fkey fmt
returns a key selector with a formatted string
val pkey : (printer -> 'a -> unit) -> 'a -> print_selector
pkey f x
returns a key selector with a printed string
Typed print functions
val pp_string : ?path:print_path -> printer -> string -> unit
Print a string object
val pp_bool : ?path:print_path -> printer -> bool -> unit
Print a boolean object
val pp_int : ?path:print_path -> printer -> int -> unit
Print an integer object
val pp_z : ?path:print_path -> printer -> Z.t -> unit
Print an integer object
val pp_float : ?path:print_path -> printer -> float -> unit
Print a float object
val pp_variable :
?path:print_path ->
printer ->
Framework.Core.Ast.Var.var ->
unit
Print a variable
val pp_list :
?path:print_path ->
?lopen:string ->
?lsep:string ->
?lclose:string ->
(printer -> 'a -> unit) ->
printer ->
'a list ->
unit
pp_list ~path:p f printer l
prints a list l
at path p
by boxing f
on every element of l
val pp_obj_list :
?path:print_path ->
?lopen:string ->
?lsep:string ->
?lclose:string ->
printer ->
print_object list ->
unit
pp_obj_list ~path:p printer l
prints a list of objects at path p
. Useful for printing heterogenous lists.
val pp_map :
?path:print_path ->
?mopen:string ->
?msep:string ->
?mclose:string ->
?mbind:string ->
(printer -> 'k -> unit) ->
(printer -> 'v -> unit) ->
printer ->
('k * 'v) list ->
unit
pp_smap ~path:p fk fv printer l
prints a map from a list l
of pairs of keys and values. Keys are boxed with function fk
and values with function fv
.
val pp_mapi :
?path:print_path ->
?mopen:string ->
?msep:string ->
?mclose:string ->
?mbind:string ->
(printer -> 'k -> unit) ->
(printer -> ('k * 'v) -> unit) ->
printer ->
('k * 'v) list ->
unit
val pp_obj_map :
?path:print_path ->
?mopen:string ->
?msep:string ->
?mclose:string ->
?mbind:string ->
printer ->
(print_object * print_object) list ->
unit
pp_obj_smap ~path:p printer l
prints a map from a list of pairs of print objects
val pp_obj_set :
?path:print_path ->
?sopen:string ->
?ssep:string ->
?sclose:string ->
printer ->
print_object set ->
unit
pp_obj_set ~path:p printer l
prints a set of objects at path p
. Useful for printing heterogenous sets.
val pp_set :
?path:print_path ->
?sopen:string ->
?ssep:string ->
?sclose:string ->
(printer -> 'a -> unit) ->
printer ->
'a set ->
unit
pp_set ~path:p f printer l
prints a set from a list l
at path p
by boxing f
on every element of l
Format
val pp_print_object : Format.formatter -> print_object -> unit
Pretty-print a printer objct
val pflush : Format.formatter -> printer -> unit
Pretty-print the printer output in a format string
val format : (printer -> 'a -> unit) -> Format.formatter -> 'a -> unit
Convert a printer function into a format function
val unformat :
?path:print_path ->
(Format.formatter -> 'a -> unit) ->
printer ->
'a ->
unit
Convert a format function into a printer
JSON
val print_object_to_json : print_object -> Yojson.Basic.t
Convert a printer object to JSON
val json_to_print_object : Yojson.Basic.t -> print_object
Convert JSON to a printer object
module Print = Mopsa_analyzer.Framework.Core.All.Print
include module type of struct include Core.Avalue end
type _ avalue_kind = _ Core.Avalue.avalue_kind = ..
type avalue_pool = Core.Avalue.avalue_pool = {
pool_typ : 'v. 'v avalue_kind -> Framework.Core.Ast.Typ.typ;
pool_bottom : 'v. 'v avalue_kind -> 'v;
pool_top : 'v. 'v avalue_kind -> 'v;
pool_join : 'v. 'v avalue_kind -> 'v -> 'v -> 'v;
pool_meet : 'v. 'v avalue_kind -> 'v -> 'v -> 'v;
pool_compare : 'v 'w. 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int;
pool_print : 'v. 'v avalue_kind -> Format.formatter -> 'v -> unit;
}
type avalue_info = Core.Avalue.avalue_info = {
typ : 'v. avalue_pool -> 'v avalue_kind -> Framework.Core.Ast.Typ.typ;
bottom : 'v. avalue_pool -> 'v avalue_kind -> 'v;
top : 'v. avalue_pool -> 'v avalue_kind -> 'v;
join : 'v. avalue_pool -> 'v avalue_kind -> 'v -> 'v -> 'v;
meet : 'v. avalue_pool -> 'v avalue_kind -> 'v -> 'v -> 'v;
compare : 'v 'w. avalue_pool -> 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int;
print : 'v. avalue_pool -> 'v avalue_kind -> Format.formatter -> 'v -> unit;
}
val register_avalue : avalue_info -> unit
val type_of_avalue : 'v avalue_kind -> Framework.Core.Ast.Typ.typ
val bottom_avalue : 'v avalue_kind -> 'v
val top_avalue : 'v avalue_kind -> 'v
val join_avalue : 'v avalue_kind -> 'v -> 'v -> 'v
val meet_avalue : 'v avalue_kind -> 'v -> 'v -> 'v
val compare_avalue : 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int
val pp_avalue : 'v avalue_kind -> Format.formatter -> 'v -> unit
val mk_avalue_expr :
'v avalue_kind ->
'v ->
Mopsa_utils.Core.Location.range ->
Framework.Core.Ast.Expr.expr
val mk_avalue_constant : 'v avalue_kind -> 'v -> Core.Ast.Constant.constant
type Framework.Core.Query.query +=
| Q_avalue : Framework.Core.Ast.Expr.expr * 'v avalue_kind -> ('a, 'v) Framework.Core.Query.query
val mk_avalue_query :
Framework.Core.Ast.Expr.expr ->
'v avalue_kind ->
('a, 'v) Framework.Core.Query.query
include module type of struct include Core.Utils end
val exec_cleaner :
Framework.Core.Ast.Stmt.stmt ->
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
('a, unit) Core.Cases.cases
val exec_cleaners :
('a, 'b) Framework.Core.Manager.man ->
('a, unit) Core.Cases.cases ->
('a, unit) Core.Cases.cases
val post_to_flow :
('a, 'b) Framework.Core.Manager.man ->
'a Core.Post.post ->
'a Core.Flow.flow
val assume :
Framework.Core.Ast.Expr.expr ->
?route:Core.Route.route ->
?translate:Core.Ast.Semantic.semantic ->
fthen:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) ->
felse:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) ->
?fboth:('a Core.Flow.flow -> 'a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) ->
?fnone:('a Core.Flow.flow -> 'a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) ->
?eval:bool ->
('a, 'c) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
('a, 'b) Core.Cases.cases
val switch :
(Framework.Core.Ast.Expr.expr list
* ('a Core.Flow.flow ->
('a, 'r) Core.Cases.cases))
list ->
?route:Core.Route.route ->
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
('a, 'r) Core.Cases.cases
val set_env :
Core.Token.token ->
't ->
('a, 't) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
'a Core.Post.post
val set_singleton_env :
'a ->
'b Framework.Core.Context.ctx ->
('b, 'a) Framework.Core.Manager.man ->
'b ->
'b
val set_env_flow :
Core.Token.token ->
'b ->
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
'a Core.Flow.flow
val get_env :
Core.Token.token ->
('a, 't) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
('a, 't) Core.Cases.cases
val get_singleton_env :
'a Framework.Core.Context.ctx ->
('a, 'b) Framework.Core.Manager.man ->
'a ->
'b
val get_singleton_env_from_flow :
Core.Token.token ->
('a, 't) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
't
val map_env :
Core.Token.token ->
('t -> 't) ->
('a, 't) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
'a Core.Post.post
val get_pair_fst :
('a, 'b * 'c) Framework.Core.Manager.man ->
Core.Token.token ->
'a Core.Flow.flow ->
('a, 'b) Core.Cases.cases
val set_pair_fst :
('a, 'b * 'c) Framework.Core.Manager.man ->
Core.Token.token ->
'b ->
'a Core.Flow.flow ->
('a, unit) Core.Cases.cases
val get_pair_snd :
('a, 'b * 'c) Framework.Core.Manager.man ->
Core.Token.token ->
'a Core.Flow.flow ->
('a, 'c) Core.Cases.cases
val set_pair_snd :
('a, 'b * 'c) Framework.Core.Manager.man ->
Core.Token.token ->
'c ->
'a Core.Flow.flow ->
('a, unit) Core.Cases.cases
val env_exec :
('a Core.Flow.flow -> 'a Core.Post.post) ->
'a Framework.Core.Context.ctx ->
('a, 't) Framework.Core.Manager.man ->
'a ->
'a
val ask_and_reduce_cases :
(('a, 'b) Framework.Core.Query.query -> 'c -> ('d, 'b) Core.Cases.cases) ->
('a, 'b) Framework.Core.Query.query ->
?bottom:(unit -> 'b) ->
'c ->
'b
val ask_and_reduce_list :
(('a, 'b) Framework.Core.Query.query -> 'c -> ('d * 'b) list) ->
('a, 'b) Framework.Core.Query.query ->
?bottom:(unit -> 'b) ->
'c ->
'b
val ask_and_reduce :
(('a, 'b) Framework.Core.Query.query -> 'c -> ('d, 'b) Core.Cases.cases) ->
('a, 'b) Framework.Core.Query.query ->
?bottom:(unit -> 'b) ->
'c ->
'b
val find_var_by_name :
?function_scope:string option ->
string ->
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
Framework.Core.Ast.Var.var
val dummy_range : Mopsa_utils.Core.Location.range
val pp_vars_info :
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
Format.formatter ->
Framework.Core.Ast.Var.var list ->
unit
val pp_vars_info_by_name :
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
Format.formatter ->
string list ->
unit
val pp_expr_vars_info :
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
Format.formatter ->
Framework.Core.Ast.Expr.expr ->
unit
val pp_stmt_vars_info :
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
Format.formatter ->
Framework.Core.Ast.Stmt.stmt ->
unit
val breakpoint :
string ->
('a, 'b) Framework.Core.Manager.man ->
'a Core.Flow.flow ->
unit
val warn_prototype_domain : string -> 'a Core.Flow.flow -> 'a Core.Flow.flow
val warn_no_guaranteed_termination_domain :
string ->
'a Core.Flow.flow ->
'a Core.Flow.flow
val warn_assumptions :
Framework.Core.Alarm.assumption_kind list ->
'a Core.Flow.flow ->
'a Core.Flow.flow
include module type of struct include Core.Marker end
type marker = Core.Marker.marker = ..
type marker_info = Core.Marker.marker_info = {
marker_name : string;
marker_print_name : (marker -> string) -> marker -> string;
marker_print : (Format.formatter -> marker -> unit) -> Format.formatter -> marker -> unit;
marker_compare : (marker -> marker -> int) -> marker -> marker -> int;
}
val pp_marker : Format.formatter -> marker -> unit
val get_marker_name : marker -> string
val register_marker : marker_info -> unit
val mk_add_marker :
marker ->
Mopsa_utils.Core.Location.range ->
Framework.Core.Ast.Stmt.stmt
val is_marker_enabled : marker -> bool
module Var = Framework.Core.All.Var
module Core = Framework.Core
module Sig = Framework.Sig
module Params = Framework.Params
module Paths = Params.Paths
module Visitor = Core.Ast.Visitor
include module type of struct include Mopsa_utils.Core.Location end
Positions
=============
Position in a file.
val get_pos_file : pos -> string
val get_pos_line : pos -> int
val get_pos_column : pos -> int
val mk_pos : string -> int -> int -> pos
Return the relative path of `file` w.r.t. the current working directory
Extended source locations, decorated with a stack of positions. It can be used to distinguish between different use of the same lexical token. E.g., in C, it tracks macro argument expansion.
Ranges
==========
type range = Mopsa_utils.Core.Location.range =
Location range of AST nodes.
Range tags can be used to annotate AST nodes added by the abstract domains that are not textually present in the source files.
val mk_string_tag : ('a, Format.formatter, unit, range_tag) format4 -> 'a
val tag_range : range -> ('a, Format.formatter, unit, range) format4 -> 'a
Tag a range with a (formatted) annotation.
val fresh_range_counter : int ref
val mk_fresh_range : unit -> range
val mk_program_range : string list -> range
val get_range_file : range -> string
val get_range_relative_file : range -> string
val get_range_line : range -> int
val get_range_column : range -> int
val is_orig_range : range -> bool
val is_program_range : range -> bool
val match_range_file : string -> range -> bool
val match_range_line : int -> range -> bool
val from_lexing_pos : Lexing.position -> pos
val from_lexing_range : Lexing.position -> Lexing.position -> range
Range annotations
=====================
val with_range : 'a -> range -> 'a with_range
val get_content : 'a with_range -> 'a
val get_range : 'a with_range -> range
val bind_range : 'a with_range -> ?range:range -> ('a -> 'b) -> 'b with_range
val bind_pair_range : 'a with_range -> ('a -> 'b * 'c) -> 'b with_range * 'c
val compare_with_range :
('a -> 'b -> int) ->
'a with_range ->
'b with_range ->
int
Pretty printers
===================
val pp_position : Format.formatter -> pos -> unit
val pp_relative_position : Format.formatter -> pos -> unit
val pp_position_stack :
(Format.formatter -> 'a -> unit) ->
Format.formatter ->
'a list ->
unit
val pp_eposition : Format.formatter -> epos -> unit
val pp_relative_eposition : Format.formatter -> epos -> unit
val pp_range : Format.formatter -> range -> unit
val pp_relative_range : Format.formatter -> range -> unit
include module type of struct include Mopsa_utils.Core.Callstack end
Call sites
**************
type callsite = Mopsa_utils.Core.Callstack.callsite = {
call_fun_orig_name : string;
(*Original name of the called function
*)call_fun_uniq_name : string;
(*Unique name of the called function
*)call_range : Mopsa_utils.Core.Location.range;
(*Call location
*)
}
Call site is the location of a call in the program
val pp_callsite : Format.formatter -> callsite -> unit
Print a call site
type callstack = callsite list
val pp_callstack : Format.formatter -> callstack -> unit
Print a call stack
val pp_callstack_short : Format.formatter -> callstack -> unit
Print a call stack in a short style
val empty_callstack : callstack
Empty call stack
val is_empty_callstack : callstack -> bool
Check that a call stack is empty
val callstack_length : callstack -> int
Return the length of a call stack
val push_callstack :
string ->
?uniq:string ->
Mopsa_utils.Core.Location.range ->
callstack ->
callstack
push_callstack orig ~uniq range cs
adds the call to function orig
at location range
at the top of the call stack cs
. The default unique function name of the function is its original name.
pop_callstack cc
returns the last call site in cc
and the remaining callstack Raises Empty_callstack
if the call stack is empty.
callstack_top cs
returns the last call site in cs
. Raises Empty_callstack
if the call stack is empty.
include module type of struct include Params.Options end
Registration
****************
val register_builtin_option : Mopsa_utils.Core.ArgExt.arg -> unit
Register a built-in option
val register_language_option : string -> Mopsa_utils.Core.ArgExt.arg -> unit
Register a language option.
val register_domain_option : string -> Mopsa_utils.Core.ArgExt.arg -> unit
Register a domain option.
Register a shared option
Import a shared option into a domain
Filters
***********
val get_options : unit -> Mopsa_utils.Core.ArgExt.arg list
Return the list of options
val get_builtin_options : unit -> Mopsa_utils.Core.ArgExt.arg list
Return the list of built-in options
val get_language_options : string -> Mopsa_utils.Core.ArgExt.arg list
Return the list of options of a language
val get_domain_options : string -> Mopsa_utils.Core.ArgExt.arg list
Return the list of options of a domain
include module type of struct include Mopsa_utils.Core.Exceptions end
Warnings
=-=-=-=-=-=-
val warn : ('a, Format.formatter, unit, unit) format4 -> 'a
val warn_at :
Mopsa_utils.Core.Location.range ->
('a, Format.formatter, unit, unit) format4 ->
'a
Panic exceptions
=-=-=-=-=-=-=-=-=-=-
val pp : ('a, Format.formatter, unit, unit) format4 -> 'a
val pp_at :
Mopsa_utils.Core.Location.range ->
('a, Format.formatter, unit, unit) format4 ->
'a
exception PanicAtLocation of Mopsa_utils.Core.Location.range * string * string
OCaml line of code
OCaml line of code
exception PanicAtFrame of Mopsa_utils.Core.Location.range
* Mopsa_utils.Core.ControlCtx.control_ctx
* string
* string
OCaml line of code
OCaml line of code
val panic : ?loc:string -> ('a, Format.formatter, unit, 'b) format4 -> 'a
Raise a panic exception using a formatted string
val panic_at :
?loc:string ->
Mopsa_utils.Core.Location.range ->
('a, Format.formatter, unit, 'b) format4 ->
'a
val panic_at_frame :
?loc:string ->
Mopsa_utils.Core.Location.range ->
Mopsa_utils.Core.ControlCtx.control_ctx ->
('a, Format.formatter, unit, 'b) format4 ->
'a
Syntax-related exceptions
=-=-=-=-=-=-=-=-=-=-=-=-=-=-
exception SyntaxError of Mopsa_utils.Core.Location.range * string
exception SyntaxErrorList of (Mopsa_utils.Core.Location.range * string) list
exception UnnamedSyntaxError of Mopsa_utils.Core.Location.range
exception UnnamedSyntaxErrorList of Mopsa_utils.Core.Location.range list
val syntax_error :
Mopsa_utils.Core.Location.range ->
('a, Format.formatter, unit, 'b) format4 ->
'a
val syntax_errors : (Mopsa_utils.Core.Location.range * string) list -> 'a
val unnamed_syntax_error : Mopsa_utils.Core.Location.range -> 'a
val unnamed_syntax_errors : Mopsa_utils.Core.Location.range list -> 'a
include module type of struct include Framework.Toplevel end
module type TOPLEVEL = Framework.Toplevel.TOPLEVEL
Signature of the toplevel abstraction
Domain encapsulation into an abstraction
val debug : ('a, Format.formatter, unit, unit) format4 -> 'a
module Make = Framework.Toplevel.Make
Encapsulate a domain into a top-level abstraction