Skip to content

Commit

Permalink
Improve comment.
Browse files Browse the repository at this point in the history
  • Loading branch information
yannbolliger committed May 26, 2021
1 parent 8956844 commit 92d8c6e
Showing 1 changed file with 6 additions and 3 deletions.
9 changes: 6 additions & 3 deletions stainless_extraction/src/expr/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -358,10 +358,13 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
}

/// Inserts a fresh copy around the expression, if the expression can contain
/// mutable types. This function must only be called, when it is safe to add a
/// fresh copy.
/// mutable types.
/// Currently, this is safe everywhere because:
/// - we either work on an immutable reference aka shared borrow aka `&T`
/// - or we own the the value, meaning it's moved when we return/alias it somewhere
/// and the compiler has made sure that it's not used afterwards.
///
/// TODO: Check that fresh copy is safe for expression.
/// TODO: Check that this is still safe (at call sites) when mutable references are introduced.
fn extract_aliasable_expr(&mut self, expr: &'a Expr<'a, 'tcx>) -> st::Expr<'l> {
let e = self.extract_expr(expr);
let tpe = self.base.extract_ty(expr.ty, &self.txtcx, expr.span);
Expand Down

0 comments on commit 92d8c6e

Please sign in to comment.