package mopsa

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

Install 

dune-project
 Dependency

gitlab.com 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.0.tar.gz
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4

doc/parsing/Parsing/Ast/index.html

Module Parsing.AstSource

Abstract syntax tree for C stubs. It is similar to the CST except:

  • predicates are expanded.
  • types and variables are resolved using the context of the Clang parser.
  • calls to sizeof are resolved using Clang's target information.
  • stubs and cases record their locals and assignments.
Sourcetype stub = {
  1. stub_name : string;
  2. stub_params : var list;
  3. stub_locals : local Mopsa_utils.Location.with_range list;
  4. stub_assigns : assigns Mopsa_utils.Location.with_range list;
  5. stub_body : section list;
  6. stub_range : Mopsa_utils.Location.range;
}

Stub sections

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

Sourceand section =
  1. | S_case of case
  2. | S_leaf of leaf
Sourceand case = {
  1. case_label : string;
  2. case_body : leaf list;
  3. case_locals : local Mopsa_utils.Location.with_range list;
  4. case_assigns : assigns Mopsa_utils.Location.with_range list;
  5. case_range : Mopsa_utils.Location.range;
}

Leaf sections

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

Sourceand local = {
  1. lvar : var;
  2. lval : local_value;
}
Sourceand assigns = {
  1. assign_target : expr Mopsa_utils.Location.with_range;
  2. assign_offset : interval list;
}
Sourceand message = {
  1. message_kind : message_kind;
  2. message_body : string;
}
Sourceand message_kind = Cst.message_kind =
  1. | WARN
  2. | UNSOUND

Expressions

*=*=*=*=*=*=*=*

Sourceand log_binop = Cst.log_binop
Sourceand binop = Cst.binop
Sourceand unop = Cst.unop
Sourceand set =
  1. | S_interval of interval
  2. | S_resource of resource
Sourceand interval = {
  1. itv_lb : expr Mopsa_utils.Location.with_range;
    (*

    lower bound

    *)
  2. itv_open_lb : bool;
    (*

    open lower bound

    *)
  3. itv_ub : expr Mopsa_utils.Location.with_range;
    (*

    upper bound

    *)
  4. itv_open_ub : bool;
    (*

    open upper bound

    *)
}
Sourceand resource = string
Sourceand builtin = Cst.builtin

Formulas

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

Utility functions

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

Sourceval compare_resource : 'a -> 'a -> int

Pretty printers

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

Sourceval pp_var : Stdlib.Format.formatter -> Mopsa_c_parser.C_AST.variable -> unit
Sourceval pp_resource : Stdlib.Format.formatter -> string -> unit
Sourceval pp_builtin : Stdlib.Format.formatter -> Cst.builtin -> 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_expr : Stdlib.Format.formatter -> expr Mopsa_utils.Location.with_range -> unit
Sourceval pp_unop : Stdlib.Format.formatter -> unop -> unit
Sourceval pp_binop : Stdlib.Format.formatter -> binop -> unit
Sourceval pp_c_qual_typ : Stdlib.Format.formatter -> Mopsa_c_parser.C_AST.type_qual -> unit
Sourceval pp_formula : Stdlib.Format.formatter -> formula Mopsa_utils.Location.with_range -> unit
Sourceval pp_log_binop : Stdlib.Format.formatter -> log_binop -> unit
Sourceval pp_set : Stdlib.Format.formatter -> set -> unit
Sourceval pp_interval : Stdlib.Format.formatter -> interval -> unit
Sourceval pp_local : Stdlib.Format.formatter -> local Mopsa_utils.Location.with_range -> unit
Sourceval pp_local_value : Stdlib.Format.formatter -> local_value -> unit
Sourceval pp_requires : Stdlib.Format.formatter -> formula Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range -> unit
Sourceval pp_assigns : Stdlib.Format.formatter -> assigns Mopsa_utils.Location.with_range -> unit
Sourceval pp_assumes : Stdlib.Format.formatter -> assumes Mopsa_utils.Location.with_range -> unit
Sourceval pp_ensures : Stdlib.Format.formatter -> formula Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range -> unit
Sourceval pp_free : Stdlib.Format.formatter -> expr Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range -> unit
Sourceval pp_message : Stdlib.Format.formatter -> message Mopsa_utils.Location.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