E8014

Error · Contract/Verification

E8014 — Code outside the module of a type with an invariant changes a field of the type. Only the module (the .vx file) that declares the type can write a field, take a &mut to a field, call a method that takes &mut self on a field, move a field out of the value, or build the type with a struct literal. Other code calls a function of the module to change a value of the type. Then the invariant holds for each value of the type outside its module.

What the compiler reports

Error[E8014] at {{.*}}.vx:[[@LINE+1]]:5: this assignment changes the field `len` of `Vec`. `Vec` has an invariant, so only code in `vec.vx` can change its fields{{$}}
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:5: this assignment changes the field `len` of `Vec`.
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:5: this assignment changes the field `len` of `Vec`.
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:18: this `&mut` can change the field `capacity` of `Vec`. `Vec` has an invariant, so only code in `vec.vx` can change its fields{{$}}
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:7: this assignment changes the field `len` of `Vec`.
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:11: this struct literal builds a `Vec`. `Vec` has an invariant, so only code in `vec.vx` can build it from its fields{{$}}
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:5: this assignment changes the field `lo` of `Interval`. `Interval` has an invariant, so only code in `interval_with_an_invariant.vx` can change its fields{{$}}
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:5: this assignment changes the field `count` of `Interval`.
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:5: `bump` takes `&mut self`, so it can change the field `count` of `Interval`.
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:5: `push` takes `&mut self`, so it can change the field `items` of `Interval`.
Error[E8014] at {{.*}}.vx:[[@LINE+1]]:17: this move leaves no value in the field `items` of `Interval`.

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
//
//
// `Vec` and `Interval` have invariants, and other files declare them. So this file cannot change
// their fields, and each change below gets E8014.
import std::vec;
import tests::modules::interval_with_an_invariant;

struct Wrapper {
  v : Vec<i64>,
}

fn through_a_reference(r : &mut Vec<i64>) -> i32 {
  r.len = 0;
  return 0;
}

fn main() -> i32 {
  let mut v = Vec<i64>::new();
  v.push(1i64);
  v.len = 100000000;
  v.len += 1;
  let c = &mut v.capacity;
  *c = 5;
  let mut w = Wrapper {
    v : Vec<i64>::new()
  };
  w.v.len = 3;
  let u = Vec<i64> {
    data : v.data, len : 0, capacity : 0
  };
  let mut i = Interval::new();
  i.lo = 5i64;
  // `Counter` has no invariant, but this `Counter` is a field of an `Interval`.
  i.count.value = 3i64;
  i.count.bump();
  i.items.push(2i64);
  let j = Interval::new();
  let items = j.items;
  println!("{} {} {} {}", v.len, u.len, i.lo, items.len);
  return 0;
}

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

Related