Module Parsing.AstSource

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

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