mopsa 1.0 (latest) · OCaml Package

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.

type 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

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

and section =

| S_case of case
| S_leaf of leaf

and 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

and 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

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

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

}

and 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

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 = Cst.message_kind =

| WARN
| UNSOUND

Expressions

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

and 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

and expr = {

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

}

and log_binop = Cst.log_binop

and binop = Cst.binop

and unop = Cst.unop

and set =

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

and var = Mopsa_c_parser.C_AST.variable

and builtin = Cst.builtin

Formulas

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

and 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

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

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

val compare_resource : 'a -> 'a -> int

Pretty printers

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

val pp_var : Format.formatter -> Mopsa_c_parser.C_AST.variable -> unit

val pp_resource : Format.formatter -> string -> unit

val pp_builtin : Format.formatter -> Cst.builtin -> unit

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

val pp_opt : ('a -> 'b -> unit) -> 'a -> 'b option -> unit

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

val pp_unop : Format.formatter -> unop -> unit

val pp_binop : Format.formatter -> binop -> unit

val pp_c_qual_typ : Format.formatter -> Mopsa_c_parser.C_AST.type_qual -> unit

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

val pp_log_binop : Format.formatter -> log_binop -> unit

val pp_set : Format.formatter -> set -> unit

val pp_interval : Format.formatter -> interval -> unit

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

val pp_local_value : Format.formatter -> local_value -> unit

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

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

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

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

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

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

val pp_leaf_section : Format.formatter -> leaf -> unit

val pp_leaf_sections : Format.formatter -> leaf list -> unit

val pp_case : Format.formatter -> case -> unit

val pp_section : Format.formatter -> section -> unit

val pp_sections : Format.formatter -> section list -> unit