package binsec

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

Source file formula_options.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
(**************************************************************************)
(*  This file is part of BINSEC.                                          *)
(*                                                                        *)
(*  Copyright (C) 2016-2026                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

include
  Cli.Make_from_logger
    (Smtlib.Formula.Logger)
    (struct
      let shortname = "fml"
      let name = "Formulas"
    end)

module OptimAll = Builder.No (struct
  let name = "optim-all"

  let doc =
    "Do not force all the optimizations (each optimization can still be set \
     individually)"
end)

module OptimCst = Builder.False (struct
  let name = "optim-cst"
  let doc = "Enable constant propagation"
end)

module OptimItv = Builder.False (struct
  let name = "optim-itv"
  let doc = "Enable intervals in read-over-write"
end)

module OptimPrn = Builder.False (struct
  let name = "optim-prn"
  let doc = "Enable pruning and inlining"
end)

module OptimRbs = Builder.False (struct
  let name = "optim-rbs"
  let doc = "Enable rebasing in read-over-write"
end)

module OptimRow = Builder.False (struct
  let name = "optim-row"
  let doc = "Enable read-over-write"
end)

module OptimSsa = Builder.False (struct
  let name = "optim-ssa"
  let doc = "Enable static single assignment"
end)

module OptimLst = Builder.Integer (struct
  let name = "optim-lst"
  let doc = "Switch to list-like memory representation in read-over-write"
  let default = 0
end)

type solver = Smtlib.Solver.t

module Solver = struct
  include Builder.Variant_choice_assoc (struct
    type t = solver

    let assoc_map : (string * solver) list =
      [
        ("z3", Z3);
        ("cvc4", CVC4);
        ("yices", Yices);
        ("boolector", Boolector);
        ("bitwuzla", Bitwuzla);
      ]

    let default : solver = Z3
    let name = "solver"
    let doc = " Set solver to use"
  end)

  module Timeout = Builder.Integer (struct
    let name = "solver-timeout"
    let doc = "Timeout for solver queries"
    let default = 5
  end)

  module Options = Builder.String_option (struct
    let name = "solver-options"
    let doc = "Use these options to launch the solver (ignore default options)"
  end)
end

module No_stitching = Builder.False (struct
  let name = "no-stitching"
  let doc = "Do not try to stitch together continuous stores/select"
end)