GitLab

In the function below, WP fails to verify the assertion (which I believe is true after exhaustively testing it):

/*@ assigns \nothing;
  @*/
int8_t foo(int8_t n) {
    int8_t m = n & 0xF;
    /*@ assert 0 <= m < 16; */
    return m;
}

It does so with all signed integer types, but doesn't with unsigned integer types. Performing the & on an unsigned integer type and casting the result to a signed integer doesn't work either. For instance, in the function below, the first assertion is verified but not the second:

int8_t bar(int8_t n) {
    uint8_t m = n & 0xF;
    /*@ assert 0 <= m < 16; */
    int8_t p = m;
    /*@ assert 0 <= p < 16; */
    return p;
}

Test file: test.c

I used this command to run Frama-C:

frama-c -wp -wp-rte test.c -wp-prover why3:alt-ergo -wp-prover why3:cvc4 -wp-prover why3:Z3

Contextual information

• Frama-C installation mode: Opam
• Frama-C version: 24.0
• Plug-in used: WP, RTE
• OS name: Fedora
• OS version: 35
• Solvers: Alt-Ergo 2.4.1, CVC4 1.8, Z3 4.8.11

Additional information (optional)