Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001812Frama-CPlug-in > wppublic2014-06-16 22:552014-06-17 11:02
ReporterIan 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSUbuntuOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001812: Assigns not respected in behaviors when using pointers to pointers
DescriptionAssigns 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 ReproduceCreate 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;
  @*/
TagsNo tags attached.
Attached Filesc file icon invalid.c [^] (339 bytes) 2014-06-16 22:55 [Show Content]
c file icon valid.c [^] (335 bytes) 2014-06-16 22:57 [Show Content]

- Relationships
related to 0001461acknowledgedcorrenson assigns, loop assigns and loop invariant 
related to 0001638acknowledgedcorrenson assigns clause appears unprovable 

-  Notes
(0005229)
correnson (manager)
2014-06-17 10:58
edited on: 2014-06-17 11:00

This is a known limitation of WP.
We are working on this topics.

The usual workaround is to specify one global large assign in the default behavior,
then refine it using ensures clauses to preserve equalities locally.

The same remark applies to loop invariants.


- Issue History
Date Modified Username Field Change
2014-06-16 22:55 Ian New Issue
2014-06-16 22:55 Ian Status new => assigned
2014-06-16 22:55 Ian Assigned To => correnson
2014-06-16 22:55 Ian File Added: invalid.c
2014-06-16 22:57 Ian File Added: valid.c
2014-06-17 10:58 correnson Note Added: 0005229
2014-06-17 10:58 correnson Status assigned => acknowledged
2014-06-17 10:58 correnson Note Edited: 0005229 View Revisions
2014-06-17 11:00 correnson Note Edited: 0005229 View Revisions
2014-06-17 11:02 correnson Relationship added related to 0001461
2014-06-17 11:02 correnson Relationship added related to 0001638


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker