package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

Essential modules.

include module type of struct include Mopsa_utils end
module Bot = Mopsa_utils.Bot
module Compare = Mopsa_utils.Compare
module Location = Mopsa_utils.Location
module Callstack = Mopsa_utils.Callstack
module Debug = Mopsa_utils.Debug
module Exceptions = Mopsa_utils.Exceptions
module OptionExt = Mopsa_utils.OptionExt
module Dnf = Mopsa_utils.Dnf
module SetExtPoly = Mopsa_utils.SetExtPoly
module SetExt = Mopsa_utils.SetExt
module SetExtSig = Mopsa_utils.SetExtSig
module SetP = Mopsa_utils.SetP
module ListExt = Mopsa_utils.ListExt
module MapExtPoly = Mopsa_utils.MapExtPoly
module MapExt = Mopsa_utils.MapExt
module MapExtSig = Mopsa_utils.MapExtSig
module InvRelation = Mopsa_utils.InvRelation
module InvRelationSig = Mopsa_utils.InvRelationSig
module Equiv = Mopsa_utils.Equiv
module MapP = Mopsa_utils.MapP
module Relation = Mopsa_utils.Relation
module RelationSig = Mopsa_utils.RelationSig
module ValueSig = Mopsa_utils.ValueSig
module Timing = Mopsa_utils.Timing
module Top = Mopsa_utils.Top
module Bot_top = Mopsa_utils.Bot_top
module ItvUtils = Mopsa_utils.ItvUtils
module CongUtils = Mopsa_utils.CongUtils
module Bitfields = Mopsa_utils.Bitfields
module GraphSig = Mopsa_utils.GraphSig
module Graph = Mopsa_utils.Graph
module ArgExt = Mopsa_utils.ArgExt
module LineEdit = Mopsa_utils.LineEdit
module TypeExt = Mopsa_utils.TypeExt
module Eq = Mopsa_utils.Eq
module Version = Mopsa_utils.Version
include module type of struct include Framework.Core.All end
include module type of struct include Ast.Semantic end
include module type of struct include Ast.Constant end
type constant = 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 : Stdlib.Format.formatter -> constant -> unit

pp_constant fmt c pretty-prints a registered constant c with formatter fmt

Registration

val register_constant : constant Mopsa_utils.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.TypeExt.compare -> unit

register_constant_compare compare registers a new comparison function for constants

val register_constant_pp : constant Mopsa_utils.TypeExt.print -> unit

register_constant_compare compare registers a new pretty-printer for constants

Common constants

type constant +=
  1. | C_top of Ast.Typ.typ
include module type of struct include Ast.Expr end
type expr_kind = Ast.Expr.expr_kind = ..

Extensible type of expression kinds

type expr = Ast.Expr.expr = {
  1. ekind : expr_kind;
    (*

    kind of the expression

    *)
  2. etyp : Ast.Typ.typ;
    (*

    type of the expression

    *)
  3. erange : Mopsa_utils.Location.range;
    (*

    location range of the expression

    *)
  4. etrans : expr Ast.Semantic.SemanticMap.t;
    (*

    translations of the expression into other semantics

    *)
  5. ehistory : expr list;
    (*

    History of preceding evaluations of the expression

    *)
}

Expressions

val compare_expr : expr -> expr -> int

compare_expr e1 e2 implements a total order between expressions

val pp_expr : Stdlib.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 -> Ast.Typ.typ

Get the type of an expression

Get the location of an expression

Get the translation map of an expression

val ehistory : expr -> expr list

Get the evaluation history of an expression

val mk_expr : ?etyp:Ast.Typ.typ -> ?etrans:expr Ast.Semantic.SemanticMap.t -> ?ehistory:expr list -> expr_kind -> Mopsa_utils.Location.range -> expr

Construct an expression

val add_expr_translation : Ast.Semantic.semantic -> expr -> expr -> expr

Add a translation of an expression

val get_expr_translations : expr -> expr Ast.Semantic.SemanticMap.t

Get all translations of an expression

val get_expr_translation : 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.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.TypeExt.compare -> unit

register_expr_compare compare registers a new expression comparison

val register_expr_pp : expr Mopsa_utils.TypeExt.print -> unit

register_expr_compare compare registers a new expression printer

Some common expressions

Variable expressions

type expr_kind +=
  1. | E_var of Ast.Var.var * Ast.Var.mode option
    (*

    optional access mode overloading the variable's access mode

    *)

Variables

val mk_var : Ast.Var.var -> ?mode:Ast.Var.mode option -> Mopsa_utils.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 : Ast.Var.var -> Ast.Var.mode option -> Ast.Var.mode

Get the overloaded access mode of a variable

Heap addresses expressions

type expr_kind +=
  1. | E_addr of Ast.Addr.addr * Ast.Var.mode option
    (*

    optional access mode overloading the address access mode

    *)
  2. | E_alloc_addr of Ast.Addr.addr_kind * Ast.Var.mode

Heap addresses

val mk_addr : Ast.Addr.addr -> ?etyp:Ast.Typ.typ -> ?mode:Ast.Var.mode option -> Mopsa_utils.Location.range -> expr

Create an address expression

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 +=
  1. | E_constant of Ast.Constant.constant

Constants

Create a constant expression

Create ⊤ expression of a given type

Unary expressions

type expr_kind +=
  1. | E_unop of Ast.Operator.operator * expr
    (*

    operand

    *)

Unary operator expressions

Create a unary operator expression

mk_not e range returns the negation of expression e using the operator Operator.O_log_not

Binary expressions

type expr_kind +=
  1. | E_binop of Ast.Operator.operator * expr * expr
    (*

    second operand

    *)

Binary operator expressions

Create a binary operator expression

val negate_expr : expr -> expr

Return the negation of an expression

Expressions containers

Sets of expression

Maps of expressions

include module type of struct include Ast.Stmt end
type stmt_kind = Ast.Stmt.stmt_kind = ..

Extensible kinds of statements

