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

« back to all changes in this revision

Viewing changes to tests/jessie/permut_search2.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/permut_search2.c

 

1

/*@ axiomatic PermutSize {

 

2

  @  logic int permut_size{Here}(int *arr); 

 

3

  @    // reads arr[0..];

 

4

  @  axiom permut_valid{Here}:

 

5

  @    \forall int *arr; 

 

6

  @      0 <= permut_size(arr) ==> \valid_range(arr,0,permut_size(arr));

 

7

  @  axiom permut_bound{Here}:

 

8

  @    \forall integer i; \forall int *arr; 

 

9

  @      0 <= i <= permut_size(arr) ==> 0 <= arr[i] <= permut_size(arr);

 

10

  @ }

 

11

  @*/

 

12

 

 

13

//@ requires 0 <= permut_size(arr);

 

14

int permut_search(int *arr, int v) {

 

15

  int idx = 0;

 

16

  //@ loop invariant 0 <= idx <= permut_size(arr);

 

17

  while (1) {

 

18

    if (arr[idx] == v) return idx;

 

19

    idx = arr[idx];

 

20

  }

 

21

} 

• Older »

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