Module `Parsing.Cst`Source

Concrete syntax tree for C stubs

Sourcetype stub = section list Mopsa_utils.Location.with_range

Stub sections

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

Sourceand section =

| S_case of case Mopsa_utils.Location.with_range
| S_leaf of leaf

Sourceand leaf =

| S_local of local Mopsa_utils.Location.with_range
| S_assumes of assumes Mopsa_utils.Location.with_range
| S_requires of requires Mopsa_utils.Location.with_range
| S_assigns of assigns Mopsa_utils.Location.with_range
| S_ensures of ensures Mopsa_utils.Location.with_range
| S_free of free Mopsa_utils.Location.with_range
| S_message of message Mopsa_utils.Location.with_range

Sourceand case = {

case_label : string;
case_body : leaf list;

}

Stub leaf sections

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

Sourceand requires = formula Mopsa_utils.Location.with_range

Sourceand ensures = formula Mopsa_utils.Location.with_range

Sourceand assumes = formula Mopsa_utils.Location.with_range

Sourceand local = {

lvar : var;
ltyp : c_qual_typ;
lval : local_value;

}

Sourceand local_value =

| L_new of resource
| L_call of var Mopsa_utils.Location.with_range * expr Mopsa_utils.Location.with_range list

Sourceand assigns = {

assign_target : expr Mopsa_utils.Location.with_range;
assign_offset : interval list;

}

Sourceand free = expr Mopsa_utils.Location.with_range

Sourceand message = {

message_kind : message_kind;
message_body : string;

}

Sourceand message_kind =

| WARN
| UNSOUND

Formulas

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

Sourceand formula =

| F_expr of expr Mopsa_utils.Location.with_range
| F_bool of bool
| F_binop of log_binop * formula Mopsa_utils.Location.with_range * formula Mopsa_utils.Location.with_range
| F_not of formula Mopsa_utils.Location.with_range
| F_forall of var * c_qual_typ * set * formula Mopsa_utils.Location.with_range
| F_exists of var * c_qual_typ * set * formula Mopsa_utils.Location.with_range
| F_in of expr Mopsa_utils.Location.with_range * set
| F_otherwise of formula Mopsa_utils.Location.with_range * expr Mopsa_utils.Location.with_range
| F_if of formula Mopsa_utils.Location.with_range * formula Mopsa_utils.Location.with_range * formula Mopsa_utils.Location.with_range

Expressions

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

Sourceand expr =

| E_top of c_qual_typ
| E_int of Z.t * int_suffix
| E_float of float
| E_string of string
| E_char of int
| E_invalid
| E_var of var
| E_unop of unop * expr Mopsa_utils.Location.with_range
| E_binop of binop * expr Mopsa_utils.Location.with_range * expr Mopsa_utils.Location.with_range
| E_addr_of of expr Mopsa_utils.Location.with_range
| E_deref of expr Mopsa_utils.Location.with_range
| E_cast of c_qual_typ * expr Mopsa_utils.Location.with_range
| E_subscript of expr Mopsa_utils.Location.with_range * expr Mopsa_utils.Location.with_range
| E_member of expr Mopsa_utils.Location.with_range * string
| E_arrow of expr Mopsa_utils.Location.with_range * string
| E_conditional of expr Mopsa_utils.Location.with_range * expr Mopsa_utils.Location.with_range * expr Mopsa_utils.Location.with_range
| E_builtin_call of builtin * expr Mopsa_utils.Location.with_range list
| E_raise of string
| E_sizeof_type of c_qual_typ Mopsa_utils.Location.with_range
| E_sizeof_expr of expr Mopsa_utils.Location.with_range
| E_return

Sourceand int_suffix =

| NO_SUFFIX
| LONG
| UNSIGNED_LONG
| LONG_LONG
| UNSIGNED_LONG_LONG

Sourceand log_binop =

| AND
| OR
| IMPLIES

Sourceand binop =

| ADD
| SUB
| MUL
| DIV
| MOD
| RSHIFT
| LSHIFT
| LOR
| LAND
| LT
| LE
| GT
| GE
| EQ
| NEQ
| BOR
| BAND
| BXOR

Sourceand unop =

| PLUS
| MINUS
| LNOT
| BNOT

Sourceand set =

| S_interval of interval
| S_resource of resource

Sourceand interval = {

itv_lb : expr Mopsa_utils.Location.with_range;
(*
lower bound
*)
itv_open_lb : bool;
(*
open lower bound
*)
itv_ub : expr Mopsa_utils.Location.with_range;
(*
upper bound
*)
itv_open_ub : bool;
(*
open upper bound
*)

}