type stmt = Ast.Stmt.stmt = {
  1. skind : stmt_kind;
    (*

    kind of the statement

    *)
  2. srange : Mopsa_utils.Location.range;
    (*

    location range of the statement

    *)
}

Statements

Create a statement

val skind : stmt -> stmt_kind

Get the kind of a statement

Get the location range of a statement

val compare_stmt : stmt -> stmt -> int

Total order between statements

val pp_stmt : Stdlib.Format.formatter -> stmt -> unit

Pretty-printer of statements

Registration

val register_stmt : stmt Mopsa_utils.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.TypeExt.compare -> unit

Register a comparison function for statements

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

Register a pretty-printer function for statements

Blocks

type block = stmt list

Blocks are sequences of statements

val pp_block : Stdlib.Format.formatter -> block -> unit

Pretty-printer for blocks

Common statements

type stmt_kind +=
  1. | S_program of Ast.Program.program * string list option
    (*

    Command-line arguments as given to Mopsa after --

    *)

Programs

type stmt_kind +=
  1. | S_assign of Ast.Expr.expr * Ast.Expr.expr
    (*

    rhs

    *)

Assignments

mk_assign lhs rhs range creates the assignment lhs = rhs;

type stmt_kind +=
  1. | S_assume of Ast.Expr.expr
    (*

    condition

    *)

Tests

Create a test statement

type stmt_kind +=
  1. | S_add of Ast.Expr.expr
    (*

    Add a dimension to the environment

    *)
  2. | S_remove of Ast.Expr.expr
    (*

    Remove a dimension from the environment and invalidate all references to it

    *)
  3. | S_invalidate of Ast.Expr.expr
    (*

    Invalidate all references to a dimension without removing it

    *)
  4. | S_rename of Ast.Expr.expr * Ast.Expr.expr
    (*

    new

    *)
  5. | S_forget of Ast.Expr.expr
    (*

    Forget a dimension by putting ⊤ (all possible values) in it. Note that the dimension is not removed

    *)
  6. | S_project of Ast.Expr.expr list
    (*

    Project the environment on the given list of dimensions. All other dimensions are removed

    *)
  7. | S_expand of Ast.Expr.expr * Ast.Expr.expr list
    (*

    Expand a dimension into a list of other dimensions. The expanded dimension is untouched

    *)
  8. | S_fold of Ast.Expr.expr * Ast.Expr.expr list
    (*

    Fold a list of dimensions into a single one. The folded dimensions are removed

    *)
  9. | S_block of stmt list * Ast.Var.var list
    (*

    local variables declared within the block

    *)
  10. | S_breakpoint of string
    (*

    Trigger a breakpoint

    *)

Dimensions

Utility functions to create various statements for dimension management

val mk_remove_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt
val mk_invalidate_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt
val mk_project : Ast.Expr.expr list -> Mopsa_utils.Location.range -> stmt
val mk_project_vars : Ast.Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_forget_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt
val mk_expand_var : Ast.Var.var -> Ast.Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_fold_var : Ast.Var.var -> Ast.Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_breakpoint : string -> Mopsa_utils.Location.range -> stmt

Containers of statements

Sets of statements

Maps of statements

include module type of struct include Ast.Typ end
type typ = Ast.Typ.typ = ..

Extensible types

val compare_typ : typ -> typ -> int

Compare two types

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

Pretty-print a type

Registration

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

Register a new type

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

Register a new type comparison

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

Register a new type pretty-printer

Common types

type typ +=
  1. | T_any
    (*

    Generic unknown type

    *)
  2. | T_addr
    (*

    Heap addresses type

    *)
include module type of struct include Ast.Program end
type prog_kind = Ast.Program.prog_kind = ..

Extensible type of program kinds

type program = Ast.Program.program = {
  1. prog_kind : prog_kind;
    (*

    kind of the program

    *)
  2. prog_range : Mopsa_utils.Location.range;
    (*

    program location

    *)
}

Programs

val compare_program : program -> program -> int

Total order between programs

val pp_program : Stdlib.Format.formatter -> program -> unit

Pretty-printer for programs

Registration

val register_program : program Mopsa_utils.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.TypeExt.compare -> unit

Register a comparison function between programs

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

Register a pretty-printer for programs

include module type of struct include Ast.Frontend end
type frontend = Ast.Frontend.frontend = {
  1. lang : string;
    (*

    Language of the frontend

    *)
  2. parse : string list -> Ast.Program.program;
    (*

    Parser function that translates a list of input source files into a Mopsa Program.program

    *)
}

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 Ast.Operator end
type operator = Ast.Operator.operator = ..

Extensible type of operators

val compare_operator : operator -> operator -> int

Total order between operators

val pp_operator : Stdlib.Format.formatter -> operator -> unit

Pretty-printer of operators

Registration

val register_operator : operator Mopsa_utils.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.TypeExt.compare -> unit

Register a comparison function for operators

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

Register a pretty-printer for operators

Some common operators

type operator +=
  1. | O_eq
    (*

    equality ==

    *)
  2. | O_ne
    (*

    inequality !=

    *)
  3. | O_lt
    (*

    less than <

    *)
  4. | O_le
    (*

    less or equal <=

    *)
  5. | O_gt
    (*

    greater than >

    *)
  6. | O_ge
    (*

    greater or equal >=

    *)
  7. | O_log_not
    (*

    logical negation

    *)
  8. | O_log_or
    (*

    logical disjunction ||

    *)
  9. | O_log_and
    (*

    logical conjunction &&

    *)
  10. | O_log_xor
    (*

    logical strict disjonction xor

    *)
  11. | 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 Ast.Var end
val print_uniq_with_uid : bool Stdlib.ref

Access modes

type var_kind = Ast.Var.var_kind = ..

Extensible kind of variables

type mode = Ast.Var.mode =
  1. | WEAK
    (*

    Weak updates are used when the variable summarizes several concrete dimensions

    *)
  2. | STRONG
    (*

    Strong updates are used when the variable represents a single concrete dimension

    *)

Access mode of a variable

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

Pretty-print an access mode

val compare_mode : mode -> mode -> int

