package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/stubs/Stubs/Ast/index.html

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