Module `Core.All`Source

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

| 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 = {

ekind : expr_kind;
(*
kind of the expression
*)
etyp : Ast.Typ.typ;
(*
type of the expression
*)
erange : Mopsa_utils.Location.range;
(*
location range of the expression
*)
etrans : expr Ast.Semantic.SemanticMap.t;
(*
translations of the expression into other semantics
*)
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

val erange : expr -> Mopsa_utils.Location.range

Get the location of an expression

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

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

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

| E_addr of Ast.Addr.addr * Ast.Var.mode option
(*
optional access mode overloading the address access mode
*)
| 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

val mk_alloc_addr : 
  ?mode:Ast.Var.mode ->
  Ast.Addr.addr_kind ->
  Mopsa_utils.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 Ast.Constant.constant

Constants

val mk_constant : 
  ?etyp:Ast.Typ.typ ->
  Ast.Constant.constant ->
  Mopsa_utils.Location.range ->
  expr

Create a constant expression

val mk_top : Ast.Typ.typ -> Mopsa_utils.Location.range -> expr

Create ⊤ expression of a given type

Unary expressions

type expr_kind +=

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

Unary operator expressions

val mk_unop : 
  ?etyp:Ast.Typ.typ ->
  Ast.Operator.operator ->
  expr ->
  Mopsa_utils.Location.range ->
  expr

Create a unary operator expression

val mk_not : expr -> Mopsa_utils.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 Ast.Operator.operator * expr * expr
(*
second operand
*)

Binary operator expressions

val mk_binop : 
  ?etyp:Ast.Typ.typ ->
  expr ->
  Ast.Operator.operator ->
  expr ->
  Mopsa_utils.Location.range ->
  expr

Create a binary operator expression

val negate_expr : expr -> expr

Return the negation of an expression

Expressions containers

module ExprSet = Ast.Expr.ExprSet

Sets of expression

module ExprMap = Ast.Expr.ExprMap

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 = {

skind : stmt_kind;
(*
kind of the statement
*)
srange : Mopsa_utils.Location.range;
(*
location range of the statement
*)

}

Statements

val mk_stmt : stmt_kind -> Mopsa_utils.Location.range -> stmt

Create a statement

val skind : stmt -> stmt_kind

Get the kind of a statement

val srange : stmt -> Mopsa_utils.Location.range

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

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

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

| S_program of Ast.Program.program * string list option
(*
Command-line arguments as given to Mopsa after --
*)

Programs

type stmt_kind +=

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

Assignments

val mk_assign : 
  Ast.Expr.expr ->
  Ast.Expr.expr ->
  Mopsa_utils.Location.range ->
  stmt

mk_assign lhs rhs range creates the assignment lhs = rhs;

type stmt_kind +=

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

Tests

val mk_assume : Ast.Expr.expr -> Mopsa_utils.Location.range -> stmt

Create a test statement

type stmt_kind +=

| S_add of Ast.Expr.expr
(*
Add a dimension to the environment
*)
| S_remove of Ast.Expr.expr
(*
Remove a dimension from the environment and invalidate all references to it
*)
| S_invalidate of Ast.Expr.expr
(*
Invalidate all references to a dimension without removing it
*)
| S_rename of Ast.Expr.expr * Ast.Expr.expr
(*
new
*)
| S_forget of Ast.Expr.expr
(*
Forget a dimension by putting ⊤ (all possible values) in it. Note that the dimension is not removed
*)
| S_project of Ast.Expr.expr list
(*
Project the environment on the given list of dimensions. All other dimensions are removed
*)
| S_expand of Ast.Expr.expr * Ast.Expr.expr list
(*
Expand a dimension into a list of other dimensions. The expanded dimension is untouched
*)
| S_fold of Ast.Expr.expr * Ast.Expr.expr list
(*
Fold a list of dimensions into a single one. The folded dimensions are removed
*)
| S_block of stmt list * Ast.Var.var list
(*
local variables declared within the block
*)
| S_breakpoint of string
(*
Trigger a breakpoint
*)

Dimensions

val mk_rename : 
  Ast.Expr.expr ->
  Ast.Expr.expr ->
  Mopsa_utils.Location.range ->
  stmt

Utility functions to create various statements for dimension management

val mk_rename_var : 
  Ast.Var.var ->
  Ast.Var.var ->
  Mopsa_utils.Location.range ->
  stmt

val mk_remove : Ast.Expr.expr -> Mopsa_utils.Location.range -> stmt

val mk_remove_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt

val mk_invalidate : Ast.Expr.expr -> Mopsa_utils.Location.range -> stmt

val mk_invalidate_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt

val mk_add : Ast.Expr.expr -> Mopsa_utils.Location.range -> stmt

val mk_add_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 : Ast.Expr.expr -> Mopsa_utils.Location.range -> stmt

val mk_forget_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt

val mk_expand : 
  Ast.Expr.expr ->
  Ast.Expr.expr list ->
  Mopsa_utils.Location.range ->
  stmt

val mk_expand_var : 
  Ast.Var.var ->
  Ast.Var.var list ->
  Mopsa_utils.Location.range ->
  stmt

val mk_fold : 
  Ast.Expr.expr ->
  Ast.Expr.expr 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

module StmtSet = Ast.Stmt.StmtSet

Sets of statements

module StmtMap = Ast.Stmt.StmtMap

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

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

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

Common types

type typ +=

| T_any
(*
Generic unknown type
*)
| 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 = {

prog_kind : prog_kind;
(*
kind of the program
*)
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

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

include module type of struct include Ast.Frontend end

type frontend = Ast.Frontend.frontend = {

lang : string;
(*
Language of the frontend
*)
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

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

val register_operator_pp : operator Mopsa_utils.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 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 =

| 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 : 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 = {

vname : string;
(*
unique name of the variable
*)
vkind : var_kind;
(*
kind the variable
*)
vtyp : Ast.Typ.typ;
(*
type of the variable
*)
vmode : mode;
(*
access mode of the variable
*)
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

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

val register_var_pp : var Mopsa_utils.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.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

module VarSet = Ast.Var.VarSet

Sets of variables

module VarMap = Ast.Var.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 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 +=

| 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 = {

addr_kind : addr_kind;
(*
Kind of the address.
*)
addr_partitioning : addr_partitioning;
(*
Partitioning policy of the address
*)
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 +=

| 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 = {

exprs : Ast.Expr.expr list;
(*
sub-expressions
*)
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 = {

compare : 'a Mopsa_utils.TypeExt.compare;
(*
Comparison function for 'a
*)
print : 'a Mopsa_utils.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 : Ast.Expr.expr visit_info -> unit

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

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

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

Visiting iterators

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

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

Sourcetype check = Alarm.check = ..

Sourceval pp_check : Stdlib.Format.formatter -> check -> unit

Print a check

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/core/Core/All/index.html

Module Core.AllSource

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

Effects

Effect trees

Generic merge

Registration

Common queries

Managers

Print objects

Printers

Print paths

Generic print functions

Typed print functions

Format

JSON

dune-project
Dependency

Module `Core.All`Source