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; @/