Module `Interproc.Domain`

Abstract state

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

module AddrSet : sig ... end

include module type of struct include AddrSet end

module Set = AddrSet.Set

type t = Set.t Mopsa_utils.Core.Top.with_top

val bottom : t

val top : t

val is_top : t -> bool

val subset : t -> t -> bool

val equal : t -> t -> bool

val compare : t -> t -> int

val join : t -> t -> t

val meet : t -> t -> t

val union : t -> t -> t

val inter : t -> t -> t

val diff : t -> t -> t

val print : Framework.Core.Print.printer -> t -> unit

val add : Set.elt -> t -> t

val fold : (Universal.Lang.Ast.Addr.t -> 'a -> 'a) -> t -> 'a -> 'a

val remove : Universal.Lang.Ast.Addr.t -> t -> t

val mem : Universal.Lang.Ast.Addr.t -> t -> bool

val filter : (Set.elt -> bool) -> t -> t

val partition : (Set.elt -> bool) -> t -> t * t

val exists : (Set.elt -> bool) -> t -> bool

val for_all : (Set.elt -> bool) -> t -> bool

val cardinal : t -> int

val find : Set.elt -> t -> Universal.Lang.Ast.Addr.t

val choose : t -> Universal.Lang.Ast.Addr.t

val singleton : Universal.Lang.Ast.Addr.t -> t

val of_list : 
  Universal.Lang.Ast.Addr.t list ->
  Set.t Mopsa_utils.Core.Top.with_top

val is_empty : t -> bool

val empty : t

val is_singleton : t -> bool

val elements : t -> Set.elt list

val map : (Universal.Lang.Ast.Addr.t -> Universal.Lang.Ast.Addr.t) -> t -> t

val iter : (Universal.Lang.Ast.Addr.t -> unit) -> t -> unit

val apply : (Set.t -> 'a) -> 'a -> t -> 'a

Domain header

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

include sig ... end

val id : t Mopsa_analyzer__Framework__Core__Id.id

val name : string

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

val checks : MopsaLib.check list

Lattice operators

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

val is_bottom : 'a -> bool

val widen : 'a -> t -> t -> t

val merge : 'a -> (t * 'b) -> (t * 'c) -> t

Initialization of environments

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

val init : 
  'a ->
  ('b, t) Framework.Core.Manager.man ->
  'b Core.Flow.flow ->
  'b Core.Post.post option

Computation of post-conditions

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

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

Evaluation of expressions

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

val is_recursive_call : 
  Lang.Ast.c_fundec ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.callstack ->
  bool

Check if there is a recursive call to a function

val is_local_scope : Lang.Ast.c_var_scope -> bool

val rename_variables_in_function_body : 
  MopsaLib.var list ->
  MopsaLib.callstack ->
  Framework.Core.Ast.Stmt.stmt ->
  Framework.Core.Ast.Stmt.stmt

Rename the variables of a function's body by attaching the callstack to them

val rename_variables_in_stub : 
  MopsaLib.var list ->
  MopsaLib.callstack ->
  Stubs.Ast.stub_func ->
  Stubs.Ast.stub_func

Rename local variables in a stub body by attaching the callstack to them

val rename_variables_in_fundec : 
  MopsaLib.callstack ->
  Lang.Ast.c_fundec ->
  Lang.Ast.c_fundec

Rename the variables of a function by attaching the callstack to them

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

𝔼⟦ alloca(size) ⟧

val eval_calls_in_args : 
  string ->
  int ->
  Framework.Core.Ast.Expr.expr list ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, Framework.Core.Ast.Expr.expr list) Core.Cases.cases

Evaluate arguments containing function calls

val is_c_fun_boolean_predicate : 
  Lang.Ast.c_fundec ->
  MopsaLib.expr list ->
  'a ->
  'b ->
  bool

val is_c_constant : MopsaLib.expr -> bool

val eval_call : 
  Lang.Ast.c_fundec ->
  Framework.Core.Ast.Expr.expr list ->
  Mopsa_utils.Core.Location.range ->
  ('a, t) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, Framework.Core.Ast.Expr.expr) Mopsa_analyzer.MopsaLib.Cases.cases

Eval a function call

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

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

Handler of queries

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

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

Pretty printer

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

val print_state : MopsaLib.printer -> t -> unit

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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Iterators/Interproc/Domain/index.html

Module `Interproc.Domain`

Abstract state

Domain header

Lattice operators

Initialization of environments

Computation of post-conditions

Evaluation of expressions

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Iterators/Interproc/Domain/index.html

Module Interproc.Domain

Abstract state

Domain header

Lattice operators

Initialization of environments

Computation of post-conditions

Evaluation of expressions

dune-project
Dependency

Module `Interproc.Domain`