False Positive during Constant Time Analysis

[aproppos]

Issue

When performing a constant time analysis on a simple caesar's cipher with a precondition specifying no tag is present, it reports warning: the branch condition may have a SecretTaintKind tag.

Steps to Reproduce

The following code produces the warning:

pub fn caesars_cipher(mut message : Vec<u8>) {
        precondition!(does_not_have_tag!(&message, crate::SecretTaint));
        for m in 0..message.len()-1 {
            message[m] = message[m] + 1;
        }
    }

SecretTaint is created with: type SecretTaint = SecretTaintKind<TAG_PROPAGATION_ALL>;

Expected Behavior

As there is an explicit pre-condition that says there is no tag present, this code should produce no warnings about a constant time analysis.

Actual Results

The following warning is produced:

warning: the branch condition may have a SecretTaintKind tag
   --> src/lib.rs:114:13
    |
114 |         for m in 0..message.len()-1 {
    | 

Environment

Rust version: rustc 1.54.0-nightly (bacf770f2 2021-05-05)
MIRAI version: 3dbc36c - Generalize union field assignment (#889)

[hermanventer]

I'm looking to see what I can do about this, but it may take a while.