No warnings shown for library methods

[ple1n]

#![feature(decl_macro)]
#![allow(unused)]
#![allow(non_snake_case)]


pub fn a() {
    verify!(false)
}

impl<S: NodeStatusT, A, GS, RKey: Key, SK: SKey> AsyncScheduler<S, A, GS, RKey, SK> {
    pub fn upkeep(&mut self, immutable: &GS, mutable: &mut A) {
        let k = 0;
        // set_model_field!(k, f, 2);
        verify!(false);
    }

hash@hash-pc /s/n/async_scheduler (master)> MIRAI_FLAGS=--diag=paranoid cargo mirai
    Checking async_scheduler v0.1.0 (/space/netns-proxy/async_scheduler)
warning: provably false verification condition
   --> src/lib.rs:150:5
    |
150 |     verify!(false)
    |     ^^^^^^^^^^^^^^

warning: `async_scheduler` (lib) generated 1 warning
    Finished dev [unoptimized + debuginfo] target(s) in 0.22s

I've tried every way I can imagine to make it work, but it doesn't.

[package]
name = "async_scheduler"
version = "0.1.0"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
anyhow = "1.0.75"
bimap = "0.6.3"

daggy = "0.8.0"
derivative = "2.2.0"
fixedbitset = "0.4.2"
mirai-annotations = "1.12.0"
rustsat = { version = "0.2.1", features = ["multiopt"] }
rustsat-minisat = "0.1.1"
scuttle = { version = "0.2.0", default-features = false }
contracts = { version = "0.6.3", features = ["mirai_assertions"] }

Is this project maintained ?

Or, it doesn't work with struct with generics.

Another irking behavior is that it doesn't take environment variables when it has cache of some kind. I have to run cargo clean so it takes up the changes to env vars.

[hermanventer]

The issue with the environmental variable seems real. cargo will rebuild things when it detects changes in compiler flags, but it happily ignores MIRAI_FLAGS. That is probably fixable.

By default, MIRAI will only show you diagnostics for source locations rooted in the crate being built. That is a very much a feature. I am none too sure what you are trying to do here, so I can't say off hand whether this is an issue that needs fixing. Can you add some details in the form of an actual project that I can debug?

[ple1n]

https://github.com/planetoryd/mirai_issue/blob/master/src/lib.rs

It doesn't work with structs with generics.

I just found another issue, it suppresses diagnostics if with print_function_names, which I think is inconsistent

hash@hash-pc /s/mirai_issue (master)> cargo clean
hash@hash-pc /s/mirai_issue (master)> MIRAI_FLAGS="--diag=paranoid" cargo mirai
   Compiling proc-macro2 v1.0.67
   Compiling unicode-ident v1.0.12
   Compiling syn v1.0.109
    Checking mirai-annotations v1.12.0
   Compiling quote v1.0.33
   Compiling contracts v0.6.3
    Checking mirai_issue v0.1.0 (/space/mirai_issue)
warning: provably false verification condition
 --> src/lib.rs:7:5
  |
7 |     verify!(false);
  |     ^^^^^^^^^^^^^^

warning: provably false verification condition
  --> src/lib.rs:14:9
   |
14 |         verify!(false)
   |         ^^^^^^^^^^^^^^

warning: `mirai_issue` (lib) generated 2 warnings
    Finished dev [unoptimized + debuginfo] target(s) in 3.78s
hash@hash-pc /s/mirai_issue (master)> cargo clean
hash@hash-pc /s/mirai_issue (master)> MIRAI_FLAGS="--print_function_names --diag=paranoid" cargo mirai
   Compiling proc-macro2 v1.0.67
   Compiling unicode-ident v1.0.12
   Compiling syn v1.0.109
    Checking mirai-annotations v1.12.0
   Compiling quote v1.0.33
   Compiling contracts v0.6.3
    Checking mirai_issue v0.1.0 (/space/mirai_issue)
src/lib.rs:6:1: 6:17 (#0): /mirai_issue/working()->()
src/lib.rs:13:5: 13:30 (#0): /mirai_issue/Empty::without_generics()->()
src/lib.rs:21:5: 21:27 (#0): /mirai_issue/Gen::<T>::with_generics()->()
    Finished dev [unoptimized + debuginfo] target(s) in 3.82s

[hermanventer]

print_function_names is a very specialized use of MIRAI. Also, printing diagnostics does not seem universally expected and would not be welcomed by the principal users of the feature.

[hermanventer]

It doesn't work with structs with generics.

See https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Overview.md#entry-points

[ple1n]

It also doesn't work with tests. https://github.com/planetoryd/mirai_issue/blob/53f4884353344e6dac42e9a0bfe68023ec5cd7db/src/lib.rs#L32 (updated code)

[hermanventer]

It also doesn't work with tests. https://github.com/planetoryd/mirai_issue/blob/53f4884353344e6dac42e9a0bfe68023ec5cd7db/src/lib.rs#L32 (updated code)

See #1239