Sourceand resource = var

Sourceand var = {

vname : string;
(*
variable name
*)
vlocal : bool;
(*
is it a local variable ?
*)
vuid : int;
(*
unique identifier
*)
vtyp : c_qual_typ;
(*
variable type
*)
vrange : Mopsa_utils.Location.range;
(*
declaration location
*)

}

Sourceand builtin =

| PRIMED
| LENGTH
| INDEX
| BYTES
| OFFSET
| BASE
| VALID_FLOAT
| FLOAT_INF
| FLOAT_NAN
| ALIVE
| RESOURCE

Types

Sourceand c_qual_typ = c_typ * c_qual

Sourceand c_typ =

| T_void
| T_char
| T_signed_char
| T_unsigned_char
| T_signed_short
| T_unsigned_short
| T_signed_int
| T_unsigned_int
| T_signed_long
| T_unsigned_long
| T_signed_long_long
| T_unsigned_long_long
| T_signed_int128
| T_unsigned_int128
| T_float
| T_double
| T_long_double
| T_float128
| T_array of c_qual_typ * array_length
| T_struct of var
| T_union of var
| T_typedef of var
| T_pointer of c_qual_typ
| T_enum of var
| T_unknown

Sourceand c_qual = {

c_qual_const : bool;
c_qual_volatile : bool;
c_qual_restrict : bool;

}

Sourceand array_length =

| A_no_length
| A_constant_length of Z.t

Utility functions

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

Sourceval target_info : Mopsa_c_parser.Clang_AST.target_info Stdlib.ref

Sourceval compare_var : var -> var -> int

Sourceval compare_resource : resource -> resource -> int

Sourceval no_c_qual : c_qual

Sourceval const : c_qual

Sourceval volatile : c_qual

Sourceval restrict : c_qual

Sourceval is_c_qual_non_empty : c_qual -> bool

Sourceval merge_c_qual : c_qual -> c_qual -> c_qual

Pretty printers

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

Sourceval pp_var : Stdlib.Format.formatter -> var -> unit

Sourceval pp_resource : Stdlib.Format.formatter -> var -> unit

Sourceval pp_builtin : Stdlib.Format.formatter -> builtin -> unit

Source

val pp_list : 
  (Stdlib.Format.formatter -> 'a -> unit) ->
  (unit, Stdlib.Format.formatter, unit) Stdlib.format ->
  Stdlib.Format.formatter ->
  'a list ->
  unit

Source

val pp_expr : 
  Stdlib.Format.formatter ->
  expr Mopsa_utils.Location.with_range ->
  unit

Sourceval pp_int_suffix : Stdlib.Format.formatter -> int_suffix -> 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 -> c_qual_typ -> unit

Sourceval pp_c_qual : Stdlib.Format.formatter -> c_qual -> unit

Sourceval pp_c_typ : Stdlib.Format.formatter -> c_typ -> unit

Source

val 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_opt : ('a -> 'b -> unit) -> 'a -> 'b option -> unit

Source

val pp_local : 
  Stdlib.Format.formatter ->
  local Mopsa_utils.Location.with_range ->
  unit

Sourceval pp_local_value : Stdlib.Format.formatter -> local_value -> unit

Source

val pp_requires : 
  Stdlib.Format.formatter ->
  formula Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range ->
  unit

Source

val pp_assigns : 
  Stdlib.Format.formatter ->
  assigns Mopsa_utils.Location.with_range ->
  unit

Source

val pp_assumes : 
  Stdlib.Format.formatter ->
  assumes Mopsa_utils.Location.with_range ->
  unit

Source

val pp_ensures : 
  Stdlib.Format.formatter ->
  formula Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range ->
  unit

Source

val pp_free : 
  Stdlib.Format.formatter ->
  expr Mopsa_utils.Location.with_range Mopsa_utils.Location.with_range ->
  unit

Source

val pp_message : 
  Stdlib.Format.formatter ->
  message Mopsa_utils.Location.with_range ->
  unit

Sourceval pp_leaf : Stdlib.Format.formatter -> leaf -> 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

Source

val pp_stub : 
  Stdlib.Format.formatter ->
  section list Mopsa_utils.Location.with_range ->
  unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/parsing/Parsing/Cst/index.html

Module `Parsing.Cst`Source

Stub sections

Stub leaf sections

Formulas

Expressions

Types

Utility functions

Pretty printers

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/parsing/Parsing/Cst/index.html

Module Parsing.CstSource

Stub sections

Stub leaf sections

Formulas

Expressions

Types

Utility functions

Pretty printers

Module `Parsing.Cst`Source