E8011

Error · Contract/Verification

E8011 — A pointer clause that is not well formed: requires valid(p, n), requires initialized(p, n) or requires !overlaps(p, q, n), where p and q are raw pointer parameters, and each clause is a requires of its own. A call through a function value or a trait would not prove the clause, so a safe function with one cannot be a function value, and a safe method of a trait impl cannot have one.

What the compiler reports

Error[E8011] at {{.*}}.vx:[[@LINE+2]]:12: `fill` is a method of an impl of `Fills`, so it must be an `unsafe fn` to have a pointer clause: a call through the trait would not prove the clause
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:9: a pointer clause in `ensures` is not supported yet: write it as a `requires`
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:10: write each pointer clause as a `requires` of its own, as in `requires valid(p, n)`
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:10: `valid` takes a raw pointer parameter and a length, as in `valid(p, n)`
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:10: only `!overlaps(p, q, n)` says something that the body can use
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:11: `!valid` says nothing that the body can use
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:10: `z` is not a parameter of `no_such_parameter`
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:10: `valid` needs a raw pointer, but `r` is `&i64`
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:11: `overlaps` needs two different pointers, but both are `p`
Error[E8011] at {{.*}}.vx:[[@LINE+2]]:12: `safe_with_a_clause` has a pointer `requires`, so it cannot be a function value yet: a call through the value would not prove the clause
10 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
//
//
// A pointer clause is a `requires` of its own: `valid(p, n)`, `initialized(p, n)` or
// `!overlaps(p, q, n)`, where `p` and `q` are raw pointer parameters. A safe function with one
// cannot be a function value, and a safe method of a trait impl cannot have one, because a call
// through the value or the trait would not prove the clause.

// The checks of the whole program come before the checks of the bodies.
trait Fills {
  fn fill(self : &Self, p : *mut i64, n : i64) -> void;
}

struct Filler {
  k : i64,
}

impl Fills for Filler {
  fn fill(self : &Filler, p : *mut i64, n : i64) -> void
  requires valid(p, n)
  {
    return;
  }
}

unsafe fn in_ensures(p : *mut i64) -> *mut i64
ensures valid(return, 1)
{
  return p;
}

unsafe fn inside_another_clause(p : *mut i64, n : i64) -> void
requires valid(p, n) && n > 0
{
  return;
}

unsafe fn no_length(p : *mut i64) -> void
requires valid(p)
{
  return;
}

unsafe fn overlaps_without_not(p : *mut i64, q : *mut i64) -> void
requires overlaps(p, q, 4)
{
  return;
}

unsafe fn not_valid(p : *mut i64) -> void
requires !valid(p, 4)
{
  return;
}

unsafe fn no_such_parameter(_p : *mut i64) -> void
requires valid(z, 4)
{
  return;
}

unsafe fn not_a_raw_pointer(r : &i64) -> void
requires valid(r, 1)
{
  return;
}

unsafe fn one_pointer_twice(p : *mut i64) -> void
requires !overlaps(p, p, 4)
{
  return;
}

fn safe_with_a_clause(p : *mut i64, n : i64) -> void
requires valid(p, n)
{
  return;
}

fn as_a_function_value() -> void {
  let _f = safe_with_a_clause;
}

fn main() -> i32 {
  return 0;
}

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

Related