Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • 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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • 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
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