Skip to content

GitLab

  • Menu
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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • 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
  • #18

Closed
Open
Created Jun 15, 2020 by Alex Coffin@GreenBeard

WP: Incorrect assigns global/static handling

View all of the following goals succeed for the following program:

#include <assert.h>

unsigned int number = 0;

/*@
  assigns number;
  ensures \valid(\result);
*/
unsigned int* a_num(void) {
  ++number;
  return &number;
}

void test_a_num(void) {
  unsigned int* a = a_num();
  unsigned int copy = *a;
  assert(copy == *a);
  unsigned int* b = a_num();
  assert(copy == *a);
}

int main(int argc, char** argv) {
  test_a_num();

  return 0;
}

compiled with frama-c-gui -wp -wp-rte -wp-smoke-tests test.c

Expected behaviour

The second assert function call fails when run, and therefore WP should not be able to prove its preconditions.

Actual behaviour

It claims that it has proven (incorrectly) that the assert function call will be successful. Of course the assert calls may be replaced with /*@ assert */ statements instead, and it still claims that they pass.

Fix ideas

Check handling of static/global variables with assigns?

Edited Jun 15, 2020 by Loïc Correnson
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking