CBMC
setjmp.c
Go to the documentation of this file.
1 
2 /* FUNCTION: longjmp */
3 
4 #ifndef __CPROVER_SETJMP_H_INCLUDED
5 #include <setjmp.h>
6 #define __CPROVER_SETJMP_H_INCLUDED
7 #endif
8 
9 void longjmp(jmp_buf env, int val)
10 {
11  // does not return
12  (void)env;
13  (void)val;
14  __CPROVER_assert(0, "longjmp requires instrumentation");
15  __CPROVER_assume(0);
16 #ifdef LIBRARY_CHECK
17  __builtin_unreachable();
18 #endif
19 }
20 
21 /* FUNCTION: _longjmp */
22 
23 #ifndef __CPROVER_SETJMP_H_INCLUDED
24 #include <setjmp.h>
25 #define __CPROVER_SETJMP_H_INCLUDED
26 #endif
27 
28 void _longjmp(jmp_buf env, int val)
29 {
30  // does not return
31  (void)env;
32  (void)val;
33  __CPROVER_assert(0, "_longjmp requires instrumentation");
34  __CPROVER_assume(0);
35 #ifdef LIBRARY_CHECK
36  __builtin_unreachable();
37 #endif
38 }
39 
40 /* FUNCTION: siglongjmp */
41 
42 #ifndef _WIN32
43 
44 #ifndef __CPROVER_SETJMP_H_INCLUDED
45 #include <setjmp.h>
46 #define __CPROVER_SETJMP_H_INCLUDED
47 #endif
48 
49 void siglongjmp(sigjmp_buf env, int val)
50 {
51  // does not return
52  (void)env;
53  (void)val;
54  __CPROVER_assert(0, "siglongjmp requires instrumentation");
55  __CPROVER_assume(0);
56 #ifdef LIBRARY_CHECK
57  __builtin_unreachable();
58 #endif
59 }
60 
61 #endif
62 
63 /* FUNCTION: setjmp */
64 
65 #ifndef __CPROVER_SETJMP_H_INCLUDED
66 #include <setjmp.h>
67 #define __CPROVER_SETJMP_H_INCLUDED
68 #endif
69 
70 #undef setjmp
71 
72 int setjmp(jmp_buf env)
73 {
74  (void)env;
75  // returns via longjmp require instrumentation; only such returns would
76  // return a non-zero value
77  return 0;
78 }
79 
80 /* FUNCTION: _setjmp */
81 
82 #ifndef __CPROVER_SETJMP_H_INCLUDED
83 #include <setjmp.h>
84 #define __CPROVER_SETJMP_H_INCLUDED
85 #endif
86 
87 int _setjmp(jmp_buf env)
88 {
89  (void)env;
90  // returns via longjmp require instrumentation; only such returns would
91  // return a non-zero value
92  return 0;
93 }
94 
95 /* FUNCTION: sigsetjmp */
96 
97 #ifndef _WIN32
98 
99 #ifndef __CPROVER_SETJMP_H_INCLUDED
100 # include <setjmp.h>
101 # define __CPROVER_SETJMP_H_INCLUDED
102 #endif
103 
104 #undef sigsetjmp
105 
106 int sigsetjmp(sigjmp_buf env, int savesigs)
107 {
108  (void)env;
109  (void)savesigs;
110  // returns via siglongjmp require instrumentation; only such returns would
111  // return a non-zero value
112  return 0;
113 }
114 
115 #endif
116 
117 /* FUNCTION: __sigsetjmp */
118 
119 #ifndef _WIN32
120 
121 #ifndef __CPROVER_SETJMP_H_INCLUDED
122 # include <setjmp.h>
123 # define __CPROVER_SETJMP_H_INCLUDED
124 #endif
125 
126 int __sigsetjmp(sigjmp_buf env, int savesigs)
127 {
128  (void)env;
129  (void)savesigs;
130  // returns via siglongjmp require instrumentation; only such returns would
131  // return a non-zero value
132  return 0;
133 }
134 
135 #endif
__CPROVER_assert
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
__CPROVER_assume
void __CPROVER_assume(__CPROVER_bool assumption)
__builtin_unreachable
void __builtin_unreachable(void)
sigsetjmp
int sigsetjmp(sigjmp_buf env, int savesigs)
Definition: setjmp.c:106
longjmp
void longjmp(jmp_buf env, int val)
Definition: setjmp.c:9
setjmp
int setjmp(jmp_buf env)
Definition: setjmp.c:72
_longjmp
void _longjmp(jmp_buf env, int val)
Definition: setjmp.c:28
siglongjmp
void siglongjmp(sigjmp_buf env, int val)
Definition: setjmp.c:49
_setjmp
int _setjmp(jmp_buf env)
Definition: setjmp.c:87
__sigsetjmp
int __sigsetjmp(sigjmp_buf env, int savesigs)
Definition: setjmp.c:126