Skip to content

Commit d5ae8ea

Browse files
mrstanbmrstanb
committed
Fix indent issues
1 parent 7c2455a commit d5ae8ea

File tree

1 file changed

+72
-73
lines changed

1 file changed

+72
-73
lines changed

‎src/util/precisionUtil.ml‎

Lines changed: 72 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -1,75 +1,74 @@
11
(* We define precision by the number of IntDomains activated.
22
* We currently have 4 types: DefExc, Interval, Enums, Congruence *)
3-
type int_precision = (bool * bool * bool * bool)
4-
(* Same applies for FloatDomain
5-
* We currently have only an interval type analysis *)
6-
type float_precision = (bool)
7-
8-
let def_exc: bool option ref = ref None
9-
let interval: bool option ref = ref None
10-
let enums: bool option ref = ref None
11-
let congruence: bool option ref = ref None
12-
13-
let get_def_exc () =
14-
if !def_exc = None then
15-
def_exc := Some (GobConfig.get_bool "ana.int.def_exc");
16-
Option.get !def_exc
17-
18-
let get_interval () =
19-
if !interval = None then
20-
interval := Some (GobConfig.get_bool "ana.int.interval");
21-
Option.get !interval
22-
23-
let get_enums () =
24-
if !enums = None then
25-
enums := Some (GobConfig.get_bool "ana.int.enums");
26-
Option.get !enums
27-
28-
let get_congruence () =
29-
if !congruence = None then
30-
congruence := Some (GobConfig.get_bool "ana.int.congruence");
31-
Option.get !congruence
32-
33-
let annotation_int_enabled: bool option ref = ref None
34-
35-
let get_annotation_int_enabled () =
36-
if !annotation_int_enabled = None then
37-
annotation_int_enabled := Some (GobConfig.get_bool "annotation.int.enabled");
38-
Option.get !annotation_int_enabled
39-
40-
(* Thus for maximum precision we activate all Domains *)
41-
let max_int_precision : int_precision = (true, true, true, true)
42-
let max_float_precision : float_precision = (true)
43-
let int_precision_from_fundec (fd: GoblintCil.fundec): int_precision =
44-
((ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_def_exc ()) ~removeAttr:"no-def_exc" ~keepAttr:"def_exc" fd),
45-
(ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_interval ()) ~removeAttr:"no-interval" ~keepAttr:"interval" fd),
46-
(ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_enums ()) ~removeAttr:"no-enums" ~keepAttr:"enums" fd),
47-
(ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_congruence ()) ~removeAttr:"no-congruence" ~keepAttr:"congruence" fd))
48-
49-
let float_precision_from_fundec (fd: GoblintCil.fundec): float_precision =
50-
((ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.float.interval" ~removeAttr:"no-float-interval" ~keepAttr:"float-interval" fd))
51-
let int_precision_from_node (): int_precision =
52-
match !MyCFG.current_node with
53-
| Some n -> int_precision_from_fundec (Node.find_fundec n)
54-
| _ -> max_int_precision (* In case a Node is None we have to handle Globals, i.e. we activate all IntDomains (TODO: verify this assumption) *)
55-
56-
let is_congruence_active (_, _, _, c: int_precision): bool = c
57-
58-
let float_precision_from_node (): float_precision =
59-
match !MyCFG.current_node with
60-
| Some n -> float_precision_from_fundec (Node.find_fundec n)
61-
| _ -> max_float_precision
62-
63-
let int_precision_from_node_or_config (): int_precision =
64-
if get_annotation_int_enabled () then
65-
int_precision_from_node ()
66-
else
67-
(get_def_exc (), get_interval (), get_enums (), get_congruence ())
68-
69-
let float_precision_from_node_or_config (): float_precision =
70-
if GobConfig.get_bool "annotation.float.enabled" then
71-
float_precision_from_node ()
72-
else
73-
let f n = GobConfig.get_bool ("ana.float."^n) in
74-
(f "interval")
75-
3+
type int_precision = (bool * bool * bool * bool)
4+
(* Same applies for FloatDomain
5+
* We currently have only an interval type analysis *)
6+
type float_precision = (bool)
7+
8+
let def_exc: bool option ref = ref None
9+
let interval: bool option ref = ref None
10+
let enums: bool option ref = ref None
11+
let congruence: bool option ref = ref None
12+
13+
let get_def_exc () =
14+
if !def_exc = None then
15+
def_exc := Some (GobConfig.get_bool "ana.int.def_exc");
16+
Option.get !def_exc
17+
18+
let get_interval () =
19+
if !interval = None then
20+
interval := Some (GobConfig.get_bool "ana.int.interval");
21+
Option.get !interval
22+
23+
let get_enums () =
24+
if !enums = None then
25+
enums := Some (GobConfig.get_bool "ana.int.enums");
26+
Option.get !enums
27+
28+
let get_congruence () =
29+
if !congruence = None then
30+
congruence := Some (GobConfig.get_bool "ana.int.congruence");
31+
Option.get !congruence
32+
33+
let annotation_int_enabled: bool option ref = ref None
34+
35+
let get_annotation_int_enabled () =
36+
if !annotation_int_enabled = None then
37+
annotation_int_enabled := Some (GobConfig.get_bool "annotation.int.enabled");
38+
Option.get !annotation_int_enabled
39+
40+
(* Thus for maximum precision we activate all Domains *)
41+
let max_int_precision : int_precision = (true, true, true, true)
42+
let max_float_precision : float_precision = (true)
43+
let int_precision_from_fundec (fd: GoblintCil.fundec): int_precision =
44+
((ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_def_exc ()) ~removeAttr:"no-def_exc" ~keepAttr:"def_exc" fd),
45+
(ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_interval ()) ~removeAttr:"no-interval" ~keepAttr:"interval" fd),
46+
(ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_enums ()) ~removeAttr:"no-enums" ~keepAttr:"enums" fd),
47+
(ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_congruence ()) ~removeAttr:"no-congruence" ~keepAttr:"congruence" fd))
48+
49+
let float_precision_from_fundec (fd: GoblintCil.fundec): float_precision =
50+
((ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.float.interval" ~removeAttr:"no-float-interval" ~keepAttr:"float-interval" fd))
51+
let int_precision_from_node (): int_precision =
52+
match !MyCFG.current_node with
53+
| Some n -> int_precision_from_fundec (Node.find_fundec n)
54+
| _ -> max_int_precision (* In case a Node is None we have to handle Globals, i.e. we activate all IntDomains (TODO: verify this assumption) *)
55+
56+
let is_congruence_active (_, _, _, c: int_precision): bool = c
57+
58+
let float_precision_from_node (): float_precision =
59+
match !MyCFG.current_node with
60+
| Some n -> float_precision_from_fundec (Node.find_fundec n)
61+
| _ -> max_float_precision
62+
63+
let int_precision_from_node_or_config (): int_precision =
64+
if get_annotation_int_enabled () then
65+
int_precision_from_node ()
66+
else
67+
(get_def_exc (), get_interval (), get_enums (), get_congruence ())
68+
69+
let float_precision_from_node_or_config (): float_precision =
70+
if GobConfig.get_bool "annotation.float.enabled" then
71+
float_precision_from_node ()
72+
else
73+
let f n = GobConfig.get_bool ("ana.float."^n) in
74+
(f "interval")

0 commit comments

Comments
 (0)