Module `Stubs.Ast`Source

Abstract Syntax Tree for stub specification. Similar to the AST of the parser, except for expressions, types and variables for which MOPSA counterparts are used.

Sourcetype stub_func = {

stub_func_name : string;
stub_func_body : section list;
stub_func_params : Mopsa.var list;
stub_func_locals : local Mopsa.with_range list;
stub_func_assigns : assigns Mopsa.with_range list;
stub_func_return_type : Mopsa.typ option;
stub_func_range : Mopsa.range;

}

Stub for a function

Sourceand stub_directive = {

stub_directive_body : section list;
stub_directive_locals : local Mopsa.with_range list;
stub_directive_assigns : assigns Mopsa.with_range list;
stub_directive_range : Mopsa.range;

}

Stub for a global directive

Stub sections

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

Sourceand section =

| S_case of case
| S_leaf of leaf

Sourceand leaf =

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

Sourceand case = {

case_label : string;
case_body : leaf list;
case_locals : local Mopsa.with_range list;
case_assigns : assigns Mopsa.with_range list;
case_range : Mopsa.range;

}

Leaf sections

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

Sourceand requires = formula Mopsa.with_range

Sourceand ensures = formula Mopsa.with_range

Sourceand assumes = formula Mopsa.with_range

Sourceand local = {

lvar : Mopsa.var;
lval : local_value;

}

Sourceand local_value =

| L_new of resource
| L_call of Mopsa.expr * Mopsa.expr list

Sourceand assigns = {

assign_target : Mopsa.expr;
assign_offset : interval list;

}

Sourceand free = Mopsa.expr

Sourceand message = {

message_kind : message_kind;
message_body : string;

}

Sourceand message_kind =

| WARN
| UNSOUND

Sourceand log_binop = Mopsa_c_stubs_parser.Cst.log_binop =

| AND
| OR
| IMPLIES

Sourceand set =

| S_interval of interval
| S_resource of resource

Sourceand interval = Mopsa.expr * Mopsa.expr

Sourceand resource = Mopsa_c_stubs_parser.Ast.resource

Sourceand builtin = Mopsa_c_stubs_parser.Ast.builtin

Formulas

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

Sourceand formula =

| F_expr of Mopsa.expr
| F_binop of log_binop * formula Mopsa.with_range * formula Mopsa.with_range
| F_not of formula Mopsa.with_range
| F_forall of Mopsa.var * set * formula Mopsa.with_range
| F_exists of Mopsa.var * set * formula Mopsa.with_range
| F_in of Mopsa.expr * set
| F_otherwise of formula Mopsa.with_range * Mopsa.expr
| F_if of formula Mopsa.with_range * formula Mopsa.with_range * formula Mopsa.with_range

Sourceval compare_assigns : assigns -> assigns -> int

Sourceval compare_resource : 'a -> 'a -> int

Sourceval compare_set : set -> set -> int

Source

val compare_formula : 
  formula Mopsa.with_range ->
  formula Mopsa.with_range ->
  int

Expressions

Sourcetype quant =

| FORALL
| EXISTS

Quantifiers

Sourcetype Mopsa.expr_kind +=

| E_stub_call of stub_func * Mopsa.expr list
(*
arguments
*)
| E_stub_return
(*
Returned value of a stub
*)
| E_stub_builtin_call of builtin * Mopsa.expr list
(*
Call to a built-in function
*)
| E_stub_attribute of Mopsa.expr * string
(*
Access to an attribute of a resource
*)
| E_stub_alloc of string * Mopsa.mode
(*
strong or weak
*)
| E_stub_resource_mem of Mopsa.expr * resource
(*
Filter environments in which an instance is in a resource pool
*)
| E_stub_primed of Mopsa.expr
(*
Primed expressions denoting values in the post-state
*)
| E_stub_quantified_formula of (quant * Mopsa.var * set) list * Mopsa.expr
(*
Quantifier-free formula
*)
| E_stub_otherwise of Mopsa.expr * Mopsa.expr option
(*
alarm
*)
| E_stub_raise of string
(*
message
*)
| E_stub_if of Mopsa.expr * Mopsa.expr * Mopsa.expr
(*
else
*)

Conditional stub expression

Statements

Sourcetype Mopsa.stmt_kind +=

| S_stub_directive of stub_directive
(*
A call to a stub directive, which are stub functions called at the initialization of the analysis. Useful to initialize variables with stub formulas.
*)
| S_stub_free of Mopsa.expr
(*
Release a resource
*)
| S_stub_requires of Mopsa.expr
(*
Filter the current environments that verify a condition, and raise an alarm if the condition may be violated.
*)
| S_stub_prepare_all_assigns of assigns list
(*
Prepare primed copies of assigned objects
*)
| S_stub_assigns of assigns
(*
Declare an assigned object
*)
| S_stub_clean_all_assigns of assigns list
(*
Clean the post-state of primed copies
*)

Heap addresses for resources

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

Sourcetype Mopsa.addr_kind +=

| A_stub_resource of string
(*
resource address
*)

