diff options
| author | Son HO | 2023-08-09 09:58:04 +0200 |
|---|---|---|
| committer | GitHub | 2023-08-09 09:58:04 +0200 |
| commit | 3d377976afe382a32f6ce718b473db5f016b1e47 (patch) | |
| tree | 3f5b7147d1c4edc2b5c9ac002e1a203cfb396427 /compiler/Driver.ml | |
| parent | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (diff) | |
| parent | 967d08107de73f7f151dc8b4fb1f1cc61f109051 (diff) | |
Merge pull request #33 from AeneasVerif/son_refactor
Update the code following Charon's refactor
Diffstat (limited to 'compiler/Driver.ml')
| -rw-r--r-- | compiler/Driver.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index d819768b..b646a53d 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -214,7 +214,9 @@ let () = (* Print a warning if the crate contains loops (loops are experimental for now) *) let has_loops = - List.exists Aeneas.LlbcAstUtils.fun_decl_has_loops m.functions + A.FunDeclId.Map.exists + (fun _ -> Aeneas.LlbcAstUtils.fun_decl_has_loops) + m.functions in if has_loops then log#lwarning (lazy "Support for loops is experimental"); @@ -222,7 +224,9 @@ let () = whenever there are opaque functions *) if !backend = Lean - && List.exists (fun (d : A.fun_decl) -> d.body = None) m.functions + && A.FunDeclId.Map.exists + (fun _ (d : A.fun_decl) -> d.body = None) + m.functions && not !split_files then ( log#error |