package binsec

  1. Overview
  2. Docs
Semantic analysis of binary executables

Install 

dune-project
 Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (19)

Authors

  1. A
    Adel Djoudi
  2. B
    Benjamin Farinier
  3. C
    Chakib Foulani
  4. D
    Dorian Lesbre
  5. F
    Frédéric Recoules
  6. G
    Guillaume Girol
  7. J
    Josselin Feist
  8. L
    Lesly-Ann Daniel
  9. M
    Mahmudul Faisal Al Ameen
  10. M
    Manh-Dung Nguyen
  11. M
    Mathéo Vergnolle
  12. M
    Mathilde Ollivier
  13. M
    Matthieu Lemerre
  14. N
    Nicolas Bellec
  15. O
    Olivier Nicole
  16. R
    Richard Bonichon
  17. R
    Robin David
  18. S
    Sébastien Bardin
  19. S
    Soline Ducousso
  20. T
    Ta Thanh Dinh
  21. Y
    Yaëlle Vinçont
  22. Y
    Yanis Sellami

Maintainers

  1. B
    BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.11.0.tbz
sha256=4cf70a0367fef6f33ee3165f05255914513ea0539b94ddfef0bd46fc9b42fa8a
sha512=cd67a5b7617f661a7786bef0c828ee55307cef5260dfecbb700a618be795d81b1ac49fc1a18c4904fd2eb8a182dc862b0159093028651e78e7dc743f5babf9e3

doc/binsec.smtlib/Binsec_smtlib/Lang/index.html

Module Binsec_smtlib.LangSource

type numeral = string

Concrete parse tree for SMT-LIB Formulas.

type constant =
  1. | CstNumeral of numeral
  2. | CstDecimal of string
  3. | CstDecimalSize of string * string
  4. | CstHexadecimal of string
  5. | CstBinary of string
  6. | CstString of string
  7. | CstBool of bool
type symbol_desc =
  1. | SimpleSymbol of string
  2. | QuotedSymbol of string
type symbol = {
  1. symbol_desc : symbol_desc;
  2. symbol_loc : Binsec_smtlib__.Location.t;
}
type symbols = symbol list
type keyword = string
type sexpr_desc =
  1. | SexprConstant of constant
  2. | SexprSymbol of symbol
  3. | SexprKeyword of keyword
  4. | SexprParens of sexprs
and sexpr = {
  1. sexpr_desc : sexpr_desc;
  2. sexpr_loc : Binsec_smtlib__.Location.t;
}
and sexprs = sexpr list
type index =
  1. | IdxNum of numeral
  2. | IdxSymbol of symbol
type indexes = index list
type info_flag_desc =
  1. | InfoFlagKeyword of keyword
type info_flag = {
  1. info_flag_desc : info_flag_desc;
  2. info_flag_loc : Binsec_smtlib__.Location.t;
}
type id_desc =
  1. | IdSymbol of symbol
  2. | IdUnderscore of symbol * indexes
type identifier = {
  1. id_desc : id_desc;
  2. id_loc : Binsec_smtlib__.Location.t;
}
type attr_value_desc =
  1. | AttrValSpecConstant of constant
  2. | AttrValSymbol of symbol
  3. | AttrValSexpr of sexprs
type attr_value = {
  1. attr_value_desc : attr_value_desc;
  2. attr_value_loc : Binsec_smtlib__.Location.t;
}
type attribute_desc =
  1. | AttrKeyword of keyword
  2. | AttrKeywordValue of keyword * attr_value
type attribute = {
  1. attribute_desc : attribute_desc;
  2. attribute_loc : Binsec_smtlib__.Location.t;
}
type attributes = attribute list
type smt_option_desc =
  1. | OptionAttribute of attribute
