Skip to content

Commit 84af5fd

Browse files
committed
Fix indentation in arg/
1 parent 80713b1 commit 84af5fd

File tree

5 files changed

+50
-50
lines changed

5 files changed

+50
-50
lines changed

src/arg/argConstraints.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ open Analyses
77
(** Add path sensitivity to a analysis *)
88
module PathSensitive3 (Spec:Spec)
99
: Spec
10-
(* with type D.t = SetDomain.ToppedSet(Spec.D)(N).t
10+
(* with type D.t = SetDomain.ToppedSet(Spec.D)(N).t
1111
and module G = Spec.G
1212
and module C = Spec.C *)
1313
=
@@ -266,7 +266,7 @@ struct
266266

267267
let should_inline f =
268268
(* (* inline __VERIFIER_error because Control requires the corresponding FunctionEntry node *)
269-
not (Svcomp.is_special_function f) || Svcomp.is_error_function f *)
269+
not (Svcomp.is_special_function f) || Svcomp.is_error_function f *)
270270
(* TODO: don't inline __VERIFIER functions for CPAchecker, but inlining needed for WP *)
271271
true
272272

src/arg/argTools.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -199,11 +199,11 @@ struct
199199
struct
200200
module Node: MyARG.Node with type t = Node.t =
201201
(val match GobConfig.get_string "exp.arg.id" with
202-
| "node" ->
203-
(module Node: MyARG.Node with type t = Node.t)
204-
| "enumerate" ->
205-
(module EnumerateNode (Node): MyARG.Node with type t = Node.t)
206-
| _ -> failwith "exp.arg.id: illegal value"
202+
| "node" ->
203+
(module Node: MyARG.Node with type t = Node.t)
204+
| "enumerate" ->
205+
(module EnumerateNode (Node): MyARG.Node with type t = Node.t)
206+
| _ -> failwith "exp.arg.id: illegal value"
207207
)
208208

209209
module Edge = MyARG.InlineEdge

src/arg/observerAnalysis.ml

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -94,18 +94,18 @@ struct
9494
type t = Node.t * Node.t [@@deriving eq]
9595
let pattern = Array.of_list Arg.path
9696
end
97-
)
97+
)
9898

9999
include MakeSpec (KMP)
100100

101101
(* let () = Arg.path
102-
|> List.map (fun (p, n) -> Printf.sprintf "(%d, %d)" p n)
103-
|> String.concat "; "
104-
|> Printf.printf "observer path: [%s]\n" *)
102+
|> List.map (fun (p, n) -> Printf.sprintf "(%d, %d)" p n)
103+
|> String.concat "; "
104+
|> Printf.printf "observer path: [%s]\n" *)
105105
end
106106

107107
(* let _ =
108-
let module Spec = MakeSpec (
108+
let module Spec = MakeSpec (
109109
struct
110110
(* let path = [(23, 24); (24, 25)] *)
111111
(* let path = [(30, 32); (32, 34); (34, 26); (26, 29)] *)
@@ -126,6 +126,6 @@ end
126126
(* let path = [(20, 21); (21, 25); (25, 27)] *)
127127
let path = [(23, 24); (24, 25); (25, 27)]
128128
end
129-
)
130-
in
131-
MCP.register_analysis (module Spec) *)
129+
)
130+
in
131+
MCP.register_analysis (module Spec) *)

src/arg/observerAutomaton.ml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,14 +30,14 @@ struct
3030
let accepting q = q = m
3131

3232
(* let next_inner prefix q x =
33-
let q' = ref q in
34-
while !q' > 0 && not (equal pattern.(!q') x) do
33+
let q' = ref q in
34+
while !q' > 0 && not (equal pattern.(!q') x) do
3535
q' := prefix.(!q' - 1)
36-
done;
37-
if equal pattern.(!q') x then begin
36+
done;
37+
if equal pattern.(!q') x then begin
3838
q' := !q' + 1
39-
end;
40-
!q' *)
39+
end;
40+
!q' *)
4141
let rec next_inner prefix q x =
4242
if q > 0 && not (equal pattern.(q) x) then
4343
next_inner prefix prefix.(q - 1) x

src/arg/violation.ml

Lines changed: 29 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -124,35 +124,35 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
124124
| Some path ->
125125
print_path path;
126126
begin match Feasibility.check_path path with
127-
| Feasibility.Feasible ->
128-
Logs.debug "feasible";
129-
130-
let module PathArg =
131-
struct
132-
module Node = Arg.Node
133-
module Edge = Arg.Edge
134-
135-
let main_entry = BatTuple.Tuple3.first (List.hd path)
136-
137-
let next =
138-
let module NHT = BatHashtbl.Make (Node) in
139-
let next = NHT.create (List.length path) in
140-
List.iter (fun (n1, e, n2) ->
141-
NHT.modify_def [] n1 (fun nexts -> (e, n2) :: nexts) next
142-
) path;
143-
144-
(fun n -> NHT.find_default next n [])
145-
end
146-
in
147-
Feasible (module PathArg)
148-
| Feasibility.Infeasible subpath ->
149-
Logs.debug "infeasible";
150-
print_path subpath;
151-
152-
Infeasible subpath
153-
| Feasibility.Unknown ->
154-
Logs.debug "unknown";
155-
Unknown
127+
| Feasibility.Feasible ->
128+
Logs.debug "feasible";
129+
130+
let module PathArg =
131+
struct
132+
module Node = Arg.Node
133+
module Edge = Arg.Edge
134+
135+
let main_entry = BatTuple.Tuple3.first (List.hd path)
136+
137+
let next =
138+
let module NHT = BatHashtbl.Make (Node) in
139+
let next = NHT.create (List.length path) in
140+
List.iter (fun (n1, e, n2) ->
141+
NHT.modify_def [] n1 (fun nexts -> (e, n2) :: nexts) next
142+
) path;
143+
144+
(fun n -> NHT.find_default next n [])
145+
end
146+
in
147+
Feasible (module PathArg)
148+
| Feasibility.Infeasible subpath ->
149+
Logs.debug "infeasible";
150+
print_path subpath;
151+
152+
Infeasible subpath
153+
| Feasibility.Unknown ->
154+
Logs.debug "unknown";
155+
Unknown
156156
end
157157
| None ->
158158
Unknown

0 commit comments

Comments
 (0)