~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to tests/jessie/array_field_addr.c

• browse files at revision 1
• compare with another revision
• download diff
• download tarball
• view history from revision 1

Show diffs side-by-side

added

removed

tests/jessie/array_field_addr.c

 

1

 

 

2

struct t {

 

3

  int tab[5];

 

4

};

 

5

 

 

6

/*@ requires \valid(i);

 

7

  @ ensures *i == 1;

 

8

  @ */

 

9

void g(int* i) {

 

10

  *i = 1;

 

11

}

 

12

 

 

13

/*@ requires \valid(a) && \valid_range(a->tab,0,4); */

 

14

void f(struct t* a) {

 

15

  g (&a->tab[0]);

 

16

  //@ assert a->tab[0] == 1;

 

17

}

 

18

 

 

19

/* 

 

20

Local Variables:

 

21

compile-command: "LC_ALL=C make array_field_addr"

 

22

End:

 

23

*/

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1