Compare two access modes

Variables

type var = Ast.Var.var = {
  1. vname : string;
    (*

    unique name of the variable

    *)
  2. vkind : var_kind;
    (*

    kind the variable

    *)
  3. vtyp : Ast.Typ.typ;
    (*

    type of the variable

    *)
  4. vmode : mode;
    (*

    access mode of the variable

    *)
  5. vsemantic : 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 -> Ast.Typ.typ
val vmode : var -> mode
val vsemantic : var -> Ast.Semantic.semantic
val mkv : string -> var_kind -> ?mode:mode -> ?semantic:Ast.Semantic.semantic -> 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 : Stdlib.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.TypeExt.info -> unit

Register a new kind of variables

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

Register a new variable comparison

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

Register a new variable pretty-printer

Common variables

type var_kind +=
  1. | V_uniq of string * int
    (*

    Unique ID

    *)
  2. | V_tmp of int
    (*

    Unique ID

    *)
  3. | V_var_attr of var * string
    (*

    Attribute

    *)
  4. | V_range_attr of Mopsa_utils.Location.range * string
    (*

    Attribute

    *)
val mk_uniq_var : string -> int -> ?mode:mode -> Ast.Typ.typ -> var

Create a unique variable

val mk_fresh_uniq_var : string -> ?mode:mode -> Ast.Typ.typ -> unit -> var

Create a fresh variable with a fresh ID

val mktmp : ?typ:Ast.Typ.typ -> ?mode:mode -> unit -> var

Create a fresh temporary variable

val mk_attr_var : var -> string -> ?mode:mode -> ?semantic:Ast.Semantic.semantic -> 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.Location.range -> string -> ?mode:mode -> ?semantic:Ast.Semantic.semantic -> 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

Sets of variables

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 Ast.Addr end
type addr_kind = Ast.Addr.addr_kind = ..

Kind of heap addresses, used to store extra information.

val addr_kind_compare_chain : (addr_kind -> addr_kind -> int) Stdlib.ref
val addr_kind_pp_chain : (Stdlib.Format.formatter -> addr_kind -> unit) Stdlib.ref
val pp_addr_kind : Stdlib.Format.formatter -> addr_kind -> unit
val compare_addr_kind : addr_kind -> addr_kind -> int
val register_addr_kind : addr_kind Mopsa_utils.TypeExt.info -> unit
type addr_partitioning = Ast.Addr.addr_partitioning = ..

Addresses are grouped by static criteria to make them finite

type addr_partitioning +=
  1. | G_all
    (*

    Group all addresses into one

    *)
val addr_partitioning_compare_chain : (addr_partitioning -> addr_partitioning -> int) Stdlib.ref
val addr_partitioning_pp_chain : (Stdlib.Format.formatter -> addr_partitioning -> unit) Stdlib.ref
val opt_hash_addr : bool Stdlib.ref

Command line option to use hashes as address format

val pp_addr_partitioning_hash : Stdlib.Format.formatter -> addr_partitioning -> unit
val pp_addr_partitioning : ?full:bool -> Stdlib.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 : Stdlib.Format.formatter -> addr_partitioning -> unit
val compare_addr_partitioning : addr_partitioning -> addr_partitioning -> int
val register_addr_partitioning : addr_partitioning Mopsa_utils.TypeExt.info -> unit
type addr = Ast.Addr.addr = {
  1. addr_kind : addr_kind;
    (*

    Kind of the address.

    *)
  2. addr_partitioning : addr_partitioning;
    (*

    Partitioning policy of the address

    *)
  3. addr_mode : Ast.Var.mode;
    (*

    Assignment mode of address (string or weak)

    *)
}

Heap addresses.

val akind : addr -> addr_kind
val pp_addr : Stdlib.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 -> Ast.Var.mode option -> Ast.Var.mode
type Ast.Var.var_kind +=
  1. | V_addr_attr of addr * string

Address variables

val mk_addr_attr : addr -> string -> Ast.Typ.typ -> Ast.Var.var
include module type of struct include Ast.Visitor end
type parts = Ast.Visitor.parts = {
  1. exprs : Ast.Expr.expr list;
    (*

    sub-expressions

    *)
  2. stmts : Ast.Stmt.stmt list;
    (*

    sub-statements

    *)
}

Parts of a statement/expression

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

builder function

val structure_of_expr : Ast.Expr.expr -> Ast.Expr.expr structure

Get the structure of an expression

val structure_of_stmt : Ast.Stmt.stmt -> 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 Ast.Visitor.visit_info = {
  1. compare : 'a Mopsa_utils.TypeExt.compare;
    (*

    Comparison function for 'a

    *)
  2. print : 'a Mopsa_utils.TypeExt.print;
    (*

    Pretty-printer for 'a'

    *)
  3. visit : ('a -> 'a structure) -> 'a -> 'a structure;
    (*

    Visitor for 'a

    *)
}

Registration descriptor for visitors

val register_expr_with_visitor : Ast.Expr.expr visit_info -> unit

Register an expression with its visitor

val register_expr_visitor : ((Ast.Expr.expr -> Ast.Expr.expr structure) -> Ast.Expr.expr -> Ast.Expr.expr structure) -> unit

Register a visitor of an expression

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

Register a statement with its visitor

val register_stmt_visitor : ((Ast.Stmt.stmt -> Ast.Stmt.stmt structure) -> Ast.Stmt.stmt -> Ast.Stmt.stmt structure) -> unit

Register a visitor of a statement

Visiting iterators

type 'a visit_action = 'a Ast.Visitor.visit_action =
  1. | Keep of 'a
    (*

    Keep the given result

    *)
  2. | VisitParts of 'a
    (*

    Continue visiting the parts of the given result

    *)
  3. | Visit of 'a
    (*

    Iterate the visitor on the given result

    *)

Actions of a visiting iterator

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

Similar to map_expr but on statements

val fold_expr : ('a -> Ast.Expr.expr -> 'a visit_action) -> ('a -> Ast.Stmt.stmt -> 'a visit_action) -> 'a -> 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 -> Ast.Expr.expr -> 'a visit_action) -> ('a -> Ast.Stmt.stmt -> 'a visit_action) -> 'a -> Ast.Stmt.stmt -> 'a

