Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2589
Closed
Open
Issue created Jan 03, 2022 by GuerricChupin@GuerricChupin

[WP] Failure to verify range information after bitwise and on signed integers

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)

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking