Module `Domain.Make`Source

Parameters

module ApronManager : Apron_manager.APRONMANAGER

Signature

include sig ... end

Sourceval with_context : 'a -> 'b -> 'b * 'a

Sourceval is_numerical_var : Mopsa.var -> bool

Sourceval empty_env : Apron.Environment.t

Sourceval print_env : Stdlib.Format.formatter -> Apron.Environment.t -> unit

Source

val filter_env : 
  (Apron.Var.t -> bool) ->
  (Apron.Var.t -> bool) ->
  Apron.Environment.t ->
  Apron.Environment.t

Sourceval fold_env : (Apron.Var.t -> 'a -> 'a) -> Apron.Environment.t -> 'a -> 'a

Sourceval exists_env : (Apron.Var.t -> bool) -> Apron.Environment.t -> bool

Sourceval gce : Apron.Environment.t -> Apron.Environment.t -> Apron.Environment.t

Sourceval diff : Apron.Environment.t -> Apron.Environment.t -> Apron.Environment.t

Source

val to_constraints : 
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  ((Apron.Coeff.t * Mopsa.var) list * Apron.Coeff.t * Apron.Lincons1.typ) list

Source

val constraints_of_var : 
  Mopsa.var ->
  ((Apron.Coeff.t * Mopsa.var) list * 'a * 'b) list ->
  ((Apron.Coeff.t * Mopsa.var) list * 'a * 'b) list

Source

val related_vars : 
  Mopsa.var ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Mopsa.var list

Source

val constant_vars : 
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Mopsa.var list

Source

val all_related_vars : 
  Mopsa.VarSet.elt ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Mopsa.VarSet.elt list

Sourceexception UnsupportedExpression

Sourceexception ImpreciseExpression

Sourceval binop_to_apron : Mopsa.operator -> Apron.Texpr1.binop

Sourceval typ_to_apron : Mopsa.typ -> Apron.Texpr1.typ

Sourceval is_env_var : Mopsa.var -> ('a Apron.Abstract1.t * Binding.t) -> bool

Sourceval is_env_var_apron : Apron.Var.t -> 'a Apron.Abstract1.t -> bool

Source

val remove_tmp : 
  Apron.Var.t list ->
  ApronManager.t Apron.Abstract1.t ->
  ApronManager.t Apron.Abstract1.t

Source

val exp_to_apron : 
  (Mopsa.expr -> bool) ->
  Mopsa.expr ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Apron.Var.t list ->
  Apron.Texpr1.expr
  * ApronManager.t Apron.Abstract1.t
  * Binding.t
  * Apron.Var.t list

Source

val bexp_to_apron : 
  (Mopsa.expr -> bool) ->
  Mopsa.expr ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Apron.Var.t list ->
  (Apron.Tcons1.typ
   * Apron.Texpr1.expr
   * Ast.Typ.typ
   * Apron.Texpr1.expr
   * Ast.Typ.typ)
    Mopsa.Dnf.t
  * ApronManager.t Apron.Abstract1.t
  * Binding.t
  * Apron.Var.t list

Source

val tcons_array_of_tcons_list : 
  Apron.Environment.t ->
  Apron.Tcons1.t list ->
  Apron.Tcons1.earray

Sourcetype t = ApronManager.t Apron.Abstract1.t * Binding.t

Bindings between Mopsa and Apron variables

include sig ... end

val id : t Core__Id.id

val name : string

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

Sourceval numeric_name : string

Environment utility functions

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

Source

val unify : 
  ApronManager.t Apron.Abstract1.t ->
  ApronManager.t Apron.Abstract1.t ->
  ApronManager.t Apron.Abstract1.t * ApronManager.t Apron.Abstract1.t * bool

Source

val add_missing_vars : 
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Mopsa.var list ->
  ApronManager.t Apron.Abstract1.t * Binding.t

Source

val print_state : 
  Mopsa.printer ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  unit

Lattice operators

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

Sourceval top : ApronManager.t Apron.Abstract1.t * Binding.t

Sourceval bottom : ApronManager.t Apron.Abstract1.t * Binding.t

Sourceval is_bottom : (ApronManager.t Apron.Abstract1.t * 'a) -> bool

Source

val subset : 
  (ApronManager.t Apron.Abstract1.t * 'a) ->
  (ApronManager.t Apron.Abstract1.t * 'b) ->
  bool

Source

val join : 
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  ApronManager.t Apron.Abstract1.t * Binding.Equiv.t

Source

val meet : 
  (ApronManager.t Apron.Abstract1.t * Binding.Equiv.t) ->
  (ApronManager.t Apron.Abstract1.t * Binding.Equiv.t) ->
  ApronManager.t Apron.Abstract1.t * Binding.Equiv.t

Source

val widen : 
  'a ->
  (ApronManager.t Apron.Abstract1.t * Binding.Equiv.t) ->
  (ApronManager.t Apron.Abstract1.t * Binding.Equiv.t) ->
  ApronManager.t Apron.Abstract1.t * Binding.Equiv.t

Transfer functions

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

Sourceval init : 'a -> ApronManager.t Apron.Abstract1.t * Binding.t

Source

val remove_var : 
  Mopsa.var ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  ApronManager.t Apron.Abstract1.t * Binding.Equiv.t

Source

val forget_var : 
  Mopsa.var ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  ApronManager.t Apron.Abstract1.t * Binding.t

Source

val bound_var : 
  Mopsa.var ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Numeric_values.Values.Intervals.Integer.Value.t

Sourceval is_var_numeric_type : Mopsa.var -> bool

Source

val assume : 
  Mopsa.stmt ->
  (('a, bool) Core.Query.query -> bool) ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) option

Source

val merge : 
  ('a * 'b) ->
  ((ApronManager.t Apron.Abstract1.t * Binding.Equiv.t) * Mopsa.change) ->
  ((ApronManager.t Apron.Abstract1.t * Binding.Equiv.t) * Mopsa.change) ->
  ApronManager.t Apron.Abstract1.t * Binding.Equiv.t

Source

val enforce_sign_constraint : 
  Core.All.var ->
  (('a, bool) Core.Query.query -> bool) ->
  'b Core.All.ctx ->
  Mopsa.range ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) option ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) option

Add the sign contraint (if existing) of a given variable into the relationnal domain

Source

val exec : 
  Mopsa.stmt ->
  ('a, 'b) Mopsa.Sig.Abstraction.Simplified.simplified_man ->
  'c Core.All.ctx ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) option

Sourceval vars : ('a Apron.Abstract1.t * Binding.t) -> Mopsa.var list

Source

val eval_interval : 
  ('a, 'b) Mopsa.Sig.Abstraction.Simplified.simplified_man ->
  Mopsa.expr ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Mopsa.ItvUtils.IntItv.t_with_bot option

Source

val ask : 
  'r. ('a, 'r) Mopsa.query ->
  ('a, t) Mopsa.Sig.Abstraction.Simplified.simplified_man ->
  'a Mopsa.ctx ->
  t ->
  'r option

Source

val print_expr : 
  ('a, 'b) Mopsa.Sig.Abstraction.Simplified.simplified_man ->
  'c Core.All.ctx ->
  (ApronManager.t Apron.Abstract1.t * Binding.t) ->
  Mopsa.printer ->
  Ast.Expr.expr ->
  unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/relational/Relational/Domain/Make/index.html

Module `Domain.Make`Source

Parameters

Signature

Environment utility functions

Lattice operators

Transfer functions

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/relational/Relational/Domain/Make/index.html

Module Domain.MakeSource

Parameters

Signature

Environment utility functions

Lattice operators

Transfer functions

Module `Domain.Make`Source