summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-05-06 10:02:42 +0200
committerSon Ho2022-05-06 10:02:42 +0200
commitccc86647e1f130bb19e288b88d167c3b1609e421 (patch)
tree69f8e0b6e1f4b048e73d64163f52d695a08053af /src
parentec920cf54bd22246cfdbbbc9301e4f5b4716d009 (diff)
Add comments in FunsAnalysis
Diffstat (limited to '')
-rw-r--r--src/FunsAnalysis.ml10
1 files changed, 8 insertions, 2 deletions
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index f187184a..dc205eb9 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -1,7 +1,8 @@
(** Compute various information, including:
- can a function fail (by having `Fail` in its body, or transitively
calling a function which can fail)
- - can a function diverge
+ - can a function diverge (bu being recursive, containing a loop or
+ transitively calling a function which can diverge)
- does a function perform stateful operations (i.e., do we need a state
to translate it)
*)
@@ -35,7 +36,12 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
(* Analyze a group of mutually recursive functions.
* As the functions can call each other, we compute the same information
- * for all of them.
+ * for all of them (if one of the functions can fail, then all of them
+ * can fail, etc.).
+ *
+ * We simply check if the functions contains panic statements, loop statements,
+ * recursive calls, etc. We use the previously computed information in case
+ * of function calls.
*)
let analyze_fun_decls (fun_ids : FunDeclId.Set.t) (d : fun_decl list) :
fun_info =