prusti-dev
prusti-dev copied to clipboard
Compiler shows `non_snake_case` warnings for internal `prusti_extern_spec_...` functions
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.
This is similar to #1202, and the fix should be the same (#1269).