E4016

Error · Borrow/Ownership

E4016 — A borrow clause that is not well formed, or one that the body does not keep. In ensures !points_into(return, *p) the result cannot point into the memory under *p, and in ensures !reaches(return, *p) it also cannot point where a reference in *p points. In ensures !keeps(p) the body stores p, or a reference read through it, nowhere that outlives the call. p is a reference parameter. Each borrow clause is an ensures of its own.

What the compiler reports

Error[E4016] at {{.*}}.vx:[[@LINE+2]]:11: `Wrong::first` says `!reaches(return, *key)`, but the result can point into `*key`
Error[E4016] at {{.*}}.vx:[[@LINE+1]]:11: `Renamed::first` says `!reaches(return, *k)`, but the result can point into `*k`
Error[E4016] at {{.*}}.vx:[[@LINE+1]]:11: `Plain::pick` says `!reaches(return, *key)`, but the result can point into `*key`
3 error(s) emitted

The fragments the test suite holds the compiler to. An ellipsis marks text the test does not constrain; the emitted message also carries a source location.

A program that triggers it

//
// Part of the Vx Project, under the Apache License v2.0 with LLVM Exceptions.
// See LICENSE for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//
// Each impl of a trait method must keep the borrow clauses of the trait. The error names the impl
// and points at the clause in the trait. An impl that names a parameter differently gets the
// clause with its own name. A default body that an impl gets must keep the clause too.

trait Source {
  fn first(self : &Self, key : &i64) -> &i64
  ensures !reaches(return, *key);
}

struct Wrong {
  n : i64,
}

impl Source for Wrong {
  fn first(self : &Wrong, key : &i64) -> &i64 {
    return key;
  }
}

struct Renamed {
  n : i64,
}

impl Source for Renamed {
  fn first(self : &Renamed, k : &i64) -> &i64 {
    return k;
  }
}

trait Pick {
  fn pick(self : &Self, key : &i64) -> &i64
  ensures !reaches(return, *key)
  {
    return key;
  }
}

struct Plain {
  n : i64,
}

impl Pick for Plain {}

fn main() -> i32 {
  let w = Wrong {
    n : 1i64
  };
  let r = Renamed {
    n : 2i64
  };
  let p = Plain {
    n : 3i64
  };
  let x = 3i64;
  return (*w.first(&x) + *r.first(&x) + *p.pick(&x)) as i32;
}

From tests/frontend/fail/an_impl_that_breaks_a_clause_of_its_trait.vx, which asserts this diagnostic on every commit.

Ownership and borrowingThe chapter covering the rule this code enforces. All diagnosticsEvery code the compiler can emit, grouped by stage. E4015A spawn region that moves a value from the code around it: let x = t; or f(t) with a parameter that takes t by value, where t is declared before the region. The region only borrows what it uses, and the function drops t after the region. Borrow it (&t), or clone it (t.clone()).

E4016

What the compiler reports

A program that triggers it

Related