package mopsa

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

Module Stubs.AstSource

Abstract Syntax Tree for stub specification. Similar to the AST of the parser, except for expressions, types and variables for which MOPSA counterparts are used.

Sourcetype stub_func = {
  1. stub_func_name : string;
  2. stub_func_body : section list;
  3. stub_func_params : Mopsa.var list;
  4. stub_func_locals : local Mopsa.with_range list;
  5. stub_func_assigns : assigns Mopsa.with_range list;
  6. stub_func_return_type : Mopsa.typ option;
  7. stub_func_range : Mopsa.range;
}

Stub for a function

Sourceand stub_directive = {
  1. stub_directive_body : section list;
  2. stub_directive_locals : local Mopsa.with_range list;
  3. stub_directive_assigns : assigns Mopsa.with_range list;
  4. stub_directive_range : Mopsa.range;
}

Stub for a global directive

Stub sections

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

Sourceand section =
  1. | S_case of case
  2. | S_leaf of leaf
Sourceand leaf =
  1. | S_local of local Mopsa.with_range
  2. | S_assumes of assumes Mopsa.with_range
  3. | S_requires of requires Mopsa.with_range
  4. | S_assigns of assigns Mopsa.with_range
  5. | S_ensures of ensures Mopsa.with_range
  6. | S_free of free Mopsa.with_range
  7. | S_message of message Mopsa.with_range
Sourceand case = {
  1. case_label : string;
  2. case_body : leaf list;
  3. case_locals : local Mopsa.with_range list;
  4. case_assigns : assigns Mopsa.with_range list;
  5. case_range : Mopsa.range;
}

Leaf sections

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

Sourceand local = {
  1. lvar : Mopsa.var;
  2. lval : local_value;
}
Sourceand local_value =
  1. | L_new of resource
  2. | L_call of Mopsa.expr * Mopsa.expr list
Sourceand assigns = {
  1. assign_target : Mopsa.expr;
  2. assign_offset : interval list;
}
Sourceand free = Mopsa.expr
Sourceand message = {
  1. message_kind : message_kind;
  2. message_body : string;
}
Sourceand message_kind =
  1. | WARN
  2. | UNSOUND
Sourceand log_binop = Mopsa_c_stubs_parser.Cst.log_binop =
  1. | AND
  2. | OR
  3. | IMPLIES
Sourceand set =
  1. | S_interval of interval
  2. | S_resource of resource
Sourceand interval = Mopsa.expr * Mopsa.expr

Formulas

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

Sourceval compare_assigns : assigns -> assigns -> int
Sourceval compare_resource : 'a -> 'a -> int
Sourceval compare_set : set -> set -> int
Sourceval compare_formula : formula Mopsa.with_range -> formula Mopsa.with_range -> int

Expressions

Sourcetype quant =
  1. | FORALL
  2. | EXISTS

Quantifiers

Sourcetype Mopsa.expr_kind +=
  1. | E_stub_call of stub_func * Mopsa.expr list
    (*

    arguments

    *)
  2. | E_stub_return
    (*

    Returned value of a stub

    *)
  3. | E_stub_builtin_call of builtin * Mopsa.expr list
    (*

    Call to a built-in function

    *)
  4. | E_stub_attribute of Mopsa.expr * string
    (*

    Access to an attribute of a resource

    *)
  5. | E_stub_alloc of string * Mopsa.mode
    (*

    strong or weak

    *)
  6. | E_stub_resource_mem of Mopsa.expr * resource
    (*

    Filter environments in which an instance is in a resource pool

    *)
  7. | E_stub_primed of Mopsa.expr
    (*

    Primed expressions denoting values in the post-state

    *)
  8. | E_stub_quantified_formula of (quant * Mopsa.var * set) list * Mopsa.expr
    (*

    Quantifier-free formula

    *)
  9. | E_stub_otherwise of Mopsa.expr * Mopsa.expr option
    (*

    alarm

    *)
  10. | E_stub_raise of string
    (*

    message

    *)
  11. | E_stub_if of Mopsa.expr * Mopsa.expr * Mopsa.expr
    (*

    else

    *)

Conditional stub expression

Statements

Sourcetype Mopsa.stmt_kind +=
  1. | S_stub_directive of stub_directive
    (*

    A call to a stub directive, which are stub functions called at the initialization of the analysis. Useful to initialize variables with stub formulas.

    *)
  2. | S_stub_free of Mopsa.expr
    (*

    Release a resource

    *)
  3. | S_stub_requires of Mopsa.expr
    (*

    Filter the current environments that verify a condition, and raise an alarm if the condition may be violated.

    *)
  4. | S_stub_prepare_all_assigns of assigns list
    (*

    Prepare primed copies of assigned objects

    *)
  5. | S_stub_assigns of assigns
    (*

    Declare an assigned object

    *)
  6. | S_stub_clean_all_assigns of assigns list
    (*

    Clean the post-state of primed copies

    *)

