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

« back to all changes in this revision

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

 

1

 

 

2

/*@ axiomatic CountBits {

 

3

  @   // the i-th bit of x as 0 or 2^i

 

4

  @   logic integer bit(integer x, integer i);

 

5

  @   // the number of bits 1 in x

 

6

  @   logic integer nbits(integer x);

 

7

  @   axiom nbits_nonneg : \forall integer x; nbits(x) >= 0;

 

8

  @   axiom nbits_zero : nbits(0) == 0;

 

9

  @   // the lowest bit 1 in x

 

10

  @   logic integer lowest_bit(integer x);

 

11

  @   axiom lowest_bit_def :

 

12

  @     \forall integer x; x != 0 ==>

 

13

  @        \exists integer i; 

 

14

  @           i >= 0 &&

 

15

  @           lowest_bit(x) == bit(x,i) &&

 

16

  @           bit(x,i) != 0 &&

 

17

  @           \forall integer j; 0 <= j < i ==> bit(x,j) == 0;

 

18

  @   axiom lowest_bit_zero :

 

19

  @     \forall integer x; lowest_bit(x) == 0 <==> x == 0;

 

20

  @   axiom lowest_bit_trick :

 

21

  @     \forall integer x; (x & -x) == lowest_bit(x);

 

22

  @   axiom remove_one_bit :

 

23

  @      \forall integer x, integer i;

 

24

  @         bit(x,i) != 0 ==> nbits((int)(x - bit(x,i))) == nbits(x) - 1;

 

25

  @ }

 

26

  @*/

 

27

 

 

28

/*@ ensures \result == nbits(x); */

 

29

int count_bits(int x) {

 

30

  int d, c;

 

31

  /*@ loop invariant c + nbits(x) == nbits(\at(x,Pre));

 

32

    @ loop variant   nbits(x);

 

33

    @*/

 

34

  for (c = 0; d = x&-x; x -= d) c++;

 

35

  return c;

 

36

}

 

37

 

 

38

 

 

39

/* 

 

40

Local Variables:

 

41

compile-command: "LC_ALL=C make count_bits"

 

42

End:

 

43

*/

• Older »

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