viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.55k stars 106 forks source link

Compiler shows `non_snake_case` warnings for internal `prusti_extern_spec_...` functions #1429

Open vfukala opened 1 year ago

vfukala commented 1 year ago

For

use prusti_contracts::*;

fn MY_FUNC() {}

#[extern_spec(crate)]
fn MY_FUNC();

fn main() {}

, Prusti output is

  __          __        __  ___             
 |__)  _\/_  |__) |  | /__`  |   ____\/_  | 
 |      /\   |  \ \__/ .__/  |       /\   | 

Prusti version: 0.2.2, commit d3dc99990e2 2023-06-26 14:59:58 UTC, built on 2023-07-01 23:37:13 UTC
warning: function `MY_FUNC` should have a snake case name
 --> bleh.rs:3:4
  |
3 | fn MY_FUNC() {}
  |    ^^^^^^^ help: convert the identifier to snake case: `my_func`
  |
  = note: `#[warn(non_snake_case)]` on by default

warning: function `prusti_extern_spec_MY_FUNC` should have a snake case name
 --> bleh.rs:6:4
  |
6 | fn MY_FUNC();
  |    ^^^^^^^ help: convert the identifier to snake case: `prusti_extern_spec_my_func`

Verification of 2 items...
Successful verification of 2 items
warning: 2 warnings emitted

, which warns about the prusti_extern_spec_MY_FUNC function, which I don't think the user should see.

The desugared specs are

#![feature(type_ascription)]
#![feature(stmt_expr_attributes)]
#![feature(register_tool)]
#![register_tool(prusti)]
#[prelude_import]
use std::prelude::rust_2018::*;
#[macro_use]
extern crate std;
use prusti_contracts::*;
fn MY_FUNC() {}
#[prusti::trusted]
#[prusti::specs_version = "0.1.8"]
#[prusti::extern_spec = "method"]
#[allow(unused, dead_code)]
fn prusti_extern_spec_MY_FUNC() { crate::MY_FUNC::<>() }
fn main() {}

, where the #[allow(...)] for prusti_extern_spec_MY_FUNC should probably also contain non_snake_case.

Aurel300 commented 1 year ago

This is similar to #1202, and the fix should be the same (#1269).