mopsa 1.0 (latest) · OCaml Package

include sig ... end

val id : unit Core__Id.id

val name : string

val debug : ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a

val checks : Mopsa.check list

Initialization of environments

==============================

val init : 'a -> 'b -> 'c -> 'c

Command-line options

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

val opt_stub_ignored_cases : string list Stdlib.ref

List of ignored stub cases

val is_case_ignored : Ast.stub_func option -> Ast.case -> bool

Check whether a case is ignored

Evaluation of expressions

=========================

val negate_formula : 
  Ast.formula Mopsa.with_range ->
  Ast.formula Mopsa.with_range

Negate a formula

val formula_to_prenex : 
  Ast.formula Mopsa.with_range ->
  (Ast.quant * Mopsa.var * Ast.set) list * Mopsa.expr

Translate a formula into prenex normal form

val vars_of_condition : Mopsa.expr -> Mopsa.VarSet.t

val var_in_expr : Mopsa.var -> Ast.Expr.expr -> bool

val remove_unnecessary_quantifiers : 
  ('a * Mopsa.VarSet.elt * Ast.set) list ->
  Mopsa.expr ->
  ('a * Mopsa.var * Ast.set) list

val prenex_to_expr : 
  (Ast.quant * Mopsa.VarSet.elt * Ast.set) list ->
  Mopsa.expr ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Translate a prenex encoding (i.e. quantifiers and a condition) into an expression

val eval_formula : 
  (Mopsa.expr -> Mopsa.range -> Mopsa.stmt) ->
  Ast.formula Mopsa.with_range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Core.Post.post

Evaluate a formula

val init_params : 
  Ast.Expr.expr list ->
  Ast.Var.var list ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Core.Flow.flow

Initialize the parameters of the stubbed function

val remove_params : 
  Ast.Var.var list ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Core.Manager.man ->
  'a Core.Flow.flow ->
  'a Core.Flow.flow

Remove parameters from the returned flow

val exec_assumes : 
  Ast.formula Mopsa.with_range Mopsa.with_range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Core.Post.post

Evaluate the formula of the `assumes` section

val exec_local_new : 
  Ast.Var.var ->
  string ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Mopsa.post

Execute an allocation of a new resource

val exec_local_call : 
  Ast.Var.var ->
  Mopsa.expr ->
  Mopsa.expr list ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Core.Post.post

Execute a function call

val exec_local : 
  Ast.local Mopsa.with_range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Mopsa.post

Execute the `local` section

val exec_ensures : 
  Ast.formula Mopsa.with_range Mopsa.with_range ->
  Ast.Var.var option ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Core.Post.post

val exec_assigns : 
  Ast.assigns Mopsa.with_range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Core.Post.post

val clean_post : 
  Ast.local Mopsa.with_range list ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Core.Manager.man ->
  'a Core.Flow.flow ->
  'a Core.Flow.flow

Remove locals

val exec_free : 
  Mopsa.expr Mopsa.with_range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Core.Post.post

val exec_message : 
  Ast.message Mopsa.with_range ->
  ('a, 'b) Mopsa.man ->
  'a Mopsa.Flow.flow ->
  'a Mopsa.Post.post

val exec_leaf : 
  Ast.leaf ->
  Ast.Var.var option ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  'a Mopsa.post

Execute a leaf section

val exec_case : 
  Ast.case ->
  Ast.Var.var option ->
  ('a, 'b) Core.Manager.man ->
  'a Core.Flow.flow ->
  'a Mopsa.flow

Execute the body of a case section

val exec_body : 
  ?stub:Ast.stub_func option ->
  Ast.section list ->
  Ast.Var.var option ->
  'b ->
  ('a, 'c) Mopsa.man ->
  'a Mopsa.flow ->
  'a Mopsa.Flow.flow

Execute the body of a stub

val prepare_all_assigns : 
  Ast.assigns Mopsa.with_range list ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Core.Manager.man ->
  'a Core.Flow.flow ->
  'a Core.Flow.flow

val clean_all_assigns : 
  Ast.assigns Mopsa.with_range list ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Core.Manager.man ->
  'a Core.Flow.flow ->
  'a Core.Flow.flow

val eval_stub_call : 
  Ast.stub_func ->
  Ast.Expr.expr list ->
  Ast.Var.var option ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Mopsa.man ->
  'a Mopsa.Flow.flow ->
  'a Mopsa.Eval.eval

Evaluate a call to a stub

val eval_otherwise : 
  Ast.Expr.expr ->
  Ast.Expr.expr option ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  ('a, Ast.Expr.expr) Core.Cases.cases

Evaluate an otherwise expression

val discard_empty_quantification_intervals : 
  (Ast.quant * Ast.Var.var * Ast.set) list ->
  Mopsa.expr ->
  Mopsa_utils.Location.range ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  ('a, Ast.Expr.expr) Core.Cases.cases

val otherwise_in_condition : Mopsa.expr -> bool

Check if a condition contains an otherwise expression

val remove_new_checks : 
  'a Mopsa.Flow.flow ->
  'b Mopsa.Flow.flow ->
  'b Mopsa.Flow.flow

Remove newly introduced checks

val move_new_checks : 
  Mopsa_utils.Location.range ->
  'a Mopsa.Flow.flow ->
  'b Mopsa.Flow.flow ->
  'b Mopsa.Flow.flow

Move newly introduced checks to a new range

val eval : 
  Mopsa.expr ->
  ('a, 'b) Mopsa.man ->
  'a Mopsa.Flow.flow ->
  ('a, Ast.Expr.expr) Mopsa.Cases.cases option

Entry point of expression evaluations

Computation of post-conditions

==============================

val exec_directive : 
  Ast.stub_directive ->
  'a ->
  ('b, 'c) Core.Manager.man ->
  'b Core.Flow.flow ->
  'b Mopsa.Post.post

Execute a global stub directive

val normalize_requirement_condition : Mopsa.expr -> Mopsa.expr

Normalize a requirement condition by adding missing otherwise decorations

val exec_requires : 
  Mopsa.expr ->
  'a ->
  ('b, 'c) Mopsa.man ->
  'b Core.Flow.flow ->
  ('b, unit) Mopsa.Cases.cases

Check a stub requirement

val exec : 
  Mopsa.stmt ->
  ('a, 'b) Core.Manager.man ->
  'a Core.Flow.flow ->
  'a Mopsa.Post.post option

Handler of queries

==================

val ask : 'a -> 'b -> 'c -> 'd option

Pretty printer

==============

val print_expr : 'a -> 'b -> 'c -> 'd -> unit

package mopsa

Command-line options