Frama-C Bug Tracking System - Frama-C
View Issue Details
0001812Frama-CPlug-in > wppublic2014-06-16 22:552014-06-17 11:02
Frama-C Neon-20140301 
0001812: Assigns not respected in behaviors when using pointers to pointers
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.
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; @*/
No tags attached.
related to 0001461acknowledged correnson assigns, loop assigns and loop invariant 
related to 0001638acknowledged correnson assigns clause appears unprovable 
c invalid.c (339) 2014-06-16 22:55
c valid.c (335) 2014-06-16 22:57
Issue History
2014-06-16 22:55IanNew Issue
2014-06-16 22:55IanStatusnew => assigned
2014-06-16 22:55IanAssigned To => correnson
2014-06-16 22:55IanFile Added: invalid.c
2014-06-16 22:57IanFile Added: valid.c
2014-06-17 10:58corrensonNote Added: 0005229
2014-06-17 10:58corrensonStatusassigned => acknowledged
2014-06-17 10:58corrensonNote Edited: 0005229View Revisions
2014-06-17 11:00corrensonNote Edited: 0005229View Revisions
2014-06-17 11:02corrensonRelationship addedrelated to 0001461
2014-06-17 11:02corrensonRelationship addedrelated to 0001638

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.