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

« back to all changes in this revision

Viewing changes to tests/spec/assigns.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/spec/assigns.c

 

1

struct list {

 

2

  int hd;

 

3

  struct list *next;

 

4

};

 

5

 

 

6

/*@ predicate reachable{L}(struct list *root, struct list *to) =

 

7

  @   root == to || root != \null && reachable(root->next,to) ;

 

8

  @*/

 

9

 

 

10

//@ assigns *p;

 

11

void reset(int *p) { *p = 0; }

 

12

 

 

13

// three equivalent assigns clauses

 

14

//@ assigns t[0..n-1];

 

15

void reset_array1(int t[],int n) {

 

16

  int i;

 

17

  for (i=0; i < n; i++) t[i] = 0;

 

18

}

 

19

 

 

20

//@ assigns *(t+(0..n-1));

 

21

void reset_array2(int t[],int n) {

 

22

  int i;

 

23

  for (i=0; i < n; i++) t[i] = 0;

 

24

}

 

25

 

 

26

//@ assigns *(t+{ i | int i ; 0 <= i < n });

 

27

void reset_array3(int t[],int n) {

 

28

  int i;

 

29

  for (i=0; i < n; i++) t[i] = 0;

 

30

}

 

31

 

 

32

//@ assigns { q->hd | struct list *q ; reachable(p,q) };

 

33

void incr_list(struct list *p) {

 

34

  while (p) { p->hd++ ; p = p->next; }

 

35

}

• Older »

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