Similar to fold_expr but on statements

val fold_map_expr : ('a -> Ast.Expr.expr -> ('a * Ast.Expr.expr) visit_action) -> ('a -> Ast.Stmt.stmt -> ('a * Ast.Stmt.stmt) visit_action) -> 'a -> Ast.Expr.expr -> 'a * Ast.Expr.expr

Combination of map and fold for expressions

val fold_map_stmt : ('a -> Ast.Expr.expr -> ('a * Ast.Expr.expr) visit_action) -> ('a -> Ast.Stmt.stmt -> ('a * Ast.Stmt.stmt) visit_action) -> 'a -> Ast.Stmt.stmt -> 'a * Ast.Stmt.stmt

Combination of map and fold for statements

val exists_expr : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Expr.expr -> bool
val for_all_expr : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Expr.expr -> bool
val exists_stmt : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Stmt.stmt -> bool
val for_all_stmt : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Stmt.stmt -> bool
val exists_child_expr : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Expr.expr -> bool
val for_all_child_expr : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Expr.expr -> bool
val exists_child_stmt : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Stmt.stmt -> bool
val for_all_child_stmt : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Stmt.stmt -> bool

Utility functions

val is_leaf_expr : Ast.Expr.expr -> bool

Test whether an expression is a leaf expression

val is_atomic_expr : Ast.Expr.expr -> bool

Test whether an expression has no sub-statement

val is_atomic_stmt : Ast.Stmt.stmt -> bool

Test whether a statement has no sub-statement

val expr_vars : Ast.Expr.expr -> Ast.Var.var list

Get all variables present in an expression

val stmt_vars : Ast.Stmt.stmt -> Ast.Var.var list

Get all variables present in a statement

val is_var_in_expr : Ast.Var.var -> Ast.Expr.expr -> bool

Check whether a variable appears in an expression

val is_var_in_stmt : Ast.Var.var -> Ast.Stmt.stmt -> bool

Check whether a variable appears in a statement

Deprecated

val fold_sub_expr : ('a -> Ast.Expr.expr -> 'a visit_action) -> ('a -> Ast.Stmt.stmt -> 'a visit_action) -> 'a -> Ast.Expr.expr -> 'a
include module type of struct include 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 = Core.Alarm.check = ..
val pp_check : Stdlib.Format.formatter -> check -> unit

Print a check

