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
  • #1019

Closed
Open
Created Jun 16, 2014 by mantis-gitlab-migration@mantis-gitlab-migration

Assigns not respected in behaviors when using pointers to pointers

ID0001812: This issue was created automatically from Mantis Issue 1812. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001812 Frama-C Plug-in > wp public 2014-06-16 2014-06-17
Reporter Ian Assigned To correnson Resolution open
Priority normal Severity minor Reproducibility always
Platform - OS Ubuntu OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version -

Description :

Assigns defined in behaviors are not always respected. The example provided shows an assigns defined in complete behaviors that causes a different results than if defined outside the behaviors. The results are expected to be the same since the behaviors are complete.

Steps To Reproduce :

Create file (attached: invalid.c):

/*@
  @ requires \valid(a) && \valid(*a) && \separated(a, *a);
  @ behavior all:
  @     assumes \true;
  @     assigns **a;
  @ complete behaviors all;
  @*/
void set_next_next(int **a){
    **a = 0;
}

void main(){
    int **a, *b, c;
    b = &c; 
    a = &b; 

    pre_fct:

    set_next_next(a);
    //@ assert b == \at(b, pre_fct);
}

Run:

frama-c -cpp-command 'gcc -C -E' -wp invalid.c

Result: Assertion in main does not validate.

By moving the assigns statement outside the behavior, the assertion is validated:

/*@
  @ requires \valid(a) && \valid(*a) && \separated(a, *a);
  @ assigns **a;
  @ behavior all:
  @     assumes \true;
  @ complete behaviors all;
  @*/

Attachments

  • invalid.c
  • valid.c
Edited Aug 05, 2021 by Allan Blanchard
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking