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

val compare_constant : constant -> constant -> int

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

type constant +=

| C_top of Framework.Core.Ast.Typ.typ
| C_bool of bool

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

val compare_expr : expr -> expr -> int

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 ekind : expr -> expr_kind

Get the kind of an expression

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 ehistory : expr -> expr list

Get the evaluation history 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

val get_expr_history : expr -> expr list

Get the evaluation history of an expression

val get_orig_expr : expr -> expr

Get the original form of an expression

val find_expr_ancestor : (expr -> bool) -> expr -> expr

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 weaken_var_expr : expr -> expr

Change the access mode of a variable expression to WEAK

val strongify_var_expr : expr -> expr

Change the access mode of a variable expression to STRONG

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

val weaken_addr_expr : expr -> expr

Change the access mode of an address expression to WEAK

val strongify_addr_expr : expr -> expr

Change the access mode of an address expression to STRONG

Constant expressions

type expr_kind +=

| E_constant of Core.Ast.Constant.constant

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

type expr_kind +=

| E_unop of Framework.Core.Ast.Operator.operator * expr
(*
operand
*)

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

type expr_kind +=

| E_binop of Framework.Core.Ast.Operator.operator * expr * expr
(*
second operand
*)

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

val negate_expr : ?esynthetic:bool -> expr -> expr

Return the negation of an 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 skind : stmt -> stmt_kind

Get the kind of 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 compare_stmt : stmt -> stmt -> int

Total order between statements

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

val register_stmt_pp : stmt Mopsa_utils.Core.TypeExt.print -> unit

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

type stmt_kind +=

| S_assign of Framework.Core.Ast.Expr.expr * Framework.Core.Ast.Expr.expr
(*
rhs
*)

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;

type stmt_kind +=

| S_assume of Framework.Core.Ast.Expr.expr
(*
condition
*)

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 compare_typ : typ -> typ -> int

Compare two types

val pp_typ : Format.formatter -> typ -> unit

Pretty-print a type

Registration

val register_typ : typ Mopsa_utils.Core.TypeExt.info -> unit

val register_typ_compare : typ Mopsa_utils.Core.TypeExt.compare -> unit

val register_typ_pp : typ Mopsa_utils.Core.TypeExt.print -> unit

Common types

type typ +=

| T_any
(*
Generic unknown type
*)
| T_addr
(*
Heap addresses type
*)
| T_bool
(*
Boolean type
*)

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 compare_program : program -> program -> int

Total order between 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

val register_program_pp : program Mopsa_utils.Core.TypeExt.print -> unit

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

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 compare_operator : operator -> operator -> int

Total order between 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

val register_operator_pp : operator Mopsa_utils.Core.TypeExt.print -> unit

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

val negate_comparison_op : operator -> operator

Return the negation of a comparison operator

val negate_logic_op : operator -> operator

Return the negation of a logical operator

include module type of struct include Framework.Core.Ast.Var end

val print_uniq_with_uid : bool ref

val force_print_uniq_with_uid : bool -> (unit -> 'a) -> 'a

Access modes

type var_kind = Framework.Core.Ast.Var.var_kind = ..

Extensible kind of variables

type mode = Framework.Core.Ast.Var.mode =

| WEAK
(*
Weak updates are used when the variable summarizes several concrete dimensions
*)
| STRONG
(*
Strong updates are used when the variable represents a single concrete dimension
*)

Access mode of a variable

val pp_mode : Format.formatter -> mode -> unit

Pretty-print an access mode

val compare_mode : mode -> mode -> int

Compare two access modes

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 vkind : var -> var_kind

val vtyp : var -> Framework.Core.Ast.Typ.typ

val vmode : var -> mode

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

val compare_var : var -> var -> int

Total order between variables

Registration

val register_var : var Mopsa_utils.Core.TypeExt.info -> unit

val register_var_compare : var Mopsa_utils.Core.TypeExt.compare -> unit

val register_var_pp : var Mopsa_utils.Core.TypeExt.print -> unit

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 start_vcounter_at : int -> unit

val get_vcounter_val : unit -> int

val get_orig_vname : var -> string

val set_orig_vname : string -> var -> var

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_compare_chain : (addr_kind -> addr_kind -> int) ref

val addr_kind_pp_chain : (Format.formatter -> addr_kind -> unit) ref

val pp_addr_kind : Format.formatter -> addr_kind -> unit

val compare_addr_kind : addr_kind -> addr_kind -> int

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

type addr_partitioning +=

| G_all
(*
Group all addresses into one
*)

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 akind : addr -> addr_kind

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 compare_addr : addr -> addr -> int

val addr_mode : 
  addr ->
  Framework.Core.Ast.Var.mode option ->
  Framework.Core.Ast.Var.mode

type Framework.Core.Ast.Var.var_kind +=

| V_addr_attr of addr * string

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

type 'a structure = parts * (parts -> 'a)

builder function

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

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

val register_stmt_with_visitor : 
  Framework.Core.Ast.Stmt.stmt visit_info ->
  unit

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

Visiting iterators

type 'a visit_action = 'a Core.Ast.Visitor.visit_action =