Heap addresses for resources

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

Sourcetype Mopsa.addr_kind +=
  1. | A_stub_resource of string
    (*

    resource address

    *)

Utility functions

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

Sourceval mk_stub_builtin_call : builtin -> Mopsa.expr list -> etyp:Ast.Typ.typ -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_stub_prepare_all_assigns : assigns Mopsa.with_range list -> Mopsa_utils.Location.range -> Mopsa.stmt
Sourceval mk_stub_clean_all_assigns : assigns Mopsa.with_range list -> Mopsa_utils.Location.range -> Mopsa.stmt
Sourceval mk_stub_quantified_formula : ?etyp:Mopsa.typ -> (quant * Mopsa.var * set) list -> Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_stub_otherwise : Mopsa.expr -> Mopsa.expr option -> ?etyp:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval is_stub_primed : Ast.Expr.expr -> bool
Sourceval find_var_quantifier : Mopsa.var -> ('a * Mopsa.var * 'b) list -> 'a * 'b
Sourceval find_var_quantifier_opt : Mopsa.var -> ('a * Mopsa.var * 'b) list -> ('a * 'b) option
Sourceval is_quantified_var : Mopsa.var -> ('a * Mopsa.var * 'b) list -> bool
Sourceval is_forall_quantified_var : Mopsa.var -> (quant * Mopsa.var * 'a) list -> bool
Sourceval is_exists_quantified_var : Mopsa.var -> (quant * Mopsa.var * 'a) list -> bool
Sourceval find_quantified_var_interval : Mopsa.var -> ('a * Mopsa.var * set) list -> Mopsa.expr * Mopsa.expr
Sourceval find_quantified_var_interval_opt : Mopsa.var -> ('a * Mopsa.var * set) list -> (Mopsa.expr * Mopsa.expr) option
Sourceval negate_stub_quantified_formula : (quant * 'a * 'b) list -> Mopsa.expr -> (quant * 'a * 'b) list * Mopsa.expr

Visit expressions present in a formula

Sourceval mk_stub_alloc_resource : ?mode:Mopsa.mode -> string -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval negate_log_binop : log_binop -> log_binop

Pretty printers

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

Sourceval pp_builtin : Stdlib.Format.formatter -> Parsing.Cst.builtin -> unit
Sourceval pp_log_binop : Stdlib.Format.formatter -> Mopsa_c_stubs_parser.Ast.log_binop -> unit
Sourceval pp_quantifier : Stdlib.Format.formatter -> quant -> unit
Sourceval pp_formula : Stdlib.Format.formatter -> formula Mopsa.with_range -> unit
Sourceval pp_set : Stdlib.Format.formatter -> set -> unit
Sourceval pp_interval : Stdlib.Format.formatter -> interval -> unit
Sourceval pp_resource : Stdlib.Format.formatter -> resource -> unit
Sourceval pp_list : (Stdlib.Format.formatter -> 'a -> unit) -> (unit, Stdlib.Format.formatter, unit) Stdlib.format -> Stdlib.Format.formatter -> 'a list -> unit
Sourceval pp_opt : ('a -> 'b -> unit) -> 'a -> 'b option -> unit
Sourceval pp_local : Stdlib.Format.formatter -> local Mopsa.with_range -> unit
Sourceval pp_local_value : Stdlib.Format.formatter -> local_value -> unit
Sourceval pp_requires : Stdlib.Format.formatter -> formula Mopsa.with_range Mopsa.with_range -> unit
Sourceval pp_assigns : Stdlib.Format.formatter -> assigns Mopsa.with_range -> unit
Sourceval pp_assumes : Stdlib.Format.formatter -> assumes Mopsa.with_range -> unit
Sourceval pp_ensures : Stdlib.Format.formatter -> formula Mopsa.with_range Mopsa.with_range -> unit
Sourceval pp_free : Stdlib.Format.formatter -> Mopsa.expr Mopsa.with_range -> unit
Sourceval pp_message : Stdlib.Format.formatter -> message Mopsa.with_range -> unit
Sourceval pp_leaf_section : Stdlib.Format.formatter -> leaf -> unit
Sourceval pp_leaf_sections : Stdlib.Format.formatter -> leaf list -> unit
Sourceval pp_case : Stdlib.Format.formatter -> case -> unit
Sourceval pp_section : Stdlib.Format.formatter -> section -> unit
Sourceval pp_sections : Stdlib.Format.formatter -> section list -> unit
Sourceval pp_stub_func : Stdlib.Format.formatter -> stub_func -> unit
Sourceval pp_stub_directive : Stdlib.Format.formatter -> stub_directive -> unit

Registration of expressions

Registration of statements

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