W1010

Warning

W1010 — An unsafe block with nothing inside it that needs unsafe.

What the compiler reports

Warning[W1010] at {{.*}}warning_for_unsafe_with_nothing_unsafe.vx:52:11: this `unsafe` block holds nothing that needs `unsafe`
Warning[W1010] at {{.*}}warning_for_unsafe_with_nothing_unsafe.vx:60:12: this `unsafe` block is inside another one

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
//
//
// An `unsafe` block with nothing inside that needs `unsafe` gets W1010, and so does one inside
// another `unsafe` block. Reading through a raw pointer, calling an `unsafe fn` or a C function,
// and turning an integer into a pointer all need `unsafe`, so those blocks get no warning. So does
// a call whose pointer `requires` the compiler cannot prove, which the block lets it trust.
// Neither does a block that declares a variable (Vx has no plain `{ .. }` block). `vec![..]`
// becomes an `unsafe` block the compiler writes, which never warns or counts as an outer block.

import std::vec;
import core::ops;

extern {
  fn c_abs(x: i32) -> i32;
}

unsafe fn read(p : *mut i32) -> i32 {
  let v = unsafe { *p };
  return v;
}

struct Cell {
  v : i32,
}

impl Cell {
  unsafe fn make(p : *mut i32) -> Cell {
    let v = unsafe { *p };
    return Cell {
      v : v
    };
  }
}

fn main() -> i32 {
  let mut x : i32 = 1;
  let mut y : i32 = 2;
  let p : *mut i32 = &mut y;
  let a = unsafe { x + 1 };
  let b = unsafe { *p };
  let c = unsafe { read(p) };
  let d = unsafe { c_abs(0 - 3) };
  let _q = unsafe { 0 as *mut i32 };
  // The second call finds the function the first call made, a different path in the checker.
  let first = unsafe { Cell::make(p) };
  let second = unsafe { Cell::make(p) };
  unsafe { unsafe { x = *p; } }
  unsafe { let x = 5; print(x); }
  let pair = vec![b, unsafe { *p }];
  print(pair.len());
  let e = unsafe { first_of(p as *const i32, 2i64) };
  return a + b + c + d + e + first.v + second.v;
}

fn first_of(q : *const i32, n : i64) -> i32
requires valid(q, n)
{
  return unsafe { q[0] };
}

From tests/frontend/pass/warning_for_unsafe_with_nothing_unsafe.vx, which asserts this diagnostic on every commit.

Related