| Keep of 'a
(*
Keep the given result
*)
| VisitParts of 'a
(*
Continue visiting the parts of the given result
*)
| Visit of 'a
(*
Iterate the visitor on the given result
*)

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

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_kind +=

| A_generic of check

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 check_of_alarm : alarm -> check

Return the check associate to 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 compare_alarm : alarm -> alarm -> int

Compare two alarms

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

val register_alarm_pp : 
  ((Format.formatter -> alarm_kind -> unit) ->
    Format.formatter ->
    alarm_kind ->
    unit) ->
  unit

val register_alarm_check : 
  ((alarm_kind -> check) -> alarm_kind -> check) ->
  unit

val register_alarm_join : 
  ((alarm_kind -> alarm_kind -> alarm_kind option) ->
    alarm_kind ->
    alarm_kind ->
    alarm_kind option) ->
  unit

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

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 =

| Warning
(*
Some executions may have issues
*)
| Safe
(*
All executions are safe
*)
| Error
(*
All executions do have issues
*)
| Unreachable
(*
No execution reaches the check point
*)

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

type assumption_kind +=

| A_ignore_unsupported_stmt of Framework.Core.Ast.Stmt.stmt

Generic assumptions for specifying potential unsoundness due to unsupported statements/expressions

type assumption_kind +=

| A_ignore_unsupported_expr of Framework.Core.Ast.Expr.expr

type assumption_kind +=

| A_prototype_domain of string

type assumption_kind +=

| A_no_guaranteed_termination_domain of string

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

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

val subset_report : report -> report -> bool

subset_report r1 r2 checks whether report r1 is included in r2

val join_report : report -> report -> report

Compute the union of two reports

val meet_report : report -> report -> report

Compute the intersection of two reports

val filter_report : (diagnostic -> bool) -> report -> report

filter_report p r keeps only diagnostics in report r that verify predicate p

val singleton_report : alarm -> report

Create a report with a single true alarm

val add_alarm : ?warning:bool -> alarm -> report -> report

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

val alarms_to_report : alarm list -> report

val report_to_alarms : report -> alarm list

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

val singleton_ctx : ('a, 'v) ctx_key -> 'v -> 'a ctx

Context with one element

val mem_ctx : ('a, 'v) ctx_key -> 'a ctx -> bool

mem_ctx k ctx returns true when an element at key k is in the context ctx.

val find_ctx : ('a, 'v) ctx_key -> 'a ctx -> 'v

find_ctx k ctx returns the element at key k in the context ctx. Raises Not_found if no element is found.

val find_ctx_opt : ('a, 'v) ctx_key -> 'a ctx -> 'v option

find_ctx k ctx returns the element of the key k in the context ctx. Returns None if no element is found.

val add_ctx : ('a, 'v) ctx_key -> 'v -> 'a ctx -> 'a ctx

add_ctx k v ctx add element v at key k in the context ctx. The previous element is overwritten if present.

val remove_ctx : ('a, 'v) ctx_key -> 'a ctx -> 'a ctx

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 most_recent_ctx : 'a ctx -> 'a ctx -> 'a ctx

Get the most recent context between two

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

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 compare_accessor : accessor -> accessor -> int

val pp_accessor : Format.formatter -> accessor -> unit

val register_accessor : accessor Mopsa_utils.Core.TypeExt.info -> unit

val compare_path : accessor list -> accessor list -> int

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 =

| Change_empty
| Change_block of Framework.Core.Ast.Stmt.stmt list
| Change_seq of change list
| Change_join of change * change
| Change_meet of change * change

val pp_change : Format.formatter -> change -> unit

val compare_change : change -> change -> int

val empty_change : change

val is_empty_change : change -> bool

val join_change : change -> change -> change

val meet_change : change -> change -> change

val add_stmt_to_change : Framework.Core.Ast.Stmt.stmt -> change -> change

Join two changes

val concat_change : change -> change -> change

Meet 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

val enable_change_tracker : unit -> unit

val disable_change_tracker : unit -> unit

val is_change_tracker_enabled : unit -> bool

val set_change_tracker_state : bool -> unit

