CBMC
mman.c
Go to the documentation of this file.
1 /* FUNCTION: mmap */
2 
3 #ifndef _WIN32
4 
5 # ifndef __CPROVER_SYS_MMAN_H_INCLUDED
6 # include <sys/mman.h>
7 # define __CPROVER_SYS_MMAN_H_INCLUDED
8 # endif
9 
10 # ifndef MAP_FIXED
11 # define MAP_FIXED 0
12 # endif
13 
14 # ifndef MAP_ANONYMOUS
15 # define MAP_ANONYMOUS 0
16 # endif
17 
18 # ifndef MAP_UNINITIALIZED
19 # define MAP_UNINITIALIZED 0
20 # endif
21 
22 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
23 void *mmap64(void *, __CPROVER_size_t, int, int, int, off_t);
24 
25 void *mmap(
26  void *addr,
27  __CPROVER_size_t length,
28  int prot,
29  int flags,
30  int fd,
31  off_t offset)
32 {
33  return mmap64(addr, length, prot, flags, fd, offset);
34 }
35 
36 #endif
37 
38 /* FUNCTION: _mmap */
39 
40 #ifndef _WIN32
41 
42 # ifndef __CPROVER_SYS_MMAN_H_INCLUDED
43 # include <sys/mman.h>
44 # define __CPROVER_SYS_MMAN_H_INCLUDED
45 # endif
46 
47 # ifndef MAP_FIXED
48 # define MAP_FIXED 0
49 # endif
50 
51 # ifndef MAP_ANONYMOUS
52 # define MAP_ANONYMOUS 0
53 # endif
54 
55 # ifndef MAP_UNINITIALIZED
56 # define MAP_UNINITIALIZED 0
57 # endif
58 
59 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
60 void *mmap64(void *, __CPROVER_size_t, int, int, int, off_t);
61 
62 void *_mmap(
63  void *addr,
64  __CPROVER_size_t length,
65  int prot,
66  int flags,
67  int fd,
68  off_t offset)
69 {
70  return mmap64(addr, length, prot, flags, fd, offset);
71 }
72 
73 #endif
74 
75 /* FUNCTION: mmap64 */
76 
77 #ifndef _WIN32
78 
79 # ifndef __CPROVER_SYS_MMAN_H_INCLUDED
80 # include <sys/mman.h>
81 # define __CPROVER_SYS_MMAN_H_INCLUDED
82 # endif
83 
84 # ifndef MAP_FIXED
85 # define MAP_FIXED 0
86 # endif
87 
88 # ifndef MAP_ANONYMOUS
89 # define MAP_ANONYMOUS 0
90 # endif
91 
92 # ifndef MAP_UNINITIALIZED
93 # define MAP_UNINITIALIZED 0
94 # endif
95 
96 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
97 
98 void *mmap64(
99  void *addr,
100  __CPROVER_size_t length,
101  int prot,
102  int flags,
103  int fd,
104  off_t offset)
105 {
106  (void)prot;
107  (void)fd;
108  (void)offset;
109 
110  if(
111  addr == 0 ||
112  (__VERIFIER_nondet___CPROVER_bool() && (flags & MAP_FIXED) == 0))
113  {
114  if(flags & MAP_ANONYMOUS && (flags & MAP_UNINITIALIZED) == 0)
115  return __CPROVER_allocate(length, 1);
116  else
117  return __CPROVER_allocate(length, 0);
118  }
119  else
120  {
121  __CPROVER_allocated_memory((__CPROVER_size_t)addr, length);
122  return addr;
123  }
124 }
125 
126 #endif
127 
128 /* FUNCTION: munmap */
129 
130 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
131 
132 int munmap(void *addr, __CPROVER_size_t length)
133 {
134  (void)length;
135 
136  __CPROVER_deallocate(addr);
137 
138  return 0;
139 }
140 
141 /* FUNCTION: _munmap */
142 
143 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
144 
145 int _munmap(void *addr, __CPROVER_size_t length)
146 {
147  (void)length;
148 
149  __CPROVER_deallocate(addr);
150 
151  return 0;
152 }
__CPROVER_allocate
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
__CPROVER_deallocate
void __CPROVER_deallocate(void *)
Definition: stdlib.c:670
__CPROVER_allocated_memory
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent)
MAP_UNINITIALIZED
#define MAP_UNINITIALIZED
Definition: mman.c:19
MAP_FIXED
#define MAP_FIXED
Definition: mman.c:11
_munmap
int _munmap(void *addr, __CPROVER_size_t length)
Definition: mman.c:145
__VERIFIER_nondet___CPROVER_bool
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void)
_mmap
void * _mmap(void *addr, __CPROVER_size_t length, int prot, int flags, int fd, off_t offset)
Definition: mman.c:62
munmap
int munmap(void *addr, __CPROVER_size_t length)
Definition: mman.c:132
mmap64
void * mmap64(void *, __CPROVER_size_t, int, int, int, off_t)
Definition: mman.c:98
MAP_ANONYMOUS
#define MAP_ANONYMOUS
Definition: mman.c:15
mmap
void * mmap(void *addr, __CPROVER_size_t length, int prot, int flags, int fd, off_t offset)
Definition: mman.c:25