type smt_option = {
  1. smt_option_desc : smt_option_desc;
  2. smt_option_loc : Binsec_smtlib__.Location.t;
}
type sort = {
  1. sort_desc : sort_desc;
  2. sort_loc : Binsec_smtlib__.Location.t;
}
and sorts = sort list
and sort_desc =
  1. | SortIdentifier of identifier
  2. | SortFun of identifier * sorts
type qual_identifier_desc =
  1. | QualIdentifierIdentifier of identifier
  2. | QualIdentifierAs of identifier * sort
type qual_identifier = {
  1. qual_identifier_desc : qual_identifier_desc;
  2. qual_identifier_loc : Binsec_smtlib__.Location.t;
}
type sorted_var_desc =
  1. | SortedVar of symbol * sort
type sorted_var = {
  1. sorted_var_desc : sorted_var_desc;
  2. sorted_var_loc : Binsec_smtlib__.Location.t;
}
type sorted_vars = sorted_var list
type var_binding_desc =
  1. | VarBinding of symbol * term
and var_binding = {
  1. var_binding_desc : var_binding_desc;
  2. var_binding_loc : Binsec_smtlib__.Location.t;
}
and var_bindings = var_binding list
and term_desc =
  1. | TermSpecConstant of constant
  2. | TermQualIdentifier of qual_identifier
  3. | TermQualIdentifierTerms of qual_identifier * terms
  4. | TermLetTerm of var_bindings * term
  5. | TermForallTerm of sorted_vars * term
  6. | TermExistsTerm of sorted_vars * term
  7. | TermLambdaTerm of sorted_vars * term
  8. | TermAnnotatedTerm of term * attributes
and terms = term list
and term = {
  1. term_desc : term_desc;
  2. term_loc : Binsec_smtlib__.Location.t;
}
type fun_def_desc =
  1. | FunDef of symbol * sorts option * sorted_vars * sort * term
type fun_def = {
  1. fun_def_desc : fun_def_desc;
  2. fun_def_loc : Binsec_smtlib__.Location.t;
}
type fun_rec_def_desc =
  1. | FunRecDef of symbol * sorts option * sorted_vars * sort * term
type fun_rec_def = {
  1. fun_rec_def_desc : fun_rec_def_desc;
  2. fun_rec_def_loc : Binsec_smtlib__.Location.t;
}
type fun_rec_defs = fun_rec_def list
type command_desc =
  1. | CmdAssert of term
  2. | CmdCheckSat
  3. | CmdCheckSatAssuming of symbols
  4. | CmdComment of string
  5. | CmdDeclareConst of symbol * sort
  6. | CmdDeclareFun of symbol * sorts option * sorts * sort
  7. | CmdDeclareSort of symbol * numeral
  8. | CmdDefineFun of fun_def
  9. | CmdDefineFunRec of fun_rec_defs
  10. | CmdDefineSort of symbol * symbols * sort
  11. | CmdEcho of string
  12. | CmdExit
  13. | CmdGetAssertions
  14. | CmdGetAssignment
  15. | CmdGetInfo of info_flag
  16. | CmdGetModel
  17. | CmdGetOption of keyword
  18. | CmdGetProof
  19. | CmdGetUnsatAssumptions
  20. | CmdGetUnsatCore
  21. | CmdGetValue of terms
  22. | CmdMetaInfo of attribute
  23. | CmdPop of numeral option
  24. | CmdPush of numeral option
  25. | CmdReset
  26. | CmdResetAssertions
  27. | CmdSetInfo of attribute
  28. | CmdSetLogic of symbol
  29. | CmdSetOption of smt_option
type command = {
  1. command_desc : command_desc;
  2. command_loc : Binsec_smtlib__.Location.t;
}
type commands = command list
type script = {
  1. script_commands : commands;
  2. script_loc : Binsec_smtlib__.Location.t;
}
type model = {
  1. model_commands : commands;
  2. model_loc : Binsec_smtlib__.Location.t;
}
module Location : sig ... end
module Lexer : sig ... end
module Parser : sig ... end
module Printer : sig ... end
module Utils : sig ... end