package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Library
Module
Module type
Parameter
Class
Class type

Utility functions for formula creation

type stats = {
  1. var : int;
  2. cst : int;
  3. unop : int;
  4. bnop : int;
  5. comp : int;
  6. select : int;
  7. store : int;
}
val bl_term_stats : Formula.bl_term -> stats
val bv_term_stats : Formula.bv_term -> stats
val ax_term_stats : Formula.ax_term -> stats
val bl_term_variables : Formula.bl_term -> Formula.VarSet.t
val bv_term_variables : Formula.bv_term -> Formula.VarSet.t
val ax_term_variables : Formula.ax_term -> Formula.VarSet.t
val is_symbolic_bl_term : Formula.bl_term -> bool
  • returns

    true if the expression is syntactically symbolic meaning there is at least one variable

val is_symbolic_bv_term : Formula.bv_term -> bool
val is_symbolic_ax_term : Formula.ax_term -> bool
val bv_size : Formula.bv_term -> int
val ax_size : Formula.ax_term -> int * int
val bv_desc_size : Formula.bv_term_desc -> int
val ax_desc_size : Formula.ax_term_desc -> int * int
val is_bl_desc_cst : Formula.bl_term_desc -> bool option
val is_bv_desc_cst : Formula.bv_term_desc -> Bitvector.t option
val is_bl_cst : Formula.bl_term -> bool option
val is_bv_cst : Formula.bv_term -> Bitvector.t option
val is_bl_desc_var : Formula.bl_term_desc -> Formula.bl_var option
val is_bv_desc_var : Formula.bv_term_desc -> Formula.bv_var option
val is_ax_desc_var : Formula.ax_term_desc -> Formula.ax_var option
val is_bl_var : Formula.bl_term -> Formula.bl_var option
val is_bv_var : Formula.bv_term -> Formula.bv_var option
val is_ax_var : Formula.ax_term -> Formula.ax_var option
val is_select : Formula.bv_term -> (int * Formula.ax_term * Formula.bv_term) option
val is_store : Formula.ax_term -> (int * Formula.ax_term * Formula.bv_term * Formula.bv_term) option
val var_hash : Formula.var -> int
val bl_var_hash : Formula.bl_var -> int
val bv_var_hash : Formula.bv_var -> int
val ax_var_hash : Formula.ax_var -> int
val var_name : Formula.var -> string
val bl_var_name : Formula.bl_var -> string
val bv_var_name : Formula.bv_var -> string
val ax_var_name : Formula.ax_var -> string
val bl_term_desc_name : Formula.bl_term_desc -> string option
val bv_term_desc_name : Formula.bv_term_desc -> string option
val ax_term_desc_name : Formula.ax_term_desc -> string option
val bl_term_name : Formula.bl_term -> string option
val bv_term_name : Formula.bv_term -> string option
val ax_term_name : Formula.ax_term -> string option
val decl_desc_name : Formula.decl_desc -> string
val def_desc_name : Formula.def_desc -> string
val decl_name : Formula.decl -> string
val def_name : Formula.def -> string
module BindEnv : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct