diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Errors.ml | 1 | ||||
| -rw-r--r-- | compiler/ExtractToFStar.ml | 2 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 2 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 6 | ||||
| -rw-r--r-- | compiler/dune | 1 |
10 files changed, 10 insertions, 12 deletions
diff --git a/compiler/Errors.ml b/compiler/Errors.ml deleted file mode 100644 index 58dd3a0b..00000000 --- a/compiler/Errors.ml +++ /dev/null @@ -1 +0,0 @@ -include Charon.Errors diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml index b44b8f25..7267101c 100644 --- a/compiler/ExtractToFStar.ml +++ b/compiler/ExtractToFStar.ml @@ -1,6 +1,6 @@ (** Extract to F* *) -open Errors +open Utils open Pure open PureUtils open TranslateCore diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 7f51c5b9..f93a0ae1 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -137,7 +137,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return * will end - this will allow us to, first, mark the other return * regions as non-endable, and, second, end those parent regions in * proper order. *) - let parent_rgs = list_parent_region_groups sg back_id in + let parent_rgs = list_ancestor_region_groups sg back_id in let parent_input_abs_ids = T.RegionGroupId.mapi (fun rg_id rg -> diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 16f68d9e..e2d2bb0a 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -442,7 +442,7 @@ let give_back_symbolic_value (_config : C.config) (* Substitution function, to replace the borrow projectors over symbolic values *) let subst (_abs : V.abs) local_given_back = (* See the below comments: there is something wrong here *) - let _ = raise Errors.Unimplemented in + let _ = raise Utils.Unimplemented in (* Compute the projection over the given back value *) let child_proj = match nsv.sv_kind with diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 9a944428..cd6df2b0 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -712,7 +712,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = | T.Adt (Assumed (Vec | Option), _, _) -> (* We can't expand those *) raise (Failure "Attempted to greedily expand a Vec or an Option ") - | T.Array _ -> raise Errors.Unimplemented + | T.Array _ -> raise Utils.Unimplemented | T.Slice _ -> raise (Failure "Can't expand symbolic slices") | T.TypeVar _ | Bool | Char | Never | Integer _ | Str -> raise (Failure "Unreachable") diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 83cdfc9b..5a6947b0 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -4,7 +4,7 @@ module V = Values module LA = LlbcAst open Scalars module E = Expressions -open Errors +open Utils module C = Contexts module Subst = Substitute module L = Logging diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 308f561c..56ab05f3 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -10,7 +10,7 @@ open TypesUtils open ValuesUtils module Inv = Invariants module S = SynthesizeSymbolic -open Errors +open Utils open Cps open InterpreterUtils open InterpreterProjectors diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 81879883..9899cfcf 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -707,7 +707,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) in (* Compute the set of ancestors of the function in call1 *) let call1_ancestors = - LlbcAstUtils.list_parent_region_groups sg rg_id1 + LlbcAstUtils.list_ancestor_region_groups sg rg_id1 in (* Check if the function used in call0 is inside *) T.RegionGroupId.Set.mem rg_id0 call1_ancestors diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index f393b059..1341bccc 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1,4 +1,4 @@ -open Errors +open Utils open LlbcAstUtils open Pure open PureUtils @@ -525,7 +525,7 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t) match bid with | None -> (None, T.RegionGroupId.Set.empty) | Some bid -> - let parents = list_parent_region_groups sg bid in + let parents = list_ancestor_region_groups sg bid in (Some bid, parents) in (* List the inputs for: @@ -1721,7 +1721,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) | None -> [] | Some back_id -> let parents_ids = - list_ordered_parent_region_groups def.signature back_id + list_ordered_ancestor_region_groups def.signature back_id in let backward_ids = List.append parents_ids [ back_id ] in List.concat diff --git a/compiler/dune b/compiler/dune index d3f5eaec..af4cdb08 100644 --- a/compiler/dune +++ b/compiler/dune @@ -18,7 +18,6 @@ Contexts Cps Crates - Errors Expressions ExpressionsUtils ExtractToFStar |