Checkct (p.binsec.0.8.1.doc.checkct.Checkct)

binsec
- CHANGES
- LICENSE
- README
- Library binsec
  - Binsec
- Library binsec.amd64decoder
  - Amd64decoder
- Library binsec.armv7decoder
  - Armv7decoder
- Library binsec.armv8decoder
  - Armv8decoder
- Library binsec.domains
  - Domains
- Library binsec.parser
  - Libparser
- Library binsec.ppc64decoder
  - Ppc64decoder
- Library binsec.smt
  - Smt
- Library binsec.sse
  - Libsse
- Library binsec.sse_register
  - Sse
- Library checkct
  - Checkct
- Library libformula
  - Libformula
- Library libterm
  - Libterm
- Library shadow_stack
  - Shadow_stack
- Sources

Sourcemodule S = Binsec.Basic_types.String

Sourcemodule B = Binsec.Bitvector.Collection

include sig ... end

val is_enabled : unit -> bool

module Logger : Binsec.Logger.S

module Debug_level : sig ... end

module Loglevel : sig ... end

module Quiet : sig ... end

module Builder : sig ... end

Sourcetype leak_info =

| HaltLeak
(*
Halts at first leak
*)
| InstrLeak
(*
Reports leaky instructions (each one is reported only once)
*)

Sourcemodule LeakInfo : sig ... end

Sourcemodule Taint : sig ... end

Sourcemodule ChosenValues : sig ... end

Sourcemodule Relse : sig ... end

Sourcemodule StatsFile : sig ... end

Sourcemodule Kind : sig ... end

Sourcemodule Report : sig ... end

Sourcemodule Status : sig ... end

Sourcetype Binsec.Ast.Obj.t +=

| Bool of bool

Sourcetype Binsec.Ast.Instr.t +=

| Secret of Binsec.Ast.Loc.t Binsec.Ast.loc

Sourcetype Binsec.Ast.t +=

| Globals of bool * string list

Sourcetype Libsse.Ir.builtin +=

| Mirror of Binsec.Dba.Var.t
| Check of Binsec.Dba.Expr.t * Kind.t

Sourcemodule type OPTIONS = sig ... end

Sourceval make_options : unit -> (module OPTIONS)

Sourcemodule Ct_state : sig ... end

Source

module Make
  (Options : OPTIONS)
  (Stats : Libsse.Types.EXPLORATION_STATISTICS)
  (Path : Libsse.Path.S)
  (State : Libsse.Types.STATE with type Value.t = Libterm.Sexpr.Expr.t) : 
  Libsse.Exec.EXTENSION with type path = Path.t and type state = State.t