CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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);
23void *mmap64(void *, __CPROVER_size_t, int, int, int, off_t);
24
25void *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);
60void *mmap64(void *, __CPROVER_size_t, int, int, int, off_t);
61
62void *_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
98void *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
132int 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
145int _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
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
__CPROVER_allocated_memory
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent)
_mmap
void * _mmap(void *addr, __CPROVER_size_t length, int prot, int flags, int fd, off_t offset)
Definition mman.c:62
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
mmap
void * mmap(void *addr, __CPROVER_size_t length, int prot, int flags, int fd, off_t offset)
Definition mman.c:25
__VERIFIER_nondet___CPROVER_bool
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void)
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