package mopsa

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

Concrete syntax tree for C stubs

Stub sections

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

and section =
  1. | S_case of case Mopsa_utils.Location.with_range
  2. | S_leaf of leaf
and case = {
  1. case_label : string;
  2. case_body : leaf list;
}

Stub leaf sections

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

and local = {
  1. lvar : var;
  2. ltyp : c_qual_typ;
  3. 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 =
  1. | WARN
  2. | UNSOUND

Formulas

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

Expressions

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

and int_suffix =
  1. | NO_SUFFIX
  2. | LONG
  3. | UNSIGNED_LONG
  4. | LONG_LONG
  5. | UNSIGNED_LONG_LONG
and log_binop =
  1. | AND
  2. | OR
  3. | IMPLIES
and binop =
  1. | ADD
  2. | SUB
  3. | MUL
  4. | DIV
  5. | MOD
  6. | RSHIFT
  7. | LSHIFT
  8. | LOR
  9. | LAND
  10. | LT
  11. | LE
  12. | GT
  13. | GE
  14. | EQ
  15. | NEQ
  16. | BOR
  17. | BAND
  18. | BXOR
and unop =
  1. | PLUS
  2. | MINUS
  3. | LNOT
  4. | BNOT
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 = var
and var = {
  1. vname : string;
    (*

    variable name

    *)
  2. vlocal : bool;
    (*

    is it a local variable ?

    *)
  3. vuid : int;
    (*

    unique identifier

    *)
  4. vtyp : c_qual_typ;
    (*

    variable type

    *)
  5. vrange : Mopsa_utils.Location.range;
    (*

    declaration location

    *)
}
and builtin =
  1. | PRIMED
  2. | LENGTH
  3. | INDEX
  4. | BYTES
  5. | OFFSET
  6. | BASE
  7. | VALID_FLOAT
  8. | FLOAT_INF
  9. | FLOAT_NAN
  10. | ALIVE
  11. | RESOURCE

Types

and c_qual_typ = c_typ * c_qual
and c_typ =
  1. | T_void
  2. | T_char
  3. | T_signed_char
  4. | T_unsigned_char
  5. | T_signed_short
  6. | T_unsigned_short
  7. | T_signed_int
  8. | T_unsigned_int
  9. | T_signed_long
  10. | T_unsigned_long
  11. | T_signed_long_long
  12. | T_unsigned_long_long
  13. | T_signed_int128
  14. | T_unsigned_int128
  15. | T_float
  16. | T_double
  17. | T_long_double
  18. | T_float128
  19. | T_array of c_qual_typ * array_length
  20. | T_struct of var
  21. | T_union of var
  22. | T_typedef of var
  23. | T_pointer of c_qual_typ
  24. | T_enum of var
  25. | T_unknown
and c_qual = {
  1. c_qual_const : bool;
  2. c_qual_volatile : bool;
  3. c_qual_restrict : bool;
}
and array_length =
  1. | A_no_length
  2. | A_constant_length of Z.t

Utility functions

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

val target_info : Mopsa_c_parser.Clang_AST.target_info Stdlib.ref
val compare_var : var -> var -> int
val compare_resource : resource -> resource -> int
val no_c_qual : c_qual
val const : c_qual
val volatile : c_qual
val restrict : c_qual
val is_c_qual_non_empty : c_qual -> bool
val merge_c_qual : c_qual -> c_qual -> c_qual

Pretty printers

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

val pp_var : Stdlib.Format.formatter -> var -> unit
val pp_resource : Stdlib.Format.formatter -> var -> unit
val pp_builtin : Stdlib.Format.formatter -> 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_expr : Stdlib.Format.formatter -> expr Mopsa_utils.Location.with_range -> unit
val pp_int_suffix : Stdlib.Format.formatter -> int_suffix -> 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 -> c_qual_typ -> unit
val pp_c_qual : Stdlib.Format.formatter -> c_qual -> unit
val pp_c_typ : Stdlib.Format.formatter -> c_typ -> 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_opt : ('a -> 'b -> unit) -> 'a -> 'b option -> 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 : Stdlib.Format.formatter -> leaf -> 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
val pp_stub : Stdlib.Format.formatter -> section list Mopsa_utils.Location.with_range -> unit
OCaml

Innovation. Community. Security.