Utility functions

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

Source

val mk_stub_call : 
  stub_func ->
  Mopsa.expr list ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_stub_builtin_call : 
  builtin ->
  Mopsa.expr list ->
  etyp:Ast.Typ.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_stub_resource_mem : 
  Mopsa.expr ->
  resource ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Sourceval mk_stub_primed : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr

Source

val mk_stub_directive : 
  stub_directive ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Sourceval mk_stub_free : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.stmt

Source

val mk_stub_prepare_all_assigns : 
  assigns Mopsa.with_range list ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Source

val mk_stub_assigns : 
  Mopsa.expr ->
  interval list ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Source

val mk_stub_clean_all_assigns : 
  assigns Mopsa.with_range list ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Sourceval mk_stub_requires : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.stmt

Source

val mk_stub_quantified_formula : 
  ?etyp:Mopsa.typ ->
  (quant * Mopsa.var * set) list ->
  Mopsa.expr ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_stub_otherwise : 
  Mopsa.expr ->
  Mopsa.expr option ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_stub_if : 
  Mopsa.expr ->
  Mopsa.expr ->
  Mopsa.expr ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Sourceval is_stub_primed : Ast.Expr.expr -> bool

Sourceval find_var_quantifier : Mopsa.var -> ('a * Mopsa.var * 'b) list -> 'a * 'b

Source

val find_var_quantifier_opt : 
  Mopsa.var ->
  ('a * Mopsa.var * 'b) list ->
  ('a * 'b) option

Sourceval is_quantified_var : Mopsa.var -> ('a * Mopsa.var * 'b) list -> bool

Source

val is_forall_quantified_var : 
  Mopsa.var ->
  (quant * Mopsa.var * 'a) list ->
  bool

Source

val is_exists_quantified_var : 
  Mopsa.var ->
  (quant * Mopsa.var * 'a) list ->
  bool

Source

val find_quantified_var_interval : 
  Mopsa.var ->
  ('a * Mopsa.var * set) list ->
  Mopsa.expr * Mopsa.expr

Source

val find_quantified_var_interval_opt : 
  Mopsa.var ->
  ('a * Mopsa.var * set) list ->
  (Mopsa.expr * Mopsa.expr) option

Source

val negate_stub_quantified_formula : 
  (quant * 'a * 'b) list ->
  Mopsa.expr ->
  (quant * 'a * 'b) list * Mopsa.expr

Source

val visit_expr_in_formula : 
  (Ast.Expr.expr -> Ast.Expr.expr Mopsa.Visitor.visit_action) ->
  formula Mopsa.with_range ->
  formula Mopsa.with_range

Visit expressions present in a formula

Source

val visit_set : 
  (Ast.Expr.expr -> Ast.Expr.expr Mopsa.Visitor.visit_action) ->
  set ->
  set

Source

val visit_expr : 
  (Ast.Expr.expr -> Ast.Expr.expr Mopsa.Visitor.visit_action) ->
  Mopsa.expr ->
  Mopsa.expr

Source

val mk_stub_alloc_resource : 
  ?mode:Mopsa.mode ->
  string ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Sourceval negate_log_binop : log_binop -> log_binop

Pretty printers

=-=-=-=-=-=-=-=-=-=

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

Source

val pp_log_binop : 
  Stdlib.Format.formatter ->
  Mopsa_c_stubs_parser.Ast.log_binop ->
  unit

Sourceval pp_quantifier : Stdlib.Format.formatter -> quant -> unit

Sourceval pp_formula : Stdlib.Format.formatter -> formula Mopsa.with_range -> unit

Sourceval pp_set : Stdlib.Format.formatter -> set -> unit

Sourceval pp_interval : Stdlib.Format.formatter -> interval -> unit

Sourceval pp_resource : Stdlib.Format.formatter -> resource -> 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

Sourceval pp_local : Stdlib.Format.formatter -> local Mopsa.with_range -> unit

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

Source

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

Sourceval pp_assigns : Stdlib.Format.formatter -> assigns Mopsa.with_range -> unit

Sourceval pp_assumes : Stdlib.Format.formatter -> assumes Mopsa.with_range -> unit

Source

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

Sourceval pp_free : Stdlib.Format.formatter -> Mopsa.expr Mopsa.with_range -> unit

Sourceval pp_message : Stdlib.Format.formatter -> message Mopsa.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

Sourceval pp_stub_func : Stdlib.Format.formatter -> stub_func -> unit

Sourceval pp_stub_directive : Stdlib.Format.formatter -> stub_directive -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/stubs/Stubs/Ast/index.html

Module `Stubs.Ast`Source

Stub sections

Leaf sections

Formulas

Expressions

Statements

Heap addresses for resources

Utility functions

Pretty printers

Registration of expressions

Registration of statements

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/stubs/Stubs/Ast/index.html

Module Stubs.AstSource

Stub sections

Leaf sections

Formulas

Expressions

Statements

Heap addresses for resources

Utility functions

Pretty printers

Registration of expressions

Registration of statements

Module `Stubs.Ast`Source