11(* =============================================================================
2- CodeHawk Binary Analyzer
2+ CodeHawk Binary Analyzer
33 Author: Henny Sipma
44 ------------------------------------------------------------------------------
55 The MIT License (MIT)
6-
6+
77 Copyright (c) 2005-2019 Kestrel Technology LLC
88 Copyright (c) 2020 Henny B. Sipma
99 Copyright (c) 2021-2024 Aarno Labs LLC
1414 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1515 copies of the Software, and to permit persons to whom the Software is
1616 furnished to do so, subject to the following conditions:
17-
17+
1818 The above copyright notice and this permission notice shall be included in all
1919 copies or substantial portions of the Software.
20-
20+
2121 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
2222 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
2323 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -39,23 +39,25 @@ open CHAnalysisSetup
3939(* bchanalyze *)
4040open BCHAnalysisTypes
4141
42+ [@@@ warning " -27" ]
43+
4244module H = Hashtbl
4345
4446
4547class bb_invariants_t :bb_invariants_int =
4648object
4749 val invariants = H. create 3
48-
50+
4951 method reset = H. clear invariants
50-
52+
5153 method add_invariant (opname :string ) (domain :string ) (inv :atlas_t ) =
5254 let optable = if H. mem invariants opname then
53- H. find invariants opname
55+ H. find invariants opname
5456 else
5557 let table = H. create 1 in
56- begin H. add invariants opname table ; table end in
58+ begin H. add invariants opname table; table end in
5759 H. replace optable domain inv
58-
60+
5961 method get_invariants = invariants
6062
6163 method toPretty =
@@ -69,44 +71,48 @@ object
6971 result := p :: ! result) varinvs) invariants;
7072 LBLOCK (List. rev ! result)
7173 end
72-
74+
7375end
7476
7577let bb_invariants = new bb_invariants_t
7678
77- let default_opsemantics domain =
79+ let default_opsemantics domain =
7880 fun ~invariant ~stable ~fwd_direction ~context ~operation ->
79- let _ = if stable then
80- if operation.op_name#getBaseName = " invariant" then
81- bb_invariants#add_invariant (List. hd (operation.op_name#getAttributes)) domain invariant in
81+ let _ =
82+ if stable then
83+ if operation.op_name#getBaseName = " invariant" then
84+ bb_invariants#add_invariant
85+ (List. hd (operation.op_name#getAttributes)) domain invariant in
8286 invariant
8387
84- let analyze_procedure_with_linear_equalities (proc :procedure_int ) (system :system_int ) =
88+ let analyze_procedure_with_linear_equalities
89+ (proc :procedure_int ) (system :system_int ) =
8590 let analysis_setup = mk_analysis_setup () in
8691 begin
87- analysis_setup#addLinearEqualities ;
88- analysis_setup#setOpSemantics (default_opsemantics " karr" ) ;
89- analysis_setup#analyze_procedure system proc
92+ analysis_setup#addLinearEqualities;
93+ analysis_setup#setOpSemantics (default_opsemantics " karr" );
94+ analysis_setup#analyze_procedure system proc
9095 end
9196
9297let analyze_procedure_with_intervals (proc :procedure_int ) (system :system_int ) =
9398 let analysis_setup = mk_analysis_setup () in
9499 begin
95- analysis_setup#addIntervals ;
96- analysis_setup#setOpSemantics (default_opsemantics " intervals" ) ;
97- analysis_setup#analyze_procedure system proc
100+ analysis_setup#addIntervals;
101+ analysis_setup#setOpSemantics (default_opsemantics " intervals" );
102+ analysis_setup#analyze_procedure system proc
98103 end
99-
104+
100105let analyze_procedure_with_valuesets (proc :procedure_int ) (system :system_int ) =
101106 let analysis_setup = mk_analysis_setup () in
102107 begin
103- analysis_setup#addValueSets ;
104- analysis_setup#setOpSemantics (default_opsemantics " valuesets" ) ;
108+ analysis_setup#addValueSets;
109+ analysis_setup#setOpSemantics (default_opsemantics " valuesets" );
105110 analysis_setup#analyze_procedure system proc
106111 end
107112
108113
109- let analyze_procedure_with_symbolic_sets (proc : procedure_int ) (system : system_int ) =
114+ let analyze_procedure_with_symbolic_sets
115+ (proc : procedure_int ) (system : system_int ) =
110116 let analysis_setup = mk_analysis_setup () in
111117 begin
112118 analysis_setup#addDomain " symbolicsets" (new symbolic_sets_domain_no_arrays_t);
0 commit comments