Module `Body.Domain`

include sig ... end

val id : unit Mopsa_analyzer__Framework__Core__Id.id

val name : string

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

val checks : MopsaLib.check list

Initialization of environments

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

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

Command-line options

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

val opt_stub_ignored_cases : string list ref

List of ignored stub cases

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

Check whether a case is ignored

Evaluation of expressions

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

val negate_formula : 
  Stubs.Ast.formula MopsaLib.with_range ->
  Stubs.Ast.formula MopsaLib.with_range

Negate a formula

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

Translate a formula into prenex normal form

val vars_of_condition : MopsaLib.expr -> Mopsa_analyzer.MopsaLib.VarSet.t

val var_in_expr : MopsaLib.var -> Framework.Core.Ast.Expr.expr -> bool

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

val prenex_to_expr : 
  (Stubs.Ast.quant * Mopsa_analyzer.MopsaLib.VarSet.elt * Stubs.Ast.set) list ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

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

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

Evaluate a formula

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

Initialize the parameters of the stubbed function

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

Remove parameters from the returned flow

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

Evaluate the formula of the `assumes` section

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

Execute an allocation of a new resource

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

Execute a function call

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

Execute the `local` section

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

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

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

Remove locals

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

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

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

Execute a leaf section

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

Execute the body of a case section

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

Execute the body of a stub

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

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

val eval_stub_call : 
  Stubs.Ast.stub_func ->
  Framework.Core.Ast.Expr.expr list ->
  Framework.Core.Ast.Var.var option ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow ->
  ('a, Framework.Core.Ast.Expr.expr) Core.Cases.cases

Evaluate a call to a stub

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

Evaluate an otherwise expression

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

val otherwise_in_condition : MopsaLib.expr -> bool

Check if a condition contains an otherwise expression

val remove_new_checks : 
  'a Mopsa_analyzer.MopsaLib.Flow.flow ->
  'b Mopsa_analyzer.MopsaLib.Flow.flow ->
  'b Mopsa_analyzer.MopsaLib.Flow.flow

Remove newly introduced checks

val move_new_checks : 
  Mopsa_utils.Core.Location.range ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow ->
  'b Mopsa_analyzer.MopsaLib.Flow.flow ->
  'b Mopsa_analyzer.MopsaLib.Flow.flow

Move newly introduced checks to a new range

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

Entry point of expression evaluations

Computation of post-conditions

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

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

Execute a global stub directive

val normalize_requirement_condition : MopsaLib.expr -> MopsaLib.expr

Normalize a requirement condition by adding missing otherwise decorations

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

Check a stub requirement

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

Handler of queries

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

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

Pretty printer

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

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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/Stubs/Body/Domain/index.html

Module `Body.Domain`

Command-line options

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/Stubs/Body/Domain/index.html

Module Body.Domain

Command-line options

dune-project
Dependency

Module `Body.Domain`