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 174
    • Issues 174
    • 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
  • #18
Closed
Open
Issue 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