val with_change_tracker : (unit -> 'a) -> 'a

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

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

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

type token +=

| T_cur
(*
Token of current (active) execution flow
*)

val register_token : token Mopsa_utils.Core.TypeExt.info -> unit

val compare_token : token -> token -> int

Compare two tokens with a total order

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

type semantic = string

val compare_semantic : semantic -> semantic -> int

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 domain = string

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 compare_route : route -> route -> int

Set of domains

Compare two routes

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

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 executes stmt in flow 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 evaluates expr in flow 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 result e' of man.eval expr flow is a simplification of e 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 of e in semantic. A common use case is to translate expressions to Universal with man.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

type symbols = Framework.Core.Print.symbols = {

sopen : string;
ssep : string;
sbind : string;
sclose : string;

}

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

type Core.Ast.Constant.constant +=

| C_avalue : 'v avalue_kind * 'v -> Core.Ast.Constant.constant

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 compare_marker : marker -> marker -> int

val pp_marker : Format.formatter -> marker -> unit

val get_marker_name : marker -> string

val register_marker : marker_info -> unit

type Framework.Core.Ast.Stmt.stmt_kind +=

| S_add_marker of marker

val mk_add_marker : 
  marker ->
  Mopsa_utils.Core.Location.range ->
  Framework.Core.Ast.Stmt.stmt

val enable_marker : string -> unit

val disable_marker : string -> unit

val is_marker_enabled : marker -> bool

val available_markers : unit -> string list

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

=============

type pos = Mopsa_utils.Core.Location.pos = {

pos_file : string;
(*
File name.
*)
pos_line : int;
(*
Line number.
*)
pos_column : int;
(*
Column number.
*)

}

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

val compare_pos : pos -> pos -> int

Comparison function of positions.

val relative_path : string -> string

Return the relative path of `file` w.r.t. the current working directory

type epos = Mopsa_utils.Core.Location.epos = {

epos_pos : pos;
epos_stack : pos list;

}

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 =

| R_program of string list
(*
list of source files
*)
| R_orig of pos * pos
(*
end position
*)
| R_ext_orig of epos * epos
(*
end position
*)
| R_fresh of int
(*
non-original fresh range with unique id
*)
| R_tagged of range_tag * range
(*
Tagged range with an annotation
*)

Location range of AST nodes.

and range_tag = Mopsa_utils.Core.Location.range_tag =

| String_tag of string
| Range_tag of range

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_tagged_range : range_tag -> range -> range

val mk_string_tag : ('a, Format.formatter, unit, range_tag) format4 -> 'a

val mk_range_tag : range -> range_tag

val mk_range_tagged_range : range -> range -> range

val tag_range : range -> ('a, Format.formatter, unit, range) format4 -> 'a

Tag a range with a (formatted) annotation.

val mk_orig_range : pos -> pos -> range

val mk_ext_orig_range : epos -> epos -> range

val fresh_range_counter : int ref

val mk_fresh_range : unit -> range

val mk_program_range : string list -> range

val untag_range : range -> range

val map_tag : (range -> range) -> range -> range

val remove_ext : range -> range

val get_range_start : range -> pos

val get_range_end : range -> pos

val set_range_start : range -> pos -> range

val set_range_end : range -> pos -> 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

val compare_range : range -> range -> int

Comparison function of ranges.

val compare_range_tag : range_tag -> range_tag -> int

val subset_range : range -> range -> bool

Range annotations

=====================

type 'a with_range = 'a Mopsa_utils.Core.Location.with_range = {

content : 'a;
range : range;

}

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

val compare_callsite : callsite -> callsite -> int

Compare two call sites

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 compare_callstack : callstack -> callstack -> int

Compare two call stacks

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.

exception Empty_callstack

Exception raised when a call stack is empty

val pop_callstack : callstack -> callsite * callstack

pop_callstack cc returns the last call site in cc and the remaining callstack Raises Empty_callstack if the call stack is empty.

val callstack_top : callstack -> callsite

callstack_top cs returns the last call site in cs. Raises Empty_callstack if the call stack is empty.

val callstack_begins_with : callstack -> callstack -> bool

callstack_begins_with ext cs checks that ext is an extension of cs, i.e. ext = x @ cs

include module type of struct include Params.Options end

Registration

****************

val register_builtin_option : Mopsa_utils.Core.ArgExt.arg -> unit

val register_language_option : string -> Mopsa_utils.Core.ArgExt.arg -> unit

val register_domain_option : string -> Mopsa_utils.Core.ArgExt.arg -> unit

val register_shared_option : string -> Mopsa_utils.Core.ArgExt.arg -> unit

val import_shared_option : string -> string -> unit

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

val help : unit -> unit

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 Panic of string * string

OCaml line of code

exception PanicAtLocation of Mopsa_utils.Core.Location.range * string * string

OCaml line of code

exception PanicAtFrame of Mopsa_utils.Core.Location.range
  * Mopsa_utils.Core.ControlCtx.control_ctx
  * string
  * string

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

=-=-=-=-=-=-=-=-=-=-=-=-=-=-

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

Sourcetype 'a info = 'a Mopsa_utils.Core.TypeExt.info

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

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/MopsaLib/index.html

Module Mopsa_analyzer.MopsaLibSource

Registration

Common constants

Registration

Some common expressions

Variable expressions

Heap addresses expressions

Constant expressions

Unary expressions

Binary expressions

Expressions containers

Registration

Blocks

Common statements

Containers of statements

Registration

Common types

Registration

Registration

Some common operators

Access modes

Variables

Registration

Common variables

Containers for variables

Deprecated

Registration

Visiting iterators

Utility functions

Deprecated

Checks

Alarms

Diagnostic

Soundness assumption

Analysis report

Generic merge

Registration

Common queries

Managers

Print objects

Printers

Print paths

Generic print functions

Typed print functions

Format

JSON

Positions

Ranges

Range annotations

Pretty printers

Call sites

Registration

Filters

Warnings

Panic exceptions

Syntax-related exceptions

Domain encapsulation into an abstraction

dune-project
Dependency

Module `Mopsa_analyzer.MopsaLib`Source