Module `Parsing.Ast`Source

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.

Sourcetype stub = {

stub_name : string;
stub_params : var list;
stub_locals : local Mopsa_utils.Location.with_range list;
stub_assigns : assigns Mopsa_utils.Location.with_range list;
stub_body : section list;
stub_range : Mopsa_utils.Location.range;

}

Stub sections

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

Sourceand section =

| S_case of case
| 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;
case_locals : local Mopsa_utils.Location.with_range list;
case_assigns : assigns Mopsa_utils.Location.with_range list;
case_range : Mopsa_utils.Location.range;

}

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;
lval : local_value;

}

Sourceand local_value =

| L_new of resource
| L_call of Mopsa_c_parser.C_AST.func 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 = Cst.message_kind =

| WARN
| UNSOUND

Expressions

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

Sourceand expr_kind =

| E_top of Mopsa_c_parser.C_AST.type_qual
| E_int of Z.t
| 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 Mopsa_c_parser.C_AST.type_qual * bool * 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 * int * string
| E_arrow of expr Mopsa_utils.Location.with_range * int * 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_return

Sourceand expr = {

kind : expr_kind;
typ : Mopsa_c_parser.C_AST.type_qual;

}

Sourceand log_binop = Cst.log_binop

Sourceand binop = Cst.binop

Sourceand unop = Cst.unop

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 = string

Sourceand var = Mopsa_c_parser.C_AST.variable

Sourceand builtin = Cst.builtin

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 * set * formula Mopsa_utils.Location.with_range
| F_exists of var * 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

Utility functions

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

Source

val compare_var : 
  Mopsa_c_parser.C_AST.variable ->
  Mopsa_c_parser.C_AST.variable ->
  int

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

Source

val 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

Source

val 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

Source

val pp_c_qual_typ : 
  Stdlib.Format.formatter ->
  Mopsa_c_parser.C_AST.type_qual ->
  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

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_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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/parsing/Parsing/Ast/index.html

Module `Parsing.Ast`Source

Stub sections

Leaf sections

Expressions

Formulas

Utility functions

Pretty printers

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/parsing/Parsing/Ast/index.html

Module Parsing.AstSource

Stub sections

Leaf sections

Expressions

Formulas

Utility functions

Pretty printers

Module `Parsing.Ast`Source