-
Notifications
You must be signed in to change notification settings - Fork 17
/
genmc.h
38 lines (32 loc) · 1002 Bytes
/
genmc.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
#ifndef __GENMC_H__
#define __GENMC_H__
/*
* If the argument is not true, blocks the execution
*/
void __VERIFIER_assume(int);
/*
* Models a limited amount of non-determinism by returning
* a pseudo-random sequence of integers. This sequence
* is always the same per execution for each thread
*/
int __VERIFIER_nondet_int(void);
/*
* Two marker functions that can be used to mark the
* beginning and end of spinloops that are not automatically
* transformed to assume() statements by GenMC.
*/
void __VERIFIER_spin_start(void);
void __VERIFIER_spin_end(void);
/*
* The signature of a recovery routine to be specified
* by the user. This routine will run after each execution,
* if the checker is run with the respective flags enabled
*/
void __VERIFIER_recovery_routine(void);
/*
* All the file opeartions before this barrier will
* have persisted to memory when the recovery routine runs.
* Should be used only once.
*/
void __VERIFIER_pbarrier(void);
#endif /* __GENMC_H__ */