CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
9void 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
28void _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
49void 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
72int 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
87int _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
106int 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
126int __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
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
__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