GitLab

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