package mopsa

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

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

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

and section =
  1. | S_case of case
  2. | S_leaf of leaf
and 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

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

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

Expressions

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

and expr = {
  1. kind : expr_kind;
  2. typ : Mopsa_c_parser.C_AST.type_qual;
}
and log_binop = Cst.log_binop
and binop = Cst.binop
and unop = Cst.unop
and set =
  1. | S_interval of interval
  2. | S_resource of resource
and 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

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

Formulas

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

Utility functions

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

val compare_resource : 'a -> 'a -> int

Pretty printers

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

val pp_var : Stdlib.Format.formatter -> Mopsa_c_parser.C_AST.variable -> unit
val pp_resource : Stdlib.Format.formatter -> string -> unit
val pp_builtin : Stdlib.Format.formatter -> Cst.builtin -> unit
val pp_list : (Stdlib.Format.formatter -> 'a -> unit) -> (unit, Stdlib.Format.formatter, unit) Stdlib.format -> Stdlib.Format.formatter -> 'a list -> unit
val pp_opt : ('a -> 'b -> unit) -> 'a -> 'b option -> unit
val pp_expr : Stdlib.Format.formatter -> expr Mopsa_utils.Location.with_range -> unit
val pp_unop : Stdlib.Format.formatter -> unop -> unit
val pp_binop : Stdlib.Format.formatter -> binop -> unit
val pp_c_qual_typ : Stdlib.Format.formatter -> Mopsa_c_parser.C_AST.type_qual -> unit
val pp_formula : Stdlib.Format.formatter -> formula Mopsa_utils.Location.with_range -> unit
val pp_log_binop : Stdlib.Format.formatter -> log_binop -> unit
val pp_set : Stdlib.Format.formatter -> set -> unit
val pp_interval : Stdlib.Format.formatter -> interval -> unit
val pp_local : Stdlib.Format.formatter -> local Mopsa_utils.Location.with_range -> unit
val pp_local_value : Stdlib.Format.formatter -> local_value -> unit
val pp_requires : Stdlib.Format.formatter -> formula Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range -> unit
val pp_assigns : Stdlib.Format.formatter -> assigns Mopsa_utils.Location.with_range -> unit
val pp_assumes : Stdlib.Format.formatter -> assumes Mopsa_utils.Location.with_range -> unit
val pp_ensures : Stdlib.Format.formatter -> formula Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range -> unit
val pp_free : Stdlib.Format.formatter -> expr Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range -> unit
val pp_message : Stdlib.Format.formatter -> message Mopsa_utils.Location.with_range -> unit
val pp_leaf_section : Stdlib.Format.formatter -> leaf -> unit
val pp_leaf_sections : Stdlib.Format.formatter -> leaf list -> unit
val pp_case : Stdlib.Format.formatter -> case -> unit
val pp_section : Stdlib.Format.formatter -> section -> unit
val pp_sections : Stdlib.Format.formatter -> section list -> unit
OCaml

Innovation. Community. Security.