Module `Body.Domain`Source

include sig ... end

val id : unit Core__Id.id

val name : string

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

Sourceval checks : Mopsa.check list

Initialization of environments

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

Sourceval init : 'a -> 'b -> 'c -> 'd option

Command-line options

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

Sourceval opt_stub_ignored_cases : string list Stdlib.ref

List of ignored stub cases

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

Check whether a case is ignored

Evaluation of expressions

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

Source

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

Negate a formula

Source

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

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

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

Source

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

Source

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

Source

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

Source

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

Initialize the parameters of the stubbed function

Source

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

Remove parameters from the returned flow

Source

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

Source

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

Source

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

Source

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

Execute the `local` section

Source

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

Source

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

Source

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

Remove locals

Source

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

Source

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

Source

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

Execute a leaf section

Source

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

Execute the body of a case section

Source

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

Execute the body of a stub

Source

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

Source

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

Source

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, Ast.Expr.expr) Core.Cases.cases

Evaluate a call to a stub

Source

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

Source

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

Sourceval otherwise_in_condition : Mopsa.expr -> bool

Check if a condition contains an otherwise expression

Source

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

Remove newly introduced checks

Source

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

Source

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

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

Source

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

Execute a global stub directive

Sourceval normalize_requirement_condition : Mopsa.expr -> Mopsa.expr

Normalize a requirement condition by adding missing otherwise decorations

Source

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

Check a stub requirement

Source

val exec : 
  Mopsa.stmt ->
  ('a, 'b) Mopsa.man ->
  'a Core.Flow.flow ->
  ('a, unit) Core.Cases.cases option

Handler of queries

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

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

Pretty printer

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

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/stubs/Stubs/Body/Domain/index.html

Module `Body.Domain`Source

Command-line options

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/stubs/Stubs/Body/Domain/index.html

Module Body.DomainSource

Command-line options

Module `Body.Domain`Source