package mopsa

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Stub sections
Stub leaf sections
Formulas
Expressions
Types
Utility functions
Pretty printers

package mopsa

Legend:
Library
Module
Module type
Parameter
Class
Class type

Concrete syntax tree for C stubs

type stub = section list Mopsa_utils.Location.with_range

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

and section =

and leaf =

and case = {

case_label : string;
case_body : leaf list;

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

and requires = formula Mopsa_utils.Location.with_range

and ensures = formula Mopsa_utils.Location.with_range

and assumes = formula Mopsa_utils.Location.with_range

and local = {

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

and local_value =

and assigns = {

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

and free = expr Mopsa_utils.Location.with_range

and message = {

message_kind : message_kind;
message_body : string;

and message_kind =

| WARN
| UNSOUND

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

and formula =

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

and expr =

and int_suffix =

| NO_SUFFIX
| LONG
| UNSIGNED_LONG
| LONG_LONG
| UNSIGNED_LONG_LONG

and log_binop =

| AND
| OR
| IMPLIES

and binop =

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

and unop =

| PLUS
| MINUS
| LNOT
| BNOT

| S_interval of interval
| S_resource of resource

and 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
*)

and resource = var

and 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
*)

and builtin =

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

and c_qual_typ = c_typ * c_qual

and 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

and c_qual = {

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

and array_length =

| A_no_length
| A_constant_length of Z.t

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

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

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

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

package mopsa

Stub sections

Stub leaf sections

Formulas

Expressions

Types

Utility functions

Pretty printers