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

« back to all changes in this revision

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

 

1

/* run.config

 

2

   DONTRUN: cast not supported yet

 

3

*/

 

4

 

 

5

#pragma SeparationPolicy(Regions)

 

6

 

 

7

/*@ requires \valid(s);

 

8

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

 

9

  @*/

 

10

void reverse_endian(short *s) {

 

11

  char *c = (char*)s;

 

12

  char tmp = *c;

 

13

  *c = *(c+1);

 

14

  *(c+1) = tmp;

 

15

}

 

16

 

 

17

/*

 

18

Local Variables:

 

19

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

 

20

End:

 

21

*/

• Older »

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