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

« back to all changes in this revision

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

 

1

/* run.config

 

2

   DONTRUN: cast not supported yet

 

3

*/

 

4

 

 

5

#pragma SeparationPolicy(Regions)

 

6

 

 

7

/*@ axiom little_endian_low_byte_short{L}: 

 

8

  @   \forall short *s; *(char*)s == *s % 256;

 

9

  @   

 

10

  @ axiom little_endian_high_byte_short{L}: 

 

11

  @   \forall short *s; *((char*)s+1) == *s / 256;

 

12

  @*/

 

13

 

 

14

/*@ axiom div_modulo:

 

15

  @   \forall integer i; i == 256 * (i / 256) + i % 256;

 

16

  @*/

 

17

 

 

18

/*@ requires \valid_range(x,0,1);

 

19

  @ ensures x[0] == \old(x[1]) && x[1] == \old(x[0]);

 

20

  @*/

 

21

void swap(char *x) {

 

22

  char tmp = *x;

 

23

  x[0] = x[1];

 

24

  x[1] = tmp;

 

25

}

 

26

 

 

27

/*@ requires \valid(s);

 

28

  @ ensures *s == 256 * (\old(*s) % 256) + (\old(*s) / 256);

 

29

  @*/

 

30

void reverse_endian(short *s) {

 

31

  char *c = (char*)s;

 

32

  swap(c);

 

33

}

 

34

 

 

35

/*

 

36

Local Variables:

 

37

compile-command: "LC_ALL=C make -j reverse_endian3"

 

38

End:

 

39

*/

• Older »

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