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

« back to all changes in this revision

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

 

1

/* run.config

 

2

   DONTRUN: cast no working yet

 

3

*/

 

4

#pragma IntModel(modulo)

 

5

 

 

6

#include <limits.h>

 

7

 

 

8

//@ requires 0 < size < 10 && \valid_range((char*)p,0,4*size-1);

 

9

void f(int* p, int size) {

 

10

  char* c = (char*) p;

 

11

  int i = 0;

 

12

  //@ loop invariant i >= 0;

 

13

  while (i < size * sizeof(int)) {

 

14

    c[i] = 0;

 

15

    ++i;

 

16

  }

 

17

}

 

18

 

 

19

//@ requires \valid(p) && \valid(q);

 

20

void g(int* p, int* q) {

 

21

  char* c = (char*) p;

 

22

  char* d = (char*) q;

 

23

  c[0] = d[0];

 

24

  c[1] = d[1];

 

25

  c[2] = d[2];

 

26

  c[3] = d[3];

 

27

  //@ assert (*c == *d);

 

28

}

 

29

 

 

30

/* 

 

31

Local Variables:

 

32

compile-command: "LC_ALL=C make cast_to_bytes"

 

33

End:

 

34

*/

• Older »

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