val register_check : ((Stdlib.Format.formatter -> check -> unit) -> Stdlib.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 = Core.Alarm.alarm_kind = ..
type alarm_kind +=
  1. | A_generic of check
type alarm = Core.Alarm.alarm = {
  1. alarm_kind : alarm_kind;
  2. alarm_check : check;
  3. alarm_range : Mopsa_utils.Location.range;
  4. alarm_callstack : Mopsa_utils.Callstack.callstack;
}

Create an alarm

val check_of_alarm : alarm -> check

Return the check associate to an alarm

val range_of_alarm : alarm -> Mopsa_utils.Location.range

Return the range of an alarm

val callstack_of_alarm : alarm -> Mopsa_utils.Callstack.callstack

Return the callstack of an alarm

val compare_alarm : alarm -> alarm -> int

Compare two alarms

val pp_alarm : Stdlib.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 : Stdlib.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 : ((Stdlib.Format.formatter -> alarm_kind -> unit) -> Stdlib.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 = Core.Alarm.alarm_info = {
  1. check : (alarm_kind -> check) -> alarm_kind -> check;
  2. compare : (alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int;
  3. print : (Stdlib.Format.formatter -> alarm_kind -> unit) -> Stdlib.Format.formatter -> alarm_kind -> unit;
  4. 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 = Framework.Core.All.AlarmSet

Set of alarms

type diagnostic_kind = Core.Alarm.diagnostic_kind =
  1. | Warning
    (*

    Some executions may have issues

    *)
  2. | Safe
    (*

    All executions are safe

    *)
  3. | Error
    (*

    All executions do have issues

    *)
  4. | Unreachable
    (*

    No execution reaches the check point

    *)

Kind of a diagnostic

type 'a diagnostic_ = 'a Core.Alarm.diagnostic_ = {
  1. diag_range : Mopsa_utils.Location.range;
  2. diag_check : check;
  3. diag_kind : diagnostic_kind;
  4. diag_alarms : AlarmSet.t;
  5. diag_callstack : 'a;
}
type diagnosticWoCs = unit 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

Create a diagnostic that says that a check maybe unsafe

Create a diagnostic that says that a check is unreachable

val pp_diagnostic_kind : Stdlib.Format.formatter -> diagnostic_kind -> unit

Print a diagnostic kind

val pp_diagnostic : Stdlib.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 = Core.Alarm.assumption_scope =
  1. | A_local of Mopsa_utils.Location.range
    (*

    Local assumptions concern a specific location range in the program

    *)
  2. | A_global
    (*

    Global assumptions can concern the entire program

    *)

Scope of an assumption

type assumption_kind = Core.Alarm.assumption_kind = ..

Domains can add new kinds of assumptions by extending the type assumption_kind

type assumption_kind +=
  1. | A_ignore_unsupported_stmt of Ast.Stmt.stmt

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

type assumption_kind +=
  1. | A_ignore_unsupported_expr of Ast.Expr.expr
type assumption = Core.Alarm.assumption = {
  1. assumption_scope : assumption_scope;
  2. assumption_kind : assumption_kind;
}
val register_assumption : assumption_kind Mopsa_utils.TypeExt.info -> unit

Register a new kind of assumptions

val pp_assumption_kind : Stdlib.Format.formatter -> assumption_kind -> unit

Print an assumption kind

val pp_assumption : Stdlib.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.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 = Framework.Core.All.RangeMap
module RangeCallStackMap = Framework.Core.All.RangeCallStackMap
module CheckMap = Framework.Core.All.CheckMap
module AssumptionSet = Framework.Core.All.AssumptionSet
type report = Core.Alarm.report = {
  1. report_diagnostics : diagnostic CheckMap.t RangeCallStackMap.t;
  2. 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 : Stdlib.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

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 = Framework.Core.All.RangeDiagnosticWoCsMap
module CallstackSet = Framework.Core.All.CallstackSet

Set of callstacks

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.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
include module type of struct include Core.Context end
type ('a, _) ctx_key = ('a, _) Core.Context.ctx_key = ..

Key to access an element in the context

type 'a ctx = 'a 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 : (Core.Print.printer -> 'a -> unit) -> Stdlib.Format.formatter -> 'a ctx -> unit

Print a context

type ctx_pool = Core.Context.ctx_pool = {
  1. ctx_pool_equal : 'a 'v 'w. ('a, 'v) ctx_key -> ('a, 'w) ctx_key -> ('v, 'w) Mopsa_utils.Eq.eq option;
  2. ctx_pool_print : 'a 'v. (Core.Print.printer -> 'a -> unit) -> Stdlib.Format.formatter -> ('a, 'v) ctx_key -> 'v -> unit;
}

Pool registered keys

type ctx_info = Core.Context.ctx_info = {
  1. ctx_equal : 'a 'v 'w. ctx_pool -> ('a, 'v) ctx_key -> ('a, 'w) ctx_key -> ('v, 'w) Mopsa_utils.Eq.eq option;
  2. ctx_print : 'a 'v. ctx_pool -> (Core.Print.printer -> 'a -> unit) -> Stdlib.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 = Framework.Core.All.GenContextKey

Generate a new key

val callstack_ctx_key : ('a, Mopsa_utils.Callstack.callstack) ctx_key

Key for storing the callstack

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
type 'a eval = 'a Eval.eval
type 'a flow = 'a Flow.flow
module Post = 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
include module type of struct include Effect end

Effects

type effect = Core.Effect.effect =
  1. | Effect_empty
  2. | Effect_block of Ast.Stmt.stmt list
  3. | Effect_seq of effect list
  4. | Effect_join of effect * effect
  5. | Effect_meet of effect * effect
val pp_effect : Stdlib.Format.formatter -> effect -> unit

Print a effect

val compare_effect : effect -> effect -> int

Compare two effects

val empty_effect : effect

Empty effect

val is_empty_effect : effect -> bool

Check whether a effect is empty

val join_effect : effect -> effect -> effect

Compute the union of two effects

val meet_effect : effect -> effect -> effect

Compute the intersection of two effects

val fold_stmt_effect : ('a -> Ast.Stmt.stmt -> 'a) -> 'a -> effect -> 'a

Fold over the statements in the effect

Effect trees

type teffect = Core.Effect.teffect =
  1. | Teffect_empty
  2. | Teffect_node of effect * teffect * teffect

Effects are presented as binary trees. Each node of the tree is associated to a domain in the abstraction and stores the statements executed by the domain when computing a post-condition.

Note that this representation is also useful when we have an abstraction DAG (i.e. when there are shared domains) thanks to the compose (stack) operator:

A x B \___/ | C

is represented as:

o / \ x C / \ A B

val empty_teffect : teffect

Create an empty effects tree

val mk_teffect : effect -> teffect -> teffect -> teffect

mk_teffect effect left right creates an effect tree with a root containing effect and having left and right as the two sub-trees

val pp_teffect : Stdlib.Format.formatter -> teffect -> unit

Print an effects tree

val compare_teffect : teffect -> teffect -> int

Compare two effects trees

val is_empty_teffect : teffect -> bool

Check whether an effects tree is empty

val get_left_teffect : teffect -> teffect

get_left_teffect te returns the left sub-tree of te

val get_right_teffect : teffect -> teffect

get_right_teffect te returns the right sub-tree of te

val get_root_effect : teffect -> effect

get_log_stmts te returns the effect at the root node of te

val set_left_teffect : teffect -> teffect -> teffect

get_left_teffect left te sets left as the left sub-tree of te

val set_right_teffect : teffect -> teffect -> teffect

get_right_teffect right te sets right as the right sub-tree of te

val map_left_teffect : (teffect -> teffect) -> teffect -> teffect

map_left_teffect f te is equivalent to set_left_teffect (f (get_left_teffect te)) te

val map_right_teffect : (teffect -> teffect) -> teffect -> teffect

map_right_teffect f te is equivalent to set_right_teffect (f (get_right_teffect te)) te

val add_stmt_to_teffect : Ast.Stmt.stmt -> teffect -> teffect

add_stmt_to_teffect stmt teffect adds stmt to the the effects of the root no of te

val merge_teffect : (effect -> effect) -> (effect -> effect) -> (effect -> effect -> effect) -> teffect -> teffect -> teffect

merge_teffect f1 f2 f te1 te2 combines te1 and te2

val concat_teffect : old:teffect -> recent:teffect -> teffect

concat_teffect old recent puts effects in old before those in recent

val meet_teffect : teffect -> teffect -> teffect

merge_teffect te1 te2 computes the effects of two intersected post-states

val join_teffect : teffect -> teffect -> teffect

merge_teffect te1 te2 computes the effects of two joined post-states

val fold_stmt_teffect : ('a -> Ast.Stmt.stmt -> 'a) -> 'a -> teffect -> 'a

Fold over the statements in the effects tree

Generic merge

type var_effect = Core.Effect.var_effect = {
  1. modified : Ast.Var.VarSet.t;
  2. removed : Ast.Var.VarSet.t;
}

Effect of a statement in terms of modified and removed variables

val generic_merge : add:(Ast.Var.var -> 'b -> 'a -> 'a) -> find:(Ast.Var.var -> 'a -> 'b) -> remove:(Ast.Var.var -> 'a -> 'a) -> ?custom:(Ast.Stmt.stmt -> var_effect option) -> ('a * effect) -> ('a * effect) -> 'a * 'a

Generic merge operator. generic_merge ~add ~find ~remove ~custom (a1,e1) (a2,e2) applies a generic merge of states a1 and a2:

  • It searches for modified variables in one state's effects, gets their value using find and adds them to the other state using add.
  • It searches for removed variables in one state's effects and remove them from the other state using remove. This function handles common statements (assign,assume,add,remove,fold,expand and rename). Other statements can be handled using the custom function that returns the var_effect of a given statement.
val enable_effects : unit -> unit
val disable_effects : unit -> unit
val are_effects_enabled : unit -> bool
val set_effects_state : bool -> unit
val with_effects : (unit -> 'a) -> 'a
include module type of struct include Core.Query end
type ('a, _) query = ('a, _) Core.Query.query = ..

Extensible type of queries

val join_query : ?ctx:'a Core.Context.ctx option -> ?lattice:'a Core.Lattice.lattice option -> ('a, 'r) query -> 'r -> 'r -> 'r

Join two queries

val meet_query : ?ctx:'a Core.Context.ctx option -> ?lattice:'a Core.Lattice.lattice option -> ('a, 'r) query -> 'r -> 'r -> 'r

Meet two queries

Registration

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

type query_pool = Core.Query.query_pool = {
  1. pool_join : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
  2. pool_meet : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
}

Pool of registered queries

type query_info = Core.Query.query_info = {
  1. join : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. 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 = Core.Query.lattice_query_pool = {
  1. pool_join : 'a 'r. 'a Core.Context.ctx -> 'a Core.Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. pool_meet : 'a 'r. 'a Core.Context.ctx -> 'a 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 = Core.Query.lattice_query_info = {
  1. join : 'a 'r. lattice_query_pool -> 'a Core.Context.ctx -> 'a Core.Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. meet : 'a 'r. lattice_query_pool -> 'a Core.Context.ctx -> 'a 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 +=
  1. | Q_defined_variables : string option -> ('a, Ast.Var.var list) query
    (*

    Extract the list of defined variables, in a given function call site, or in all scopes

    *)
  2. | Q_allocated_addresses : ('a, Ast.Addr.addr list) query
    (*

    Query to extract the list of addresses allocated in the heap

    *)
  3. | Q_variables_linked_to : Ast.Expr.expr -> ('a, 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 +=
  1. | T_cur
    (*

    Token of current (active) execution flow

    *)
val register_token : token Mopsa_utils.TypeExt.info -> unit

Register a new token with its compare and print functions

val compare_token : token -> token -> int

Compare two tokens with a total order

val pp_token : Stdlib.Format.formatter -> token -> unit

Pretty printer of tokens

module TokenMap = Framework.Core.All.TokenMap
include module type of struct include Ast.Semantic end
type semantic = string
val compare_semantic : semantic -> semantic -> int
val pp_semantic : Stdlib.Format.formatter -> semantic -> unit
val any_semantic : semantic
val is_any_semantic : semantic -> bool
module SemanticSet = Framework.Core.All.SemanticSet
module SemanticMap = Framework.Core.All.SemanticMap
include module type of struct include Core.Route end
type domain = string
type route = Core.Route.route =
  1. | Below of domain
    (*

    Sub-tree below a domain

    *)
  2. | Semantic of Ast.Semantic.semantic
    (*

    Sub-tree identified by a semantic

    *)

Routes

module DomainSet = Framework.Core.All.DomainSet
val compare_route : route -> route -> int

Set of domains

Compare two routes

val pp_route : Stdlib.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 : Stdlib.Format.formatter -> routing_table -> unit

Print a routing table

include module type of struct include Core.Lattice end
module type LATTICE = Framework.Core.All.LATTICE

Signature of a lattice module.

type 'a lattice = 'a Core.Lattice.lattice = {
  1. bottom : 'a;
  2. top : 'a;
  3. is_bottom : 'a -> bool;
  4. subset : 'a Core.Context.ctx -> 'a -> 'a -> bool;
  5. join : 'a Core.Context.ctx -> 'a -> 'a -> 'a;
  6. meet : 'a Core.Context.ctx -> 'a -> 'a -> 'a;
  7. widen : 'a Core.Context.ctx -> 'a -> 'a -> 'a;
  8. merge : 'a -> ('a * Core.Effect.teffect) -> ('a * Core.Effect.teffect) -> 'a;
  9. print : 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 = {
  1. eq : 'a 'b. 'a id -> 'b id -> ('a, 'b) Mopsa_utils.Eq.eq option;
}
type witness_chain = Core.Id.witness_chain = {
  1. eq : 'a 'b. witness -> 'a id -> 'b id -> ('a, 'b) Mopsa_utils.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.Eq.eq option

Equality witness of identifiers

module GenDomainId = Framework.Core.All.GenDomainId

Generator of a new domain identifier

module GenStatelessDomainId = Framework.Core.All.GenStatelessDomainId

Generator of a new identifier for stateless domains

module GenValueId = Framework.Core.All.GenValueId

Generator of a new value identifier

include module type of struct include Core.Manager end

Managers

type ('a, 't) man = ('a, 't) Core.Manager.man = {
  1. lattice : 'a Core.Lattice.lattice;
    (*

    Access to lattice operators on the toplevel abstract element 'a.

    *)
  2. get : 'a -> 't;
    (*

    Returns the domain's abstract element 't.

    *)
  3. set : 't -> 'a -> 'a;
    (*

    Sets the domain's abstract element 't.

    *)
  4. exec : ?route:Core.Route.route -> Ast.Stmt.stmt -> 'a Core.Flow.flow -> 'a Core.Post.post;
    (*

    man.exec stmt flow executes stmt in flow and returns the post state.

    *)
  5. eval : ?route:Core.Route.route -> ?translate:Ast.Semantic.semantic -> ?translate_when:(Ast.Semantic.semantic * (Ast.Expr.expr -> bool)) list -> Ast.Expr.expr -> 'a Core.Flow.flow -> 'a 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.

    *)
  6. ask : 'r. ?route:Core.Route.route -> ('a, 'r) 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.

    *)
  7. print_expr : ?route:Core.Route.route -> 'a Core.Flow.flow -> Core.Print.printer -> Ast.Expr.expr -> unit;
    (*

    man.print_expr flow is the expression printer for the type 'a.

    *)
  8. get_effects : Core.Effect.teffect -> Core.Effect.teffect;
    (*

    Gets the effects tree.

    *)
  9. set_effects : Core.Effect.teffect -> Core.Effect.teffect -> Core.Effect.teffect;
    (*

    Sets the effect tree.

    *)
}

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).

include module type of struct include Core.Print end
type symbols = Core.Print.symbols = {
  1. sopen : string;
  2. ssep : string;
  3. sbind : string;
  4. sclose : string;
}

Symbols for printing maps, lists and sets

type ('k, 'v) map = ('k, 'v) Mopsa_utils.MapExtPoly.t

Structured print objects

type 'v set = 'v Mopsa_utils.SetExtPoly.t
type print_object = Core.Print.print_object =
  1. | Empty
  2. | Bool of bool
  3. | Int of Z.t
  4. | Float of float
  5. | String of string
  6. | Var of Ast.Var.var
  7. | Map of (print_object, print_object) map * symbols
  8. | List of print_object list * symbols
  9. | Set of print_object set * symbols

Printers

type printer = 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 -> Ast.Expr.expr list

Get the expressions that were already printed

val add_printed_expr : printer -> Ast.Expr.expr -> unit

Mark an expression as printed

val mem_printed_expr : printer -> Ast.Expr.expr -> bool

Check whether an expression was already printed

type print_selector = Core.Print.print_selector =
  1. | Key of string
  2. | Index of int
  3. | 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, Stdlib.Format.formatter, unit, print_object) Stdlib.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, Stdlib.Format.formatter, unit, print_selector) Stdlib.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 -> 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 : Stdlib.Format.formatter -> print_object -> unit

Pretty-print a printer objct

val pflush : Stdlib.Format.formatter -> printer -> unit

Pretty-print the printer output in a format string

val format : (printer -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit

Convert a printer function into a format function

val unformat : ?path:print_path -> (Stdlib.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

include module type of struct include Core.Avalue end
type _ avalue_kind = _ Core.Avalue.avalue_kind = ..
type avalue_pool = Core.Avalue.avalue_pool = {
  1. pool_typ : 'v. 'v avalue_kind -> Ast.Typ.typ;
  2. pool_bottom : 'v. 'v avalue_kind -> 'v;
  3. pool_top : 'v. 'v avalue_kind -> 'v;
  4. pool_join : 'v. 'v avalue_kind -> 'v -> 'v -> 'v;
  5. pool_meet : 'v. 'v avalue_kind -> 'v -> 'v -> 'v;
  6. pool_compare : 'v 'w. 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int;
  7. pool_print : 'v. 'v avalue_kind -> Stdlib.Format.formatter -> 'v -> unit;
}
type avalue_info = Core.Avalue.avalue_info = {
  1. typ : 'v. avalue_pool -> 'v avalue_kind -> Ast.Typ.typ;
  2. bottom : 'v. avalue_pool -> 'v avalue_kind -> 'v;
  3. top : 'v. avalue_pool -> 'v avalue_kind -> 'v;
  4. join : 'v. avalue_pool -> 'v avalue_kind -> 'v -> 'v -> 'v;
  5. meet : 'v. avalue_pool -> 'v avalue_kind -> 'v -> 'v -> 'v;
  6. compare : 'v 'w. avalue_pool -> 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int;
  7. print : 'v. avalue_pool -> 'v avalue_kind -> Stdlib.Format.formatter -> 'v -> unit;
}
val register_avalue : avalue_info -> unit
val type_of_avalue : 'v avalue_kind -> 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 -> Stdlib.Format.formatter -> 'v -> unit
val mk_avalue_expr : 'v avalue_kind -> 'v -> Mopsa_utils.Location.range -> Ast.Expr.expr
val mk_avalue_constant : 'v avalue_kind -> 'v -> Ast.Constant.constant
type Core.Query.query +=
  1. | Q_avalue : Ast.Expr.expr * 'v avalue_kind -> ('a, 'v) Core.Query.query
val mk_avalue_query : Ast.Expr.expr -> 'v avalue_kind -> ('a, 'v) Core.Query.query
include module type of struct include Core.Utils end
val exec_cleaner : Ast.Stmt.stmt -> ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> ('a, unit) Core.Cases.cases
val exec_cleaners : ('a, 'b) Core.Manager.man -> ('a, unit) Core.Cases.cases -> ('a, unit) Core.Cases.cases
val post_to_flow : ('a, 'b) Core.Manager.man -> 'a Core.Post.post -> 'a Core.Flow.flow
val assume : Ast.Expr.expr -> ?route:Core.Route.route -> ?translate: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) Core.Manager.man -> 'a Core.Flow.flow -> ('a, 'b) Core.Cases.cases
val switch : (Ast.Expr.expr list * ('a Core.Flow.flow -> ('a, 'r) Core.Cases.cases)) list -> ?route:Core.Route.route -> ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> ('a, 'r) Core.Cases.cases
val set_env : Core.Token.token -> 't -> ('a, 't) Core.Manager.man -> 'a Core.Flow.flow -> 'a Core.Flow.flow
val get_env : Core.Token.token -> ('a, 't) Core.Manager.man -> 'a Core.Flow.flow -> 't
val map_env : Core.Token.token -> ('t -> 't) -> ('a, 't) Core.Manager.man -> 'a Core.Flow.flow -> 'a Core.Flow.flow
val get_pair_fst : ('a, 'b * 'c) Core.Manager.man -> 'a -> 'b
val set_pair_fst : ('a, 'b * 'c) Core.Manager.man -> 'b -> 'a -> 'a
val get_pair_snd : ('a, 'b * 'c) Core.Manager.man -> 'a -> 'c
val set_pair_snd : ('a, 'b * 'c) Core.Manager.man -> 'c -> 'a -> 'a
val env_exec : ('a Core.Flow.flow -> 'a Core.Post.post) -> 'a Core.Context.ctx -> ('a, 't) Core.Manager.man -> 'a -> 'a
val ask_and_reduce_cases : (('a, 'b) Core.Query.query -> 'c -> ('d, 'b) Core.Cases.cases) -> ('a, 'b) Core.Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
val ask_and_reduce_list : (('a, 'b) Core.Query.query -> 'c -> ('d * 'b) list) -> ('a, 'b) Core.Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
val ask_and_reduce : (('a, 'b) Core.Query.query -> 'c -> ('d, 'b) Core.Cases.cases) -> ('a, 'b) Core.Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
val find_var_by_name : ?function_scope:string option -> string -> ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> Ast.Var.var
val dummy_range : Mopsa_utils.Location.range
val pp_vars_info : ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> Stdlib.Format.formatter -> Ast.Var.var list -> unit
val pp_vars_info_by_name : ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> Stdlib.Format.formatter -> string list -> unit
val pp_expr_vars_info : ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> Stdlib.Format.formatter -> Ast.Expr.expr -> unit
val pp_stmt_vars_info : ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> Stdlib.Format.formatter -> Ast.Stmt.stmt -> unit
val breakpoint : string -> ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> unit
module Core = Framework.Core
module Sig = Framework.Sig
module Params = Framework.Params
module Paths = Framework.Params.Paths
include module type of struct include Location end

Positions

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

type pos = Utils_core.Location.pos = {
  1. pos_file : string;
    (*

    File name.

    *)
  2. pos_line : int;
    (*

    Line number.

    *)
  3. 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

Ranges

==========

type range = Utils_core.Location.range =
  1. | R_program of string list
    (*

    list of source files

    *)
  2. | R_orig of pos * pos
    (*

    end position

    *)
  3. | R_fresh of int
    (*

    non-original fresh range with unique id

    *)
  4. | R_tagged of range_tag * range
    (*

    Tagged range with an annotation

    *)

Location range of AST nodes.

and range_tag = Utils_core.Location.range_tag =
  1. | String_tag of string
  2. | 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, Stdlib.Format.formatter, unit, range_tag) Stdlib.format4 -> 'a
val mk_range_tag : range -> range_tag
val mk_range_tagged_range : range -> range -> range
val tag_range : range -> ('a, Stdlib.Format.formatter, unit, range) Stdlib.format4 -> 'a

Tag a range with a (formatted) annotation.

val mk_orig_range : pos -> pos -> range
val fresh_range_counter : int Stdlib.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 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 : Stdlib.Lexing.position -> pos
val from_lexing_range : Stdlib.Lexing.position -> Stdlib.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 Utils_core.Location.with_range = {
  1. content : 'a;
  2. 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 : Stdlib.Format.formatter -> pos -> unit
val pp_relative_position : Stdlib.Format.formatter -> pos -> unit
val pp_range : Stdlib.Format.formatter -> range -> unit
val pp_relative_range : Stdlib.Format.formatter -> range -> unit
include module type of struct include Callstack end

Call sites

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

type callsite = Utils_core.Callstack.callsite = {
  1. call_fun_orig_name : string;
    (*

    Original name of the called function

    *)
  2. call_fun_uniq_name : string;
    (*

    Unique name of the called function

    *)
  3. call_range : Utils_core.Location.range;
    (*

    Call location

    *)
}

Call site is the location of a call in the program

val pp_callsite : Stdlib.Format.formatter -> callsite -> unit

Print a call site

val compare_callsite : callsite -> callsite -> int

Compare two call sites

Call stacks

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

type callstack = callsite list

A call stack

val pp_callstack : Stdlib.Format.formatter -> callstack -> unit

Print a call stack

val pp_callstack_short : Stdlib.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 -> 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 cs returns the last call site in cs and the remaining call stack. 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 Framework.Params.Options end

Registration

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

val register_builtin_option : Mopsa_utils.ArgExt.arg -> unit

Register a built-in option

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

Register a language option.

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

Register a domain option.

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

Register a shared option

val import_shared_option : string -> string -> unit

Import a shared option into a domain

Filters

***********

val get_options : unit -> Mopsa_utils.ArgExt.arg list

Return the list of options

val get_builtin_options : unit -> Mopsa_utils.ArgExt.arg list

Return the list of built-in options

val get_language_options : string -> Mopsa_utils.ArgExt.arg list

Return the list of options of a language

val get_domain_options : string -> Mopsa_utils.ArgExt.arg list

Return the list of options of a domain

val help : unit -> unit
include module type of struct include Exceptions end

Warnings

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

val warn : ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a
val warn_at : Utils_core.Location.range -> ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a

Panic exceptions

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

val pp : ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a
val pp_at : Utils_core.Location.range -> ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a
exception Panic of string * string

OCaml line of code

exception PanicAtLocation of Utils_core.Location.range * string * string

OCaml line of code

OCaml line of code

exception PanicAtFrame of Utils_core.Location.range * Utils_core.Callstack.callstack * string * string

OCaml line of code

OCaml line of code

val panic : ?loc:string -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

Raise a panic exception using a formatted string

val panic_at : ?loc:string -> Utils_core.Location.range -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
val panic_at_frame : ?loc:string -> Utils_core.Location.range -> Utils_core.Callstack.callstack -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

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

exception SyntaxError of Utils_core.Location.range * string
exception SyntaxErrorList of (Utils_core.Location.range * string) list
exception UnnamedSyntaxError of Utils_core.Location.range
exception UnnamedSyntaxErrorList of Utils_core.Location.range list
val syntax_error : Utils_core.Location.range -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
val syntax_errors : (Utils_core.Location.range * string) list -> 'a
val unnamed_syntax_error : Utils_core.Location.range -> 'a
val unnamed_syntax_errors : Utils_core.Location.range list -> 'a
type 'a info = 'a 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, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a

Encapsulate a domain into a top-level abstraction

OCaml

Innovation. Community. Security.

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