summaryrefslogtreecommitdiff
path: root/src/CfimAstUtils.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-06 14:43:35 +0100
committerSon Ho2022-01-06 14:43:35 +0100
commitf2fb0dc39cfa9aef2b16963d3f8a270ec45bae5e (patch)
tree652fbd0e923a1cae5d6516f4ce9cadd9177c56db /src/CfimAstUtils.ml
parent3cadf01e5b67af4ec91f2de3c32e119cd90c678c (diff)
Make good progress on implementing utilities to test symbolic execution
Diffstat (limited to 'src/CfimAstUtils.ml')
-rw-r--r--src/CfimAstUtils.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml
index f811475c..96410dde 100644
--- a/src/CfimAstUtils.ml
+++ b/src/CfimAstUtils.ml
@@ -2,7 +2,7 @@ open CfimAst
open Utils
(** Check if a [statement] contains loops *)
-let rec statement_has_loops (st : statement) : bool =
+let statement_has_loops (st : statement) : bool =
let obj =
object
inherit [_] iter_statement
@@ -14,3 +14,6 @@ let rec statement_has_loops (st : statement) : bool =
obj#visit_statement () st;
false
with Found -> true
+
+(** Check if a [fun_def] contains loops *)
+let fun_def_has_loops (fd : fun_def) : bool = statement_has_loops fd.body