Skip to content

Commit 81b71d8

Browse files
committed
Adapt graph to also include loops including the goal.
1 parent 88e3983 commit 81b71d8

File tree

1 file changed

+8
-6
lines changed

1 file changed

+8
-6
lines changed

src/analyses/base.ml

+8-6
Original file line numberDiff line numberDiff line change
@@ -1256,13 +1256,15 @@ struct
12561256
let goal_reached = AD.exists (fun g -> is_prefix_of n g) goal in
12571257
let already_visited = AD.subset (AD.singleton n) visited in
12581258
if already_visited then
1259-
false, graph
1260-
else if goal_reached then
1261-
let graph = ValueDomain.ADGraph.add node (AD.singleton n) graph in
1262-
(true, graph)
1263-
else begin
1259+
if goal_reached then
1260+
let graph = ValueDomain.ADGraph.add node (AD.singleton n) graph in
1261+
(true, graph)
1262+
else
1263+
false, graph
1264+
else
1265+
begin
12641266
let found, graph = dfs n (visited, graph) in
1265-
if found then
1267+
if goal_reached || found then
12661268
let graph = ValueDomain.ADGraph.add node (AD.singleton n) graph in
12671269
(true, graph)
12681270
else

0 commit comments

Comments
 (0)