diff options
| -rw-r--r-- | src/FunsAnalysis.ml | 10 |
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 = |