diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 22 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.mli | 2 |
2 files changed, 19 insertions, 5 deletions
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index c9bad3ef..39a17c25 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -620,12 +620,24 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) (* Retrieve the first id of the group *) match ids with | [] -> - (* We shouldn't get there: we actually introduce reborrows with - {!prepare_ashared_loans} and in the [match_mut_borrows] function - of {!MakeJoinMatcher} to introduce some fresh abstractions for - this purpose. + (* We *can* get there, if the loop doesn't touch the borrowed + values. + For instance: + {[ + pub fn iter_slice(a: &mut [u8]) { + let len = a.len(); + let mut i = 0; + while i < len { + i += 1; + } + } + ]} *) - raise (Failure "Unexpected") + log#ldebug + (lazy + ("No loop region to end for the region group " + ^ RegionGroupId.to_string rg_id)); + () | id0 :: ids -> let id0 = ref id0 in (* Add the proper region group into the abstraction *) diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli index 65a76359..c0e5dca5 100644 --- a/compiler/InterpreterLoopsFixedPoint.mli +++ b/compiler/InterpreterLoopsFixedPoint.mli @@ -56,6 +56,8 @@ val prepare_ashared_loans : loop_id option -> Cps.cm_fun - the map from region group id to the corresponding abstraction appearing in the fixed point (this is useful to compute the return type of the loop backward functions for instance). + Note that this is a partial map: the loop doesn't necessarily introduce + an abstraction for each input region of the function. Rem.: the list of symbolic values should be computable by simply exploring the fixed point environment and listing all the symbolic values we find. |