diff --git a/lib/libtheta-llvm.so b/lib/libtheta-llvm.so index ece2598555..85eb353bb0 100755 Binary files a/lib/libtheta-llvm.so and b/lib/libtheta-llvm.so differ diff --git a/subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.cpp b/subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.cpp index 41629cff8c..1face86b45 100644 --- a/subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.cpp +++ b/subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.cpp @@ -10,6 +10,10 @@ std::unordered_map> BasicBlock::LUT = std::unordered_map < llvm::BasicBlock *, std::shared_ptr> (); +void BasicBlock::reset() { + LUT = std::unordered_map < llvm::BasicBlock *, std::shared_ptr>(); +} + void BasicBlock::init() { initialized = true; numOfInstructions = 0; diff --git a/subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.h b/subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.h index 183edf815c..849e6bfedd 100644 --- a/subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.h +++ b/subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.h @@ -32,6 +32,8 @@ class BasicBlock { } } + static void reset(); + void init(); int getNumOfInstructions() { return numOfInstructions; } diff --git a/subprojects/frontends/llvm/src/main/cpp/types/Module.cpp b/subprojects/frontends/llvm/src/main/cpp/types/Module.cpp index 37244f7ade..a3258302bc 100644 --- a/subprojects/frontends/llvm/src/main/cpp/types/Module.cpp +++ b/subprojects/frontends/llvm/src/main/cpp/types/Module.cpp @@ -56,6 +56,11 @@ Module::Module() { } void Module::parseLLVMModule(std::shared_ptr llvmModule) { + instance = Module(); + Analysis::reset(); + BasicBlock::reset(); + Register::reset(); + // Analyze module first Analysis::checkModule(llvmModule.get()); diff --git a/subprojects/frontends/llvm/src/main/cpp/types/Module.h b/subprojects/frontends/llvm/src/main/cpp/types/Module.h index 8af64b97a2..afdc1b00ad 100644 --- a/subprojects/frontends/llvm/src/main/cpp/types/Module.h +++ b/subprojects/frontends/llvm/src/main/cpp/types/Module.h @@ -10,6 +10,8 @@ #include #include "Function.h" #include "BasicBlock.h" +#include "operands/Register.h" +#include "../utilities/Analysis.h" #include "GlobalVariable.h" // Global context diff --git a/subprojects/frontends/llvm/src/main/cpp/types/operands/Register.cpp b/subprojects/frontends/llvm/src/main/cpp/types/operands/Register.cpp index 76c08ff386..96ea0cc7f6 100644 --- a/subprojects/frontends/llvm/src/main/cpp/types/operands/Register.cpp +++ b/subprojects/frontends/llvm/src/main/cpp/types/operands/Register.cpp @@ -8,6 +8,10 @@ std::unordered_map> Register::LUT = std::unordered_map < llvm::Value *, std::shared_ptr> (); +void Register::reset() { + LUT = std::unordered_map < llvm::Value *, std::shared_ptr>(); +} + Register::Register(llvm::Value &llvmRegister) { if(llvmRegister.getName() == "") name = "register_" + std::to_string(nameCounter); else { diff --git a/subprojects/frontends/llvm/src/main/cpp/types/operands/Register.h b/subprojects/frontends/llvm/src/main/cpp/types/operands/Register.h index 029fd06f48..1905728cee 100644 --- a/subprojects/frontends/llvm/src/main/cpp/types/operands/Register.h +++ b/subprojects/frontends/llvm/src/main/cpp/types/operands/Register.h @@ -67,6 +67,8 @@ class Register : public Operand { } } + static void reset(); + static std::shared_ptr findRegister(llvm::Value *key); }; diff --git a/subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.cpp b/subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.cpp index 3b8f174598..53f4119df8 100644 --- a/subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.cpp +++ b/subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.cpp @@ -96,4 +96,9 @@ bool Analysis::checkIfAndOrXor(const llvm::BinaryOperator *binOp) { if(opname=="or") return true; if(opname=="xor") return true; return false; -} \ No newline at end of file +} + +void Analysis::reset() { +// hasIntInBitwiseBinaryOp = false; +// hasStructs = false; +} diff --git a/subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.h b/subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.h index 3e9e96a402..ea25a9b740 100644 --- a/subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.h +++ b/subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.h @@ -26,6 +26,7 @@ class Analysis { public: static void checkInstruction(llvm::Instruction* instruction); // when parsing, every instruction should be checked with this static void checkModule(const llvm::Module*); // before parsing module, this should be called on it + static void reset(); static bool getStructAnalysisResult() { return hasStructs; diff --git a/subprojects/xcfa/llvm2xcfa/src/test/java/hu/bme/mit/theta/llvm2xcfa/TestLlvm2Xcfa.kt b/subprojects/xcfa/llvm2xcfa/src/test/java/hu/bme/mit/theta/llvm2xcfa/TestLlvm2Xcfa.kt index 77a778d8d8..a0912bc8ba 100644 --- a/subprojects/xcfa/llvm2xcfa/src/test/java/hu/bme/mit/theta/llvm2xcfa/TestLlvm2Xcfa.kt +++ b/subprojects/xcfa/llvm2xcfa/src/test/java/hu/bme/mit/theta/llvm2xcfa/TestLlvm2Xcfa.kt @@ -41,6 +41,32 @@ class TestLlvm2Xcfa { arrayOf("/c/example_struct.c"), arrayOf("/c/example_void_func.c"), arrayOf("/c/test_locks_14-2.c"), + + arrayOf("/c/dekker.i"), + arrayOf("/c/00assignment.c"), +// arrayOf("/c/01cast.c"), + arrayOf("/c/02types.c"), + arrayOf("/c/03bitwise.c"), +// arrayOf("/c/04real.c"), +// arrayOf("/c/05math.c"), + arrayOf("/c/06arrays.c"), + arrayOf("/c/07arrayinit.c"), + arrayOf("/c/08vararray.c"), +// arrayOf("/c/09struct.c"), + arrayOf("/c/10ptr.c"), + arrayOf("/c/11ptrs.c"), + arrayOf("/c/12ptrtypes.c"), + arrayOf("/c/13typedef.c"), + arrayOf("/c/14ushort.c"), + arrayOf("/c/15addition.c"), + arrayOf("/c/16loop.c"), +// arrayOf("/c/17recursive.c"), + arrayOf("/c/18multithread.c"), + arrayOf("/c/19dportest.c"), + arrayOf("/c/20testinline.c"), + arrayOf("/c/21namecollision.c"), +// arrayOf("/c/22nondet.c"), + arrayOf("/c/23overflow.c"), ) } diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/00assignment.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/00assignment.c new file mode 100644 index 0000000000..3b2a4b33d2 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/00assignment.c @@ -0,0 +1,5 @@ +void reach_error(){} +int main() { + int a = 1; + if(a) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/01cast.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/01cast.c new file mode 100644 index 0000000000..2ebc365223 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/01cast.c @@ -0,0 +1,6 @@ +void reach_error(){} +int __VERIFIER_nondet(); +int main() { + int a = __VERIFIER_nondet(); + if(((char)a) != 0) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/02types.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/02types.c new file mode 100644 index 0000000000..6cfb80e8ba --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/02types.c @@ -0,0 +1,15 @@ +void reach_error(){} +int main() { + _Bool a; + unsigned char uc; + signed char c; + unsigned short us; + short s; + unsigned int ui; + int i; + unsigned long ul; + long l; + unsigned long long ull; + long long ll; + if(a+uc+c+us+s+ui+i+ul+l+ull+ll) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/03bitwise.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/03bitwise.c new file mode 100644 index 0000000000..36b65433e7 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/03bitwise.c @@ -0,0 +1,7 @@ +void reach_error(){} +int __VERIFIER_nondet_int(); +int main() { + int a = __VERIFIER_nondet_int(); + a = a | 0; + if(a == -10) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/04real.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/04real.c new file mode 100644 index 0000000000..fd2f62c684 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/04real.c @@ -0,0 +1,8 @@ +void reach_error(){} +extern float __VERIFIER_nondet_float(); +int main() { + float f = __VERIFIER_nondet_float(); + double d = f; + long double ld = d; + if(ld > 0.28f && ld < 0.32f) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/05math.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/05math.c new file mode 100644 index 0000000000..ffb8f7b2e4 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/05math.c @@ -0,0 +1,22 @@ +void reach_error(){} +float fabs(float); +float floor(float); +float round(float); +float fmax(float, float); +float fmin(float, float); +float sqrt(float); +int isnan(float); + +int main() { + float f = 12.65f; + float f1 = fabs(f); + float f2 = floor(f); + float f3 = round(f); + float f4 = fmax(f2, f3); + float f5 = fmin(f2, f3); + float f6 = sqrt(f); + float f7 = isnan(f); + f = 0.0f; + float f8 = isnan(0.0f/0.0f); + if(f8) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/06arrays.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/06arrays.c new file mode 100644 index 0000000000..7398bf83d7 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/06arrays.c @@ -0,0 +1,8 @@ +void reach_error(){} + +int main() { + int a[2], b[3]; + a[0] = 12; + b[3] = a[0]; + if(b[3] > 11) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/07arrayinit.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/07arrayinit.c new file mode 100644 index 0000000000..f96afd311f --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/07arrayinit.c @@ -0,0 +1,7 @@ +void reach_error(){} + +int main() { + int x; + int a[3] = {2, x+1, 4}; + if(a[1] > 2) reach_error(); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/08vararray.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/08vararray.c new file mode 100644 index 0000000000..d9d96c105f --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/08vararray.c @@ -0,0 +1,7 @@ +void reach_error(){} + +int main() { + int x; + int a[3] = {1, 2, 3}; + if(a[x] == 2) reach_error(); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/09struct.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/09struct.c new file mode 100644 index 0000000000..bdb621deec --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/09struct.c @@ -0,0 +1,16 @@ +void reach_error(){} + +struct A{ + int a; + char c; + struct { + int a; + } b; +}; + +int main() { + struct A a; + a.a = 3; + a.c = 1; + if(a.a + a.c + a.b.a < 4) reach_error(); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/10ptr.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/10ptr.c new file mode 100644 index 0000000000..25bec49b9d --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/10ptr.c @@ -0,0 +1,13 @@ +void reach_error(){} + +int main() { + int a = 110; + int *b = &a; + char *c = (char*)b; + a = 90; + char d = *c; + if(d > 100) reach_error(); + *b = 120; + d = *c; + if(d > 100) reach_error(); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/11ptrs.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/11ptrs.c new file mode 100644 index 0000000000..bdbb5d2739 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/11ptrs.c @@ -0,0 +1,12 @@ +void reach_error(){} + +void check_geq_110(int* param) { + if(*param >= 110) reach_error(); +} + +int main() { + int a = 100, b = 110, c = 120; + check_geq_110(&a); + check_geq_110(&b); + check_geq_110(&c); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/12ptrtypes.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/12ptrtypes.c new file mode 100644 index 0000000000..f42a220292 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/12ptrtypes.c @@ -0,0 +1,11 @@ +void reach_error(){} + +void check_geq_110(void* param) { + if(*(unsigned int*)param <= 110) reach_error(); +} + +int main() { + float f = 0.3f; + unsigned int all = -1; + check_geq_110(&all); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/13typedef.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/13typedef.c new file mode 100644 index 0000000000..bd3d461557 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/13typedef.c @@ -0,0 +1,8 @@ +void reach_error(){} + + +char char1; +int main() { + char char2; + if(char1 + char2 > 256) reach_error(); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/14ushort.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/14ushort.c new file mode 100644 index 0000000000..a5832df2d0 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/14ushort.c @@ -0,0 +1,10 @@ +void reach_error(){} + +extern unsigned short __VERIFIER_nondet_ushort(); + +int main() { + short ush; + long c; + ush = __VERIFIER_nondet_ushort(); + if(ush) reach_error(); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/15addition.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/15addition.c new file mode 100644 index 0000000000..20d3c13112 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/15addition.c @@ -0,0 +1,7 @@ +void reach_error(){} + +int main() { + int z = 6; + int y = 1; + if((z*z) - 12 * y - 6 * z + 12 == 0) reach_error(); + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/16loop.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/16loop.c new file mode 100644 index 0000000000..fcb835be73 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/16loop.c @@ -0,0 +1,7 @@ +void reach_error(){} + +int main() { + for(int i = 0; i < 30; i++) { + if(i == 28) reach_error(); + } + } \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/17recursive.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/17recursive.c new file mode 100644 index 0000000000..89286486ee --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/17recursive.c @@ -0,0 +1,11 @@ +void reach_error(){} + +int fibonacci(int i) { + if(i == 0) return 0; + else if(i == 1) return 1; + else return fibonacci(i-1) + fibonacci(i-2); +} + +int main() { + if(fibonacci(8) != 21) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/18multithread.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/18multithread.c new file mode 100644 index 0000000000..8ca102134e --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/18multithread.c @@ -0,0 +1,717 @@ + +typedef unsigned char __u_char; +typedef unsigned short int __u_short; +typedef unsigned int __u_int; +typedef unsigned long int __u_long; +typedef signed char __int8_t; +typedef unsigned char __uint8_t; +typedef signed short int __int16_t; +typedef unsigned short int __uint16_t; +typedef signed int __int32_t; +typedef unsigned int __uint32_t; +__extension__ typedef signed long long int __int64_t; +__extension__ typedef unsigned long long int __uint64_t; +typedef __int8_t __int_least8_t; +typedef __uint8_t __uint_least8_t; +typedef __int16_t __int_least16_t; +typedef __uint16_t __uint_least16_t; +typedef __int32_t __int_least32_t; +typedef __uint32_t __uint_least32_t; +typedef __int64_t __int_least64_t; +typedef __uint64_t __uint_least64_t; +__extension__ typedef long long int __quad_t; +__extension__ typedef unsigned long long int __u_quad_t; +__extension__ typedef long long int __intmax_t; +__extension__ typedef unsigned long long int __uintmax_t; +__extension__ typedef __uint64_t __dev_t; +__extension__ typedef unsigned int __uid_t; +__extension__ typedef unsigned int __gid_t; +__extension__ typedef unsigned long int __ino_t; +__extension__ typedef __uint64_t __ino64_t; +__extension__ typedef unsigned int __mode_t; +__extension__ typedef unsigned int __nlink_t; +__extension__ typedef long int __off_t; +__extension__ typedef __int64_t __off64_t; +__extension__ typedef int __pid_t; +__extension__ typedef struct { int __val[2]; } __fsid_t; +__extension__ typedef long int __clock_t; +__extension__ typedef unsigned long int __rlim_t; +__extension__ typedef __uint64_t __rlim64_t; +__extension__ typedef unsigned int __id_t; +__extension__ typedef long int __time_t; +__extension__ typedef unsigned int __useconds_t; +__extension__ typedef long int __suseconds_t; +__extension__ typedef int __daddr_t; +__extension__ typedef int __key_t; +__extension__ typedef int __clockid_t; +__extension__ typedef void * __timer_t; +__extension__ typedef long int __blksize_t; +__extension__ typedef long int __blkcnt_t; +__extension__ typedef __int64_t __blkcnt64_t; +__extension__ typedef unsigned long int __fsblkcnt_t; +__extension__ typedef __uint64_t __fsblkcnt64_t; +__extension__ typedef unsigned long int __fsfilcnt_t; +__extension__ typedef __uint64_t __fsfilcnt64_t; +__extension__ typedef int __fsword_t; +__extension__ typedef int __ssize_t; +__extension__ typedef long int __syscall_slong_t; +__extension__ typedef unsigned long int __syscall_ulong_t; +typedef __off64_t __loff_t; +typedef char *__caddr_t; +__extension__ typedef int __intptr_t; +__extension__ typedef unsigned int __socklen_t; +typedef int __sig_atomic_t; +__extension__ typedef __int64_t __time64_t; +static __inline __uint16_t +__bswap_16 (__uint16_t __bsx) +{ + return __builtin_bswap16 (__bsx); +} +static __inline __uint32_t +__bswap_32 (__uint32_t __bsx) +{ + return __builtin_bswap32 (__bsx); +} +__extension__ static __inline __uint64_t +__bswap_64 (__uint64_t __bsx) +{ + return __builtin_bswap64 (__bsx); +} +static __inline __uint16_t +__uint16_identity (__uint16_t __x) +{ + return __x; +} +static __inline __uint32_t +__uint32_identity (__uint32_t __x) +{ + return __x; +} +static __inline __uint64_t +__uint64_identity (__uint64_t __x) +{ + return __x; +} +typedef unsigned int size_t; +typedef __time_t time_t; +struct timespec +{ + __time_t tv_sec; + __syscall_slong_t tv_nsec; +}; +typedef __pid_t pid_t; +struct sched_param +{ + int sched_priority; +}; + + +typedef unsigned long int __cpu_mask; +typedef struct +{ + __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))]; +} cpu_set_t; + +extern int __sched_cpucount (size_t __setsize, const cpu_set_t *__setp) + __attribute__ ((__nothrow__ , __leaf__)); +extern cpu_set_t *__sched_cpualloc (size_t __count) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void __sched_cpufree (cpu_set_t *__set) __attribute__ ((__nothrow__ , __leaf__)); + + +extern int sched_setparam (__pid_t __pid, const struct sched_param *__param) + __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_getparam (__pid_t __pid, struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_setscheduler (__pid_t __pid, int __policy, + const struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_getscheduler (__pid_t __pid) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_yield (void) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_get_priority_max (int __algorithm) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_get_priority_min (int __algorithm) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_rr_get_interval (__pid_t __pid, struct timespec *__t) __attribute__ ((__nothrow__ , __leaf__)); + +typedef __clock_t clock_t; +struct tm +{ + int tm_sec; + int tm_min; + int tm_hour; + int tm_mday; + int tm_mon; + int tm_year; + int tm_wday; + int tm_yday; + int tm_isdst; + long int tm_gmtoff; + const char *tm_zone; +}; +typedef __clockid_t clockid_t; +typedef __timer_t timer_t; +struct itimerspec + { + struct timespec it_interval; + struct timespec it_value; + }; +struct sigevent; +struct __locale_struct +{ + struct __locale_data *__locales[13]; + const unsigned short int *__ctype_b; + const int *__ctype_tolower; + const int *__ctype_toupper; + const char *__names[13]; +}; +typedef struct __locale_struct *__locale_t; +typedef __locale_t locale_t; + +extern clock_t clock (void) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t time (time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern double difftime (time_t __time1, time_t __time0) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern time_t mktime (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern size_t strftime (char *__restrict __s, size_t __maxsize, + const char *__restrict __format, + const struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern size_t strftime_l (char *__restrict __s, size_t __maxsize, + const char *__restrict __format, + const struct tm *__restrict __tp, + locale_t __loc) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *gmtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *localtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *gmtime_r (const time_t *__restrict __timer, + struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *localtime_r (const time_t *__restrict __timer, + struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern char *asctime (const struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern char *ctime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern char *asctime_r (const struct tm *__restrict __tp, + char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); +extern char *ctime_r (const time_t *__restrict __timer, + char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); +extern char *__tzname[2]; +extern int __daylight; +extern long int __timezone; +extern char *tzname[2]; +extern void tzset (void) __attribute__ ((__nothrow__ , __leaf__)); +extern int daylight; +extern long int timezone; +extern int stime (const time_t *__when) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t timegm (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t timelocal (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern int dysize (int __year) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int nanosleep (const struct timespec *__requested_time, + struct timespec *__remaining); +extern int clock_getres (clockid_t __clock_id, struct timespec *__res) __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_gettime (clockid_t __clock_id, struct timespec *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_settime (clockid_t __clock_id, const struct timespec *__tp) + __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_nanosleep (clockid_t __clock_id, int __flags, + const struct timespec *__req, + struct timespec *__rem); +extern int clock_getcpuclockid (pid_t __pid, clockid_t *__clock_id) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_create (clockid_t __clock_id, + struct sigevent *__restrict __evp, + timer_t *__restrict __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_delete (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_settime (timer_t __timerid, int __flags, + const struct itimerspec *__restrict __value, + struct itimerspec *__restrict __ovalue) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_gettime (timer_t __timerid, struct itimerspec *__value) + __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_getoverrun (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timespec_get (struct timespec *__ts, int __base) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); + +struct __pthread_rwlock_arch_t +{ + unsigned int __readers; + unsigned int __writers; + unsigned int __wrphase_futex; + unsigned int __writers_futex; + unsigned int __pad3; + unsigned int __pad4; + unsigned char __flags; + unsigned char __shared; + signed char __rwelision; + unsigned char __pad2; + int __cur_writer; +}; +typedef struct __pthread_internal_slist +{ + struct __pthread_internal_slist *__next; +} __pthread_slist_t; +struct __pthread_mutex_s +{ + int __lock ; + unsigned int __count; + int __owner; + int __kind; + + unsigned int __nusers; + __extension__ union + { + struct { short __espins; short __eelision; } __elision_data; + __pthread_slist_t __list; + }; + +}; +struct __pthread_cond_s +{ + __extension__ union + { + __extension__ unsigned long long int __wseq; + struct + { + unsigned int __low; + unsigned int __high; + } __wseq32; + }; + __extension__ union + { + __extension__ unsigned long long int __g1_start; + struct + { + unsigned int __low; + unsigned int __high; + } __g1_start32; + }; + unsigned int __g_refs[2] ; + unsigned int __g_size[2]; + unsigned int __g1_orig_size; + unsigned int __wrefs; + unsigned int __g_signals[2]; +}; +typedef unsigned long int pthread_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_mutexattr_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_condattr_t; +typedef unsigned int pthread_key_t; +typedef int pthread_once_t; +union pthread_attr_t +{ + char __size[36]; + long int __align; +}; +typedef union pthread_attr_t pthread_attr_t; +typedef union +{ + struct __pthread_mutex_s __data; + char __size[24]; + long int __align; +} pthread_mutex_t; +typedef union +{ + struct __pthread_cond_s __data; + char __size[48]; + __extension__ long long int __align; +} pthread_cond_t; +typedef union +{ + struct __pthread_rwlock_arch_t __data; + char __size[32]; + long int __align; +} pthread_rwlock_t; +typedef union +{ + char __size[8]; + long int __align; +} pthread_rwlockattr_t; +typedef volatile int pthread_spinlock_t; +typedef union +{ + char __size[20]; + long int __align; +} pthread_barrier_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_barrierattr_t; +typedef int __jmp_buf[6]; +enum +{ + PTHREAD_CREATE_JOINABLE, + PTHREAD_CREATE_DETACHED +}; +enum +{ + PTHREAD_MUTEX_TIMED_NP, + PTHREAD_MUTEX_RECURSIVE_NP, + PTHREAD_MUTEX_ERRORCHECK_NP, + PTHREAD_MUTEX_ADAPTIVE_NP + , + PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP, + PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP, + PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP, + PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL +}; +enum +{ + PTHREAD_MUTEX_STALLED, + PTHREAD_MUTEX_STALLED_NP = PTHREAD_MUTEX_STALLED, + PTHREAD_MUTEX_ROBUST, + PTHREAD_MUTEX_ROBUST_NP = PTHREAD_MUTEX_ROBUST +}; +enum +{ + PTHREAD_PRIO_NONE, + PTHREAD_PRIO_INHERIT, + PTHREAD_PRIO_PROTECT +}; +enum +{ + PTHREAD_RWLOCK_PREFER_READER_NP, + PTHREAD_RWLOCK_PREFER_WRITER_NP, + PTHREAD_RWLOCK_PREFER_WRITER_NONRECURSIVE_NP, + PTHREAD_RWLOCK_DEFAULT_NP = PTHREAD_RWLOCK_PREFER_READER_NP +}; +enum +{ + PTHREAD_INHERIT_SCHED, + PTHREAD_EXPLICIT_SCHED +}; +enum +{ + PTHREAD_SCOPE_SYSTEM, + PTHREAD_SCOPE_PROCESS +}; +enum +{ + PTHREAD_PROCESS_PRIVATE, + PTHREAD_PROCESS_SHARED +}; +struct _pthread_cleanup_buffer +{ + void (*__routine) (void *); + void *__arg; + int __canceltype; + struct _pthread_cleanup_buffer *__prev; +}; +enum +{ + PTHREAD_CANCEL_ENABLE, + PTHREAD_CANCEL_DISABLE +}; +enum +{ + PTHREAD_CANCEL_DEFERRED, + PTHREAD_CANCEL_ASYNCHRONOUS +}; + +extern int pthread_create (pthread_t *__restrict __newthread, + const pthread_attr_t *__restrict __attr, + void *(*__start_routine) (void *), + void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3))); +extern void pthread_exit (void *__retval) __attribute__ ((__noreturn__)); +extern int pthread_join (pthread_t __th, void **__thread_return); +extern int pthread_detach (pthread_t __th) __attribute__ ((__nothrow__ , __leaf__)); +extern pthread_t pthread_self (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int pthread_equal (pthread_t __thread1, pthread_t __thread2) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int pthread_attr_init (pthread_attr_t *__attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_destroy (pthread_attr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getdetachstate (const pthread_attr_t *__attr, + int *__detachstate) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setdetachstate (pthread_attr_t *__attr, + int __detachstate) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getguardsize (const pthread_attr_t *__attr, + size_t *__guardsize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setguardsize (pthread_attr_t *__attr, + size_t __guardsize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getschedparam (const pthread_attr_t *__restrict __attr, + struct sched_param *__restrict __param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setschedparam (pthread_attr_t *__restrict __attr, + const struct sched_param *__restrict + __param) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_getschedpolicy (const pthread_attr_t *__restrict + __attr, int *__restrict __policy) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setschedpolicy (pthread_attr_t *__attr, int __policy) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getinheritsched (const pthread_attr_t *__restrict + __attr, int *__restrict __inherit) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setinheritsched (pthread_attr_t *__attr, + int __inherit) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getscope (const pthread_attr_t *__restrict __attr, + int *__restrict __scope) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setscope (pthread_attr_t *__attr, int __scope) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getstackaddr (const pthread_attr_t *__restrict + __attr, void **__restrict __stackaddr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))) __attribute__ ((__deprecated__)); +extern int pthread_attr_setstackaddr (pthread_attr_t *__attr, + void *__stackaddr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) __attribute__ ((__deprecated__)); +extern int pthread_attr_getstacksize (const pthread_attr_t *__restrict + __attr, size_t *__restrict __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setstacksize (pthread_attr_t *__attr, + size_t __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getstack (const pthread_attr_t *__restrict __attr, + void **__restrict __stackaddr, + size_t *__restrict __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))); +extern int pthread_attr_setstack (pthread_attr_t *__attr, void *__stackaddr, + size_t __stacksize) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_setschedparam (pthread_t __target_thread, int __policy, + const struct sched_param *__param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))); +extern int pthread_getschedparam (pthread_t __target_thread, + int *__restrict __policy, + struct sched_param *__restrict __param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3))); +extern int pthread_setschedprio (pthread_t __target_thread, int __prio) + __attribute__ ((__nothrow__ , __leaf__)); +extern int pthread_once (pthread_once_t *__once_control, + void (*__init_routine) (void)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_setcancelstate (int __state, int *__oldstate); +extern int pthread_setcanceltype (int __type, int *__oldtype); +extern int pthread_cancel (pthread_t __th); +extern void pthread_testcancel (void); +typedef struct +{ + struct + { + __jmp_buf __cancel_jmp_buf; + int __mask_was_saved; + } __cancel_jmp_buf[1]; + void *__pad[4]; +} __pthread_unwind_buf_t __attribute__ ((__aligned__)); +struct __pthread_cleanup_frame +{ + void (*__cancel_routine) (void *); + void *__cancel_arg; + int __do_it; + int __cancel_type; +}; +extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))); +extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))); +extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))) __attribute__ ((__noreturn__)) + __attribute__ ((__weak__)) + ; +struct __jmp_buf_tag; +extern int __sigsetjmp (struct __jmp_buf_tag *__env, int __savemask) __attribute__ ((__nothrow__)); +extern int pthread_mutex_init (pthread_mutex_t *__mutex, + const pthread_mutexattr_t *__mutexattr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_destroy (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_trylock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_lock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_timedlock (pthread_mutex_t *__restrict __mutex, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutex_unlock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_getprioceiling (const pthread_mutex_t * + __restrict __mutex, + int *__restrict __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutex_setprioceiling (pthread_mutex_t *__restrict __mutex, + int __prioceiling, + int *__restrict __old_ceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 3))); +extern int pthread_mutex_consistent (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_init (pthread_mutexattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_destroy (pthread_mutexattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getpshared (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setpshared (pthread_mutexattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_gettype (const pthread_mutexattr_t *__restrict + __attr, int *__restrict __kind) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_settype (pthread_mutexattr_t *__attr, int __kind) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getprotocol (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __protocol) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setprotocol (pthread_mutexattr_t *__attr, + int __protocol) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getprioceiling (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setprioceiling (pthread_mutexattr_t *__attr, + int __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getrobust (const pthread_mutexattr_t *__attr, + int *__robustness) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setrobust (pthread_mutexattr_t *__attr, + int __robustness) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_init (pthread_rwlock_t *__restrict __rwlock, + const pthread_rwlockattr_t *__restrict + __attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_destroy (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_rdlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_tryrdlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_timedrdlock (pthread_rwlock_t *__restrict __rwlock, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlock_wrlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_trywrlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_timedwrlock (pthread_rwlock_t *__restrict __rwlock, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlock_unlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_init (pthread_rwlockattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_destroy (pthread_rwlockattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_getpshared (const pthread_rwlockattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlockattr_setpshared (pthread_rwlockattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_getkind_np (const pthread_rwlockattr_t * + __restrict __attr, + int *__restrict __pref) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlockattr_setkind_np (pthread_rwlockattr_t *__attr, + int __pref) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_init (pthread_cond_t *__restrict __cond, + const pthread_condattr_t *__restrict __cond_attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_destroy (pthread_cond_t *__cond) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_signal (pthread_cond_t *__cond) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_broadcast (pthread_cond_t *__cond) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_wait (pthread_cond_t *__restrict __cond, + pthread_mutex_t *__restrict __mutex) + __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_cond_timedwait (pthread_cond_t *__restrict __cond, + pthread_mutex_t *__restrict __mutex, + const struct timespec *__restrict __abstime) + __attribute__ ((__nonnull__ (1, 2, 3))); +extern int pthread_condattr_init (pthread_condattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_destroy (pthread_condattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_getpshared (const pthread_condattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_condattr_setpshared (pthread_condattr_t *__attr, + int __pshared) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_getclock (const pthread_condattr_t * + __restrict __attr, + __clockid_t *__restrict __clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_condattr_setclock (pthread_condattr_t *__attr, + __clockid_t __clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_init (pthread_spinlock_t *__lock, int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_destroy (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_lock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_trylock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_unlock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_init (pthread_barrier_t *__restrict __barrier, + const pthread_barrierattr_t *__restrict + __attr, unsigned int __count) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_destroy (pthread_barrier_t *__barrier) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_wait (pthread_barrier_t *__barrier) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_init (pthread_barrierattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_destroy (pthread_barrierattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_getpshared (const pthread_barrierattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_key_create (pthread_key_t *__key, + void (*__destr_function) (void *)) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__)); +extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__)); +extern int pthread_setspecific (pthread_key_t __key, + const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int pthread_getcpuclockid (pthread_t __thread_id, + __clockid_t *__clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); +extern int pthread_atfork (void (*__prepare) (void), + void (*__parent) (void), + void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__)); + +void reach_error(){} + +int x = 0; +int ERR = 0; + +void *thr1(void *_) { + __VERIFIER_atomic_begin(); + x = 1; + __VERIFIER_atomic_end(); + __VERIFIER_atomic_begin(); + x = 2; + __VERIFIER_atomic_end(); +} + +void *thr2(void *_) { + __VERIFIER_atomic_begin(); + int i = x; + __VERIFIER_atomic_end(); + __VERIFIER_atomic_begin(); + int j = x; + __VERIFIER_atomic_end(); + if(i != j) ERR = 1; +} + +int main() { + pthread_t t1, t2; + pthread_create(&t1, 0, thr1, 0); + pthread_create(&t2, 0, thr2, 0); + if(ERR) reach_error(); + return 0; +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/19dportest.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/19dportest.c new file mode 100644 index 0000000000..c42b332ad0 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/19dportest.c @@ -0,0 +1,792 @@ + +typedef unsigned char __u_char; +typedef unsigned short int __u_short; +typedef unsigned int __u_int; +typedef unsigned long int __u_long; +typedef signed char __int8_t; +typedef unsigned char __uint8_t; +typedef signed short int __int16_t; +typedef unsigned short int __uint16_t; +typedef signed int __int32_t; +typedef unsigned int __uint32_t; +__extension__ typedef signed long long int __int64_t; +__extension__ typedef unsigned long long int __uint64_t; +typedef __int8_t __int_least8_t; +typedef __uint8_t __uint_least8_t; +typedef __int16_t __int_least16_t; +typedef __uint16_t __uint_least16_t; +typedef __int32_t __int_least32_t; +typedef __uint32_t __uint_least32_t; +typedef __int64_t __int_least64_t; +typedef __uint64_t __uint_least64_t; +__extension__ typedef long long int __quad_t; +__extension__ typedef unsigned long long int __u_quad_t; +__extension__ typedef long long int __intmax_t; +__extension__ typedef unsigned long long int __uintmax_t; +__extension__ typedef __uint64_t __dev_t; +__extension__ typedef unsigned int __uid_t; +__extension__ typedef unsigned int __gid_t; +__extension__ typedef unsigned long int __ino_t; +__extension__ typedef __uint64_t __ino64_t; +__extension__ typedef unsigned int __mode_t; +__extension__ typedef unsigned int __nlink_t; +__extension__ typedef long int __off_t; +__extension__ typedef __int64_t __off64_t; +__extension__ typedef int __pid_t; +__extension__ typedef struct { int __val[2]; } __fsid_t; +__extension__ typedef long int __clock_t; +__extension__ typedef unsigned long int __rlim_t; +__extension__ typedef __uint64_t __rlim64_t; +__extension__ typedef unsigned int __id_t; +__extension__ typedef long int __time_t; +__extension__ typedef unsigned int __useconds_t; +__extension__ typedef long int __suseconds_t; +__extension__ typedef int __daddr_t; +__extension__ typedef int __key_t; +__extension__ typedef int __clockid_t; +__extension__ typedef void * __timer_t; +__extension__ typedef long int __blksize_t; +__extension__ typedef long int __blkcnt_t; +__extension__ typedef __int64_t __blkcnt64_t; +__extension__ typedef unsigned long int __fsblkcnt_t; +__extension__ typedef __uint64_t __fsblkcnt64_t; +__extension__ typedef unsigned long int __fsfilcnt_t; +__extension__ typedef __uint64_t __fsfilcnt64_t; +__extension__ typedef int __fsword_t; +__extension__ typedef int __ssize_t; +__extension__ typedef long int __syscall_slong_t; +__extension__ typedef unsigned long int __syscall_ulong_t; +typedef __off64_t __loff_t; +typedef char *__caddr_t; +__extension__ typedef int __intptr_t; +__extension__ typedef unsigned int __socklen_t; +typedef int __sig_atomic_t; +__extension__ typedef __int64_t __time64_t; +static __inline __uint16_t +__bswap_16 (__uint16_t __bsx) +{ + return __builtin_bswap16 (__bsx); +} +static __inline __uint32_t +__bswap_32 (__uint32_t __bsx) +{ + return __builtin_bswap32 (__bsx); +} +__extension__ static __inline __uint64_t +__bswap_64 (__uint64_t __bsx) +{ + return __builtin_bswap64 (__bsx); +} +static __inline __uint16_t +__uint16_identity (__uint16_t __x) +{ + return __x; +} +static __inline __uint32_t +__uint32_identity (__uint32_t __x) +{ + return __x; +} +static __inline __uint64_t +__uint64_identity (__uint64_t __x) +{ + return __x; +} +typedef unsigned int size_t; +typedef __time_t time_t; +struct timespec +{ + __time_t tv_sec; + __syscall_slong_t tv_nsec; +}; +typedef __pid_t pid_t; +struct sched_param +{ + int sched_priority; +}; + + +typedef unsigned long int __cpu_mask; +typedef struct +{ + __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))]; +} cpu_set_t; + +extern int __sched_cpucount (size_t __setsize, const cpu_set_t *__setp) + __attribute__ ((__nothrow__ , __leaf__)); +extern cpu_set_t *__sched_cpualloc (size_t __count) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void __sched_cpufree (cpu_set_t *__set) __attribute__ ((__nothrow__ , __leaf__)); + + +extern int sched_setparam (__pid_t __pid, const struct sched_param *__param) + __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_getparam (__pid_t __pid, struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_setscheduler (__pid_t __pid, int __policy, + const struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_getscheduler (__pid_t __pid) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_yield (void) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_get_priority_max (int __algorithm) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_get_priority_min (int __algorithm) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_rr_get_interval (__pid_t __pid, struct timespec *__t) __attribute__ ((__nothrow__ , __leaf__)); + +typedef __clock_t clock_t; +struct tm +{ + int tm_sec; + int tm_min; + int tm_hour; + int tm_mday; + int tm_mon; + int tm_year; + int tm_wday; + int tm_yday; + int tm_isdst; + long int tm_gmtoff; + const char *tm_zone; +}; +typedef __clockid_t clockid_t; +typedef __timer_t timer_t; +struct itimerspec + { + struct timespec it_interval; + struct timespec it_value; + }; +struct sigevent; +struct __locale_struct +{ + struct __locale_data *__locales[13]; + const unsigned short int *__ctype_b; + const int *__ctype_tolower; + const int *__ctype_toupper; + const char *__names[13]; +}; +typedef struct __locale_struct *__locale_t; +typedef __locale_t locale_t; + +extern clock_t clock (void) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t time (time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern double difftime (time_t __time1, time_t __time0) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern time_t mktime (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern size_t strftime (char *__restrict __s, size_t __maxsize, + const char *__restrict __format, + const struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern size_t strftime_l (char *__restrict __s, size_t __maxsize, + const char *__restrict __format, + const struct tm *__restrict __tp, + locale_t __loc) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *gmtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *localtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *gmtime_r (const time_t *__restrict __timer, + struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *localtime_r (const time_t *__restrict __timer, + struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern char *asctime (const struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern char *ctime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern char *asctime_r (const struct tm *__restrict __tp, + char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); +extern char *ctime_r (const time_t *__restrict __timer, + char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); +extern char *__tzname[2]; +extern int __daylight; +extern long int __timezone; +extern char *tzname[2]; +extern void tzset (void) __attribute__ ((__nothrow__ , __leaf__)); +extern int daylight; +extern long int timezone; +extern int stime (const time_t *__when) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t timegm (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t timelocal (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern int dysize (int __year) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int nanosleep (const struct timespec *__requested_time, + struct timespec *__remaining); +extern int clock_getres (clockid_t __clock_id, struct timespec *__res) __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_gettime (clockid_t __clock_id, struct timespec *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_settime (clockid_t __clock_id, const struct timespec *__tp) + __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_nanosleep (clockid_t __clock_id, int __flags, + const struct timespec *__req, + struct timespec *__rem); +extern int clock_getcpuclockid (pid_t __pid, clockid_t *__clock_id) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_create (clockid_t __clock_id, + struct sigevent *__restrict __evp, + timer_t *__restrict __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_delete (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_settime (timer_t __timerid, int __flags, + const struct itimerspec *__restrict __value, + struct itimerspec *__restrict __ovalue) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_gettime (timer_t __timerid, struct itimerspec *__value) + __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_getoverrun (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timespec_get (struct timespec *__ts, int __base) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); + +struct __pthread_rwlock_arch_t +{ + unsigned int __readers; + unsigned int __writers; + unsigned int __wrphase_futex; + unsigned int __writers_futex; + unsigned int __pad3; + unsigned int __pad4; + unsigned char __flags; + unsigned char __shared; + signed char __rwelision; + unsigned char __pad2; + int __cur_writer; +}; +typedef struct __pthread_internal_slist +{ + struct __pthread_internal_slist *__next; +} __pthread_slist_t; +struct __pthread_mutex_s +{ + int __lock ; + unsigned int __count; + int __owner; + int __kind; + + unsigned int __nusers; + __extension__ union + { + struct { short __espins; short __eelision; } __elision_data; + __pthread_slist_t __list; + }; + +}; +struct __pthread_cond_s +{ + __extension__ union + { + __extension__ unsigned long long int __wseq; + struct + { + unsigned int __low; + unsigned int __high; + } __wseq32; + }; + __extension__ union + { + __extension__ unsigned long long int __g1_start; + struct + { + unsigned int __low; + unsigned int __high; + } __g1_start32; + }; + unsigned int __g_refs[2] ; + unsigned int __g_size[2]; + unsigned int __g1_orig_size; + unsigned int __wrefs; + unsigned int __g_signals[2]; +}; +typedef unsigned long int pthread_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_mutexattr_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_condattr_t; +typedef unsigned int pthread_key_t; +typedef int pthread_once_t; +union pthread_attr_t +{ + char __size[36]; + long int __align; +}; +typedef union pthread_attr_t pthread_attr_t; +typedef union +{ + struct __pthread_mutex_s __data; + char __size[24]; + long int __align; +} pthread_mutex_t; +typedef union +{ + struct __pthread_cond_s __data; + char __size[48]; + __extension__ long long int __align; +} pthread_cond_t; +typedef union +{ + struct __pthread_rwlock_arch_t __data; + char __size[32]; + long int __align; +} pthread_rwlock_t; +typedef union +{ + char __size[8]; + long int __align; +} pthread_rwlockattr_t; +typedef volatile int pthread_spinlock_t; +typedef union +{ + char __size[20]; + long int __align; +} pthread_barrier_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_barrierattr_t; +typedef int __jmp_buf[6]; +enum +{ + PTHREAD_CREATE_JOINABLE, + PTHREAD_CREATE_DETACHED +}; +enum +{ + PTHREAD_MUTEX_TIMED_NP, + PTHREAD_MUTEX_RECURSIVE_NP, + PTHREAD_MUTEX_ERRORCHECK_NP, + PTHREAD_MUTEX_ADAPTIVE_NP + , + PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP, + PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP, + PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP, + PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL +}; +enum +{ + PTHREAD_MUTEX_STALLED, + PTHREAD_MUTEX_STALLED_NP = PTHREAD_MUTEX_STALLED, + PTHREAD_MUTEX_ROBUST, + PTHREAD_MUTEX_ROBUST_NP = PTHREAD_MUTEX_ROBUST +}; +enum +{ + PTHREAD_PRIO_NONE, + PTHREAD_PRIO_INHERIT, + PTHREAD_PRIO_PROTECT +}; +enum +{ + PTHREAD_RWLOCK_PREFER_READER_NP, + PTHREAD_RWLOCK_PREFER_WRITER_NP, + PTHREAD_RWLOCK_PREFER_WRITER_NONRECURSIVE_NP, + PTHREAD_RWLOCK_DEFAULT_NP = PTHREAD_RWLOCK_PREFER_READER_NP +}; +enum +{ + PTHREAD_INHERIT_SCHED, + PTHREAD_EXPLICIT_SCHED +}; +enum +{ + PTHREAD_SCOPE_SYSTEM, + PTHREAD_SCOPE_PROCESS +}; +enum +{ + PTHREAD_PROCESS_PRIVATE, + PTHREAD_PROCESS_SHARED +}; +struct _pthread_cleanup_buffer +{ + void (*__routine) (void *); + void *__arg; + int __canceltype; + struct _pthread_cleanup_buffer *__prev; +}; +enum +{ + PTHREAD_CANCEL_ENABLE, + PTHREAD_CANCEL_DISABLE +}; +enum +{ + PTHREAD_CANCEL_DEFERRED, + PTHREAD_CANCEL_ASYNCHRONOUS +}; + +extern int pthread_create (pthread_t *__restrict __newthread, + const pthread_attr_t *__restrict __attr, + void *(*__start_routine) (void *), + void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3))); +extern void pthread_exit (void *__retval) __attribute__ ((__noreturn__)); +extern int pthread_join (pthread_t __th, void **__thread_return); +extern int pthread_detach (pthread_t __th) __attribute__ ((__nothrow__ , __leaf__)); +extern pthread_t pthread_self (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int pthread_equal (pthread_t __thread1, pthread_t __thread2) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int pthread_attr_init (pthread_attr_t *__attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_destroy (pthread_attr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getdetachstate (const pthread_attr_t *__attr, + int *__detachstate) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setdetachstate (pthread_attr_t *__attr, + int __detachstate) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getguardsize (const pthread_attr_t *__attr, + size_t *__guardsize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setguardsize (pthread_attr_t *__attr, + size_t __guardsize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getschedparam (const pthread_attr_t *__restrict __attr, + struct sched_param *__restrict __param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setschedparam (pthread_attr_t *__restrict __attr, + const struct sched_param *__restrict + __param) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_getschedpolicy (const pthread_attr_t *__restrict + __attr, int *__restrict __policy) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setschedpolicy (pthread_attr_t *__attr, int __policy) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getinheritsched (const pthread_attr_t *__restrict + __attr, int *__restrict __inherit) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setinheritsched (pthread_attr_t *__attr, + int __inherit) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getscope (const pthread_attr_t *__restrict __attr, + int *__restrict __scope) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setscope (pthread_attr_t *__attr, int __scope) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getstackaddr (const pthread_attr_t *__restrict + __attr, void **__restrict __stackaddr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))) __attribute__ ((__deprecated__)); +extern int pthread_attr_setstackaddr (pthread_attr_t *__attr, + void *__stackaddr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) __attribute__ ((__deprecated__)); +extern int pthread_attr_getstacksize (const pthread_attr_t *__restrict + __attr, size_t *__restrict __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setstacksize (pthread_attr_t *__attr, + size_t __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getstack (const pthread_attr_t *__restrict __attr, + void **__restrict __stackaddr, + size_t *__restrict __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))); +extern int pthread_attr_setstack (pthread_attr_t *__attr, void *__stackaddr, + size_t __stacksize) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_setschedparam (pthread_t __target_thread, int __policy, + const struct sched_param *__param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))); +extern int pthread_getschedparam (pthread_t __target_thread, + int *__restrict __policy, + struct sched_param *__restrict __param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3))); +extern int pthread_setschedprio (pthread_t __target_thread, int __prio) + __attribute__ ((__nothrow__ , __leaf__)); +extern int pthread_once (pthread_once_t *__once_control, + void (*__init_routine) (void)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_setcancelstate (int __state, int *__oldstate); +extern int pthread_setcanceltype (int __type, int *__oldtype); +extern int pthread_cancel (pthread_t __th); +extern void pthread_testcancel (void); +typedef struct +{ + struct + { + __jmp_buf __cancel_jmp_buf; + int __mask_was_saved; + } __cancel_jmp_buf[1]; + void *__pad[4]; +} __pthread_unwind_buf_t __attribute__ ((__aligned__)); +struct __pthread_cleanup_frame +{ + void (*__cancel_routine) (void *); + void *__cancel_arg; + int __do_it; + int __cancel_type; +}; +extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))); +extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))); +extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))) __attribute__ ((__noreturn__)) + __attribute__ ((__weak__)) + ; +struct __jmp_buf_tag; +extern int __sigsetjmp (struct __jmp_buf_tag *__env, int __savemask) __attribute__ ((__nothrow__)); +extern int pthread_mutex_init (pthread_mutex_t *__mutex, + const pthread_mutexattr_t *__mutexattr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_destroy (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_trylock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_lock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_timedlock (pthread_mutex_t *__restrict __mutex, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutex_unlock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_getprioceiling (const pthread_mutex_t * + __restrict __mutex, + int *__restrict __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutex_setprioceiling (pthread_mutex_t *__restrict __mutex, + int __prioceiling, + int *__restrict __old_ceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 3))); +extern int pthread_mutex_consistent (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_init (pthread_mutexattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_destroy (pthread_mutexattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getpshared (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setpshared (pthread_mutexattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_gettype (const pthread_mutexattr_t *__restrict + __attr, int *__restrict __kind) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_settype (pthread_mutexattr_t *__attr, int __kind) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getprotocol (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __protocol) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setprotocol (pthread_mutexattr_t *__attr, + int __protocol) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getprioceiling (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setprioceiling (pthread_mutexattr_t *__attr, + int __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getrobust (const pthread_mutexattr_t *__attr, + int *__robustness) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setrobust (pthread_mutexattr_t *__attr, + int __robustness) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_init (pthread_rwlock_t *__restrict __rwlock, + const pthread_rwlockattr_t *__restrict + __attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_destroy (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_rdlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_tryrdlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_timedrdlock (pthread_rwlock_t *__restrict __rwlock, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlock_wrlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_trywrlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_timedwrlock (pthread_rwlock_t *__restrict __rwlock, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlock_unlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_init (pthread_rwlockattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_destroy (pthread_rwlockattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_getpshared (const pthread_rwlockattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlockattr_setpshared (pthread_rwlockattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_getkind_np (const pthread_rwlockattr_t * + __restrict __attr, + int *__restrict __pref) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlockattr_setkind_np (pthread_rwlockattr_t *__attr, + int __pref) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_init (pthread_cond_t *__restrict __cond, + const pthread_condattr_t *__restrict __cond_attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_destroy (pthread_cond_t *__cond) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_signal (pthread_cond_t *__cond) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_broadcast (pthread_cond_t *__cond) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_wait (pthread_cond_t *__restrict __cond, + pthread_mutex_t *__restrict __mutex) + __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_cond_timedwait (pthread_cond_t *__restrict __cond, + pthread_mutex_t *__restrict __mutex, + const struct timespec *__restrict __abstime) + __attribute__ ((__nonnull__ (1, 2, 3))); +extern int pthread_condattr_init (pthread_condattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_destroy (pthread_condattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_getpshared (const pthread_condattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_condattr_setpshared (pthread_condattr_t *__attr, + int __pshared) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_getclock (const pthread_condattr_t * + __restrict __attr, + __clockid_t *__restrict __clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_condattr_setclock (pthread_condattr_t *__attr, + __clockid_t __clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_init (pthread_spinlock_t *__lock, int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_destroy (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_lock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_trylock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_unlock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_init (pthread_barrier_t *__restrict __barrier, + const pthread_barrierattr_t *__restrict + __attr, unsigned int __count) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_destroy (pthread_barrier_t *__barrier) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_wait (pthread_barrier_t *__barrier) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_init (pthread_barrierattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_destroy (pthread_barrierattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_getpshared (const pthread_barrierattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_key_create (pthread_key_t *__key, + void (*__destr_function) (void *)) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__)); +extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__)); +extern int pthread_setspecific (pthread_key_t __key, + const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int pthread_getcpuclockid (pthread_t __thread_id, + __clockid_t *__clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); +extern int pthread_atfork (void (*__prepare) (void), + void (*__parent) (void), + void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__)); + +void reach_error(){} + +int x = 0; + +void *thr1(void *_) { + int i = 0; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + x += i; +} + +void *thr2(void *_) { + int i = 0; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + i++; + x += i; +} + +int main() { +// for(int i = 0; i < 16; ++i) { + pthread_t t1, t2; + pthread_create(&t1, 0, thr1, 0); + pthread_create(&t2, 0, thr2, 0); + if(x > 41) reach_error(); + pthread_join(t1, 0); + pthread_join(t2, 0); +// } + + return 0; +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/20testinline.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/20testinline.c new file mode 100644 index 0000000000..d4695534cd --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/20testinline.c @@ -0,0 +1,12 @@ +void reach_error(); + +void func(int a) { + int x; + if(a == 1 && x == 2) reach_error(); + x = 1; +} + +int main() { + func(0); + func(1); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/21namecollision.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/21namecollision.c new file mode 100644 index 0000000000..f4df8686d0 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/21namecollision.c @@ -0,0 +1,15 @@ +int f(int x) { + return x - 1; +} + +int fp(int x) { + return x + 1; +} + +int main() { + int x; + x = f(x) - fp(x); + x = f(x) - fp(x); + x = f(x) - fp(x); + if(x == -2) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/22nondet.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/22nondet.c new file mode 100644 index 0000000000..86f2999f11 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/22nondet.c @@ -0,0 +1,10 @@ +extern int __VERIFIER_nondet_int(); +int main() { + int i = 0; + if((__VERIFIER_nondet_int() % 2) != 0) { + i = 1; + } else { + i = 2; + } + if(i==2) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/23overflow.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/23overflow.c new file mode 100644 index 0000000000..3d596e0e7b --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/23overflow.c @@ -0,0 +1,7 @@ +extern int __VERIFIER_nondet_int(); +void reach_error(); +int main() { + int i = __VERIFIER_nondet_int(); + i = i * 2; + if(i == 1) reach_error(); +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/dekker.i b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/dekker.i new file mode 100644 index 0000000000..86388ecf9c --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/dekker.i @@ -0,0 +1,797 @@ +extern void abort(void); +void assume_abort_if_not(int cond) { + if(!cond) {abort();} +} +extern void abort(void); + +extern void __assert_fail (const char *__assertion, const char *__file, + unsigned int __line, const char *__function) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +extern void __assert_perror_fail (int __errnum, const char *__file, + unsigned int __line, const char *__function) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +extern void __assert (const char *__assertion, const char *__file, int __line) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); + +void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "dekker.c", 7, __extension__ __PRETTY_FUNCTION__); })); } +extern void __VERIFIER_atomic_begin(void); +extern void __VERIFIER_atomic_end(void); +typedef unsigned char __u_char; +typedef unsigned short int __u_short; +typedef unsigned int __u_int; +typedef unsigned long int __u_long; +typedef signed char __int8_t; +typedef unsigned char __uint8_t; +typedef signed short int __int16_t; +typedef unsigned short int __uint16_t; +typedef signed int __int32_t; +typedef unsigned int __uint32_t; +__extension__ typedef signed long long int __int64_t; +__extension__ typedef unsigned long long int __uint64_t; +typedef __int8_t __int_least8_t; +typedef __uint8_t __uint_least8_t; +typedef __int16_t __int_least16_t; +typedef __uint16_t __uint_least16_t; +typedef __int32_t __int_least32_t; +typedef __uint32_t __uint_least32_t; +typedef __int64_t __int_least64_t; +typedef __uint64_t __uint_least64_t; +__extension__ typedef long long int __quad_t; +__extension__ typedef unsigned long long int __u_quad_t; +__extension__ typedef long long int __intmax_t; +__extension__ typedef unsigned long long int __uintmax_t; +__extension__ typedef __uint64_t __dev_t; +__extension__ typedef unsigned int __uid_t; +__extension__ typedef unsigned int __gid_t; +__extension__ typedef unsigned long int __ino_t; +__extension__ typedef __uint64_t __ino64_t; +__extension__ typedef unsigned int __mode_t; +__extension__ typedef unsigned int __nlink_t; +__extension__ typedef long int __off_t; +__extension__ typedef __int64_t __off64_t; +__extension__ typedef int __pid_t; +__extension__ typedef struct { int __val[2]; } __fsid_t; +__extension__ typedef long int __clock_t; +__extension__ typedef unsigned long int __rlim_t; +__extension__ typedef __uint64_t __rlim64_t; +__extension__ typedef unsigned int __id_t; +__extension__ typedef long int __time_t; +__extension__ typedef unsigned int __useconds_t; +__extension__ typedef long int __suseconds_t; +__extension__ typedef int __daddr_t; +__extension__ typedef int __key_t; +__extension__ typedef int __clockid_t; +__extension__ typedef void * __timer_t; +__extension__ typedef long int __blksize_t; +__extension__ typedef long int __blkcnt_t; +__extension__ typedef __int64_t __blkcnt64_t; +__extension__ typedef unsigned long int __fsblkcnt_t; +__extension__ typedef __uint64_t __fsblkcnt64_t; +__extension__ typedef unsigned long int __fsfilcnt_t; +__extension__ typedef __uint64_t __fsfilcnt64_t; +__extension__ typedef int __fsword_t; +__extension__ typedef int __ssize_t; +__extension__ typedef long int __syscall_slong_t; +__extension__ typedef unsigned long int __syscall_ulong_t; +typedef __off64_t __loff_t; +typedef char *__caddr_t; +__extension__ typedef int __intptr_t; +__extension__ typedef unsigned int __socklen_t; +typedef int __sig_atomic_t; +__extension__ typedef __int64_t __time64_t; +static __inline __uint16_t +__bswap_16 (__uint16_t __bsx) +{ + return __builtin_bswap16 (__bsx); +} +static __inline __uint32_t +__bswap_32 (__uint32_t __bsx) +{ + return __builtin_bswap32 (__bsx); +} +__extension__ static __inline __uint64_t +__bswap_64 (__uint64_t __bsx) +{ + return __builtin_bswap64 (__bsx); +} +static __inline __uint16_t +__uint16_identity (__uint16_t __x) +{ + return __x; +} +static __inline __uint32_t +__uint32_identity (__uint32_t __x) +{ + return __x; +} +static __inline __uint64_t +__uint64_identity (__uint64_t __x) +{ + return __x; +} +typedef unsigned int size_t; +typedef __time_t time_t; +struct timespec +{ + __time_t tv_sec; + __syscall_slong_t tv_nsec; +}; +typedef __pid_t pid_t; +struct sched_param +{ + int sched_priority; +}; + + +typedef unsigned long int __cpu_mask; +typedef struct +{ + __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))]; +} cpu_set_t; + +extern int __sched_cpucount (size_t __setsize, const cpu_set_t *__setp) + __attribute__ ((__nothrow__ , __leaf__)); +extern cpu_set_t *__sched_cpualloc (size_t __count) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void __sched_cpufree (cpu_set_t *__set) __attribute__ ((__nothrow__ , __leaf__)); + + +extern int sched_setparam (__pid_t __pid, const struct sched_param *__param) + __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_getparam (__pid_t __pid, struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_setscheduler (__pid_t __pid, int __policy, + const struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_getscheduler (__pid_t __pid) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_yield (void) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_get_priority_max (int __algorithm) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_get_priority_min (int __algorithm) __attribute__ ((__nothrow__ , __leaf__)); +extern int sched_rr_get_interval (__pid_t __pid, struct timespec *__t) __attribute__ ((__nothrow__ , __leaf__)); + +typedef __clock_t clock_t; +struct tm +{ + int tm_sec; + int tm_min; + int tm_hour; + int tm_mday; + int tm_mon; + int tm_year; + int tm_wday; + int tm_yday; + int tm_isdst; + long int tm_gmtoff; + const char *tm_zone; +}; +typedef __clockid_t clockid_t; +typedef __timer_t timer_t; +struct itimerspec + { + struct timespec it_interval; + struct timespec it_value; + }; +struct sigevent; +struct __locale_struct +{ + struct __locale_data *__locales[13]; + const unsigned short int *__ctype_b; + const int *__ctype_tolower; + const int *__ctype_toupper; + const char *__names[13]; +}; +typedef struct __locale_struct *__locale_t; +typedef __locale_t locale_t; + +extern clock_t clock (void) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t time (time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern double difftime (time_t __time1, time_t __time0) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern time_t mktime (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern size_t strftime (char *__restrict __s, size_t __maxsize, + const char *__restrict __format, + const struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern size_t strftime_l (char *__restrict __s, size_t __maxsize, + const char *__restrict __format, + const struct tm *__restrict __tp, + locale_t __loc) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *gmtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *localtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *gmtime_r (const time_t *__restrict __timer, + struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern struct tm *localtime_r (const time_t *__restrict __timer, + struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); +extern char *asctime (const struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern char *ctime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); +extern char *asctime_r (const struct tm *__restrict __tp, + char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); +extern char *ctime_r (const time_t *__restrict __timer, + char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); +extern char *__tzname[2]; +extern int __daylight; +extern long int __timezone; +extern char *tzname[2]; +extern void tzset (void) __attribute__ ((__nothrow__ , __leaf__)); +extern int daylight; +extern long int timezone; +extern int stime (const time_t *__when) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t timegm (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern time_t timelocal (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern int dysize (int __year) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int nanosleep (const struct timespec *__requested_time, + struct timespec *__remaining); +extern int clock_getres (clockid_t __clock_id, struct timespec *__res) __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_gettime (clockid_t __clock_id, struct timespec *__tp) __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_settime (clockid_t __clock_id, const struct timespec *__tp) + __attribute__ ((__nothrow__ , __leaf__)); +extern int clock_nanosleep (clockid_t __clock_id, int __flags, + const struct timespec *__req, + struct timespec *__rem); +extern int clock_getcpuclockid (pid_t __pid, clockid_t *__clock_id) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_create (clockid_t __clock_id, + struct sigevent *__restrict __evp, + timer_t *__restrict __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_delete (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_settime (timer_t __timerid, int __flags, + const struct itimerspec *__restrict __value, + struct itimerspec *__restrict __ovalue) __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_gettime (timer_t __timerid, struct itimerspec *__value) + __attribute__ ((__nothrow__ , __leaf__)); +extern int timer_getoverrun (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__)); +extern int timespec_get (struct timespec *__ts, int __base) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); + +struct __pthread_rwlock_arch_t +{ + unsigned int __readers; + unsigned int __writers; + unsigned int __wrphase_futex; + unsigned int __writers_futex; + unsigned int __pad3; + unsigned int __pad4; + unsigned char __flags; + unsigned char __shared; + signed char __rwelision; + unsigned char __pad2; + int __cur_writer; +}; +typedef struct __pthread_internal_slist +{ + struct __pthread_internal_slist *__next; +} __pthread_slist_t; +struct __pthread_mutex_s +{ + int __lock ; + unsigned int __count; + int __owner; + int __kind; + + unsigned int __nusers; + __extension__ union + { + struct { short __espins; short __eelision; } __elision_data; + __pthread_slist_t __list; + }; + +}; +struct __pthread_cond_s +{ + __extension__ union + { + __extension__ unsigned long long int __wseq; + struct + { + unsigned int __low; + unsigned int __high; + } __wseq32; + }; + __extension__ union + { + __extension__ unsigned long long int __g1_start; + struct + { + unsigned int __low; + unsigned int __high; + } __g1_start32; + }; + unsigned int __g_refs[2] ; + unsigned int __g_size[2]; + unsigned int __g1_orig_size; + unsigned int __wrefs; + unsigned int __g_signals[2]; +}; +typedef unsigned long int pthread_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_mutexattr_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_condattr_t; +typedef unsigned int pthread_key_t; +typedef int pthread_once_t; +union pthread_attr_t +{ + char __size[36]; + long int __align; +}; +typedef union pthread_attr_t pthread_attr_t; +typedef union +{ + struct __pthread_mutex_s __data; + char __size[24]; + long int __align; +} pthread_mutex_t; +typedef union +{ + struct __pthread_cond_s __data; + char __size[48]; + __extension__ long long int __align; +} pthread_cond_t; +typedef union +{ + struct __pthread_rwlock_arch_t __data; + char __size[32]; + long int __align; +} pthread_rwlock_t; +typedef union +{ + char __size[8]; + long int __align; +} pthread_rwlockattr_t; +typedef volatile int pthread_spinlock_t; +typedef union +{ + char __size[20]; + long int __align; +} pthread_barrier_t; +typedef union +{ + char __size[4]; + int __align; +} pthread_barrierattr_t; +typedef int __jmp_buf[6]; +enum +{ + PTHREAD_CREATE_JOINABLE, + PTHREAD_CREATE_DETACHED +}; +enum +{ + PTHREAD_MUTEX_TIMED_NP, + PTHREAD_MUTEX_RECURSIVE_NP, + PTHREAD_MUTEX_ERRORCHECK_NP, + PTHREAD_MUTEX_ADAPTIVE_NP + , + PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP, + PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP, + PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP, + PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL +}; +enum +{ + PTHREAD_MUTEX_STALLED, + PTHREAD_MUTEX_STALLED_NP = PTHREAD_MUTEX_STALLED, + PTHREAD_MUTEX_ROBUST, + PTHREAD_MUTEX_ROBUST_NP = PTHREAD_MUTEX_ROBUST +}; +enum +{ + PTHREAD_PRIO_NONE, + PTHREAD_PRIO_INHERIT, + PTHREAD_PRIO_PROTECT +}; +enum +{ + PTHREAD_RWLOCK_PREFER_READER_NP, + PTHREAD_RWLOCK_PREFER_WRITER_NP, + PTHREAD_RWLOCK_PREFER_WRITER_NONRECURSIVE_NP, + PTHREAD_RWLOCK_DEFAULT_NP = PTHREAD_RWLOCK_PREFER_READER_NP +}; +enum +{ + PTHREAD_INHERIT_SCHED, + PTHREAD_EXPLICIT_SCHED +}; +enum +{ + PTHREAD_SCOPE_SYSTEM, + PTHREAD_SCOPE_PROCESS +}; +enum +{ + PTHREAD_PROCESS_PRIVATE, + PTHREAD_PROCESS_SHARED +}; +struct _pthread_cleanup_buffer +{ + void (*__routine) (void *); + void *__arg; + int __canceltype; + struct _pthread_cleanup_buffer *__prev; +}; +enum +{ + PTHREAD_CANCEL_ENABLE, + PTHREAD_CANCEL_DISABLE +}; +enum +{ + PTHREAD_CANCEL_DEFERRED, + PTHREAD_CANCEL_ASYNCHRONOUS +}; + +extern int pthread_create (pthread_t *__restrict __newthread, + const pthread_attr_t *__restrict __attr, + void *(*__start_routine) (void *), + void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3))); +extern void pthread_exit (void *__retval) __attribute__ ((__noreturn__)); +extern int pthread_join (pthread_t __th, void **__thread_return); +extern int pthread_detach (pthread_t __th) __attribute__ ((__nothrow__ , __leaf__)); +extern pthread_t pthread_self (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int pthread_equal (pthread_t __thread1, pthread_t __thread2) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); +extern int pthread_attr_init (pthread_attr_t *__attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_destroy (pthread_attr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getdetachstate (const pthread_attr_t *__attr, + int *__detachstate) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setdetachstate (pthread_attr_t *__attr, + int __detachstate) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getguardsize (const pthread_attr_t *__attr, + size_t *__guardsize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setguardsize (pthread_attr_t *__attr, + size_t __guardsize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getschedparam (const pthread_attr_t *__restrict __attr, + struct sched_param *__restrict __param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setschedparam (pthread_attr_t *__restrict __attr, + const struct sched_param *__restrict + __param) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_getschedpolicy (const pthread_attr_t *__restrict + __attr, int *__restrict __policy) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setschedpolicy (pthread_attr_t *__attr, int __policy) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getinheritsched (const pthread_attr_t *__restrict + __attr, int *__restrict __inherit) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setinheritsched (pthread_attr_t *__attr, + int __inherit) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getscope (const pthread_attr_t *__restrict __attr, + int *__restrict __scope) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setscope (pthread_attr_t *__attr, int __scope) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getstackaddr (const pthread_attr_t *__restrict + __attr, void **__restrict __stackaddr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))) __attribute__ ((__deprecated__)); +extern int pthread_attr_setstackaddr (pthread_attr_t *__attr, + void *__stackaddr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) __attribute__ ((__deprecated__)); +extern int pthread_attr_getstacksize (const pthread_attr_t *__restrict + __attr, size_t *__restrict __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_attr_setstacksize (pthread_attr_t *__attr, + size_t __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_attr_getstack (const pthread_attr_t *__restrict __attr, + void **__restrict __stackaddr, + size_t *__restrict __stacksize) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))); +extern int pthread_attr_setstack (pthread_attr_t *__attr, void *__stackaddr, + size_t __stacksize) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_setschedparam (pthread_t __target_thread, int __policy, + const struct sched_param *__param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))); +extern int pthread_getschedparam (pthread_t __target_thread, + int *__restrict __policy, + struct sched_param *__restrict __param) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3))); +extern int pthread_setschedprio (pthread_t __target_thread, int __prio) + __attribute__ ((__nothrow__ , __leaf__)); +extern int pthread_once (pthread_once_t *__once_control, + void (*__init_routine) (void)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_setcancelstate (int __state, int *__oldstate); +extern int pthread_setcanceltype (int __type, int *__oldtype); +extern int pthread_cancel (pthread_t __th); +extern void pthread_testcancel (void); +typedef struct +{ + struct + { + __jmp_buf __cancel_jmp_buf; + int __mask_was_saved; + } __cancel_jmp_buf[1]; + void *__pad[4]; +} __pthread_unwind_buf_t __attribute__ ((__aligned__)); +struct __pthread_cleanup_frame +{ + void (*__cancel_routine) (void *); + void *__cancel_arg; + int __do_it; + int __cancel_type; +}; +extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))); +extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))); +extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf) + __attribute__ ((__regparm__ (1))) __attribute__ ((__noreturn__)) + __attribute__ ((__weak__)) + ; +struct __jmp_buf_tag; +extern int __sigsetjmp (struct __jmp_buf_tag *__env, int __savemask) __attribute__ ((__nothrow__)); +extern int pthread_mutex_init (pthread_mutex_t *__mutex, + const pthread_mutexattr_t *__mutexattr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_destroy (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_trylock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_lock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_timedlock (pthread_mutex_t *__restrict __mutex, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutex_unlock (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutex_getprioceiling (const pthread_mutex_t * + __restrict __mutex, + int *__restrict __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutex_setprioceiling (pthread_mutex_t *__restrict __mutex, + int __prioceiling, + int *__restrict __old_ceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 3))); +extern int pthread_mutex_consistent (pthread_mutex_t *__mutex) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_init (pthread_mutexattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_destroy (pthread_mutexattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getpshared (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setpshared (pthread_mutexattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_gettype (const pthread_mutexattr_t *__restrict + __attr, int *__restrict __kind) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_settype (pthread_mutexattr_t *__attr, int __kind) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getprotocol (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __protocol) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setprotocol (pthread_mutexattr_t *__attr, + int __protocol) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getprioceiling (const pthread_mutexattr_t * + __restrict __attr, + int *__restrict __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setprioceiling (pthread_mutexattr_t *__attr, + int __prioceiling) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_mutexattr_getrobust (const pthread_mutexattr_t *__attr, + int *__robustness) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_mutexattr_setrobust (pthread_mutexattr_t *__attr, + int __robustness) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_init (pthread_rwlock_t *__restrict __rwlock, + const pthread_rwlockattr_t *__restrict + __attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_destroy (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_rdlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_tryrdlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_timedrdlock (pthread_rwlock_t *__restrict __rwlock, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlock_wrlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_trywrlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlock_timedwrlock (pthread_rwlock_t *__restrict __rwlock, + const struct timespec *__restrict + __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlock_unlock (pthread_rwlock_t *__rwlock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_init (pthread_rwlockattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_destroy (pthread_rwlockattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_getpshared (const pthread_rwlockattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlockattr_setpshared (pthread_rwlockattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_rwlockattr_getkind_np (const pthread_rwlockattr_t * + __restrict __attr, + int *__restrict __pref) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_rwlockattr_setkind_np (pthread_rwlockattr_t *__attr, + int __pref) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_init (pthread_cond_t *__restrict __cond, + const pthread_condattr_t *__restrict __cond_attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_destroy (pthread_cond_t *__cond) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_signal (pthread_cond_t *__cond) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_broadcast (pthread_cond_t *__cond) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_cond_wait (pthread_cond_t *__restrict __cond, + pthread_mutex_t *__restrict __mutex) + __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_cond_timedwait (pthread_cond_t *__restrict __cond, + pthread_mutex_t *__restrict __mutex, + const struct timespec *__restrict __abstime) + __attribute__ ((__nonnull__ (1, 2, 3))); +extern int pthread_condattr_init (pthread_condattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_destroy (pthread_condattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_getpshared (const pthread_condattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_condattr_setpshared (pthread_condattr_t *__attr, + int __pshared) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_condattr_getclock (const pthread_condattr_t * + __restrict __attr, + __clockid_t *__restrict __clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_condattr_setclock (pthread_condattr_t *__attr, + __clockid_t __clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_init (pthread_spinlock_t *__lock, int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_destroy (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_lock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_trylock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_spin_unlock (pthread_spinlock_t *__lock) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_init (pthread_barrier_t *__restrict __barrier, + const pthread_barrierattr_t *__restrict + __attr, unsigned int __count) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_destroy (pthread_barrier_t *__barrier) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrier_wait (pthread_barrier_t *__barrier) + __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_init (pthread_barrierattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_destroy (pthread_barrierattr_t *__attr) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_barrierattr_getpshared (const pthread_barrierattr_t * + __restrict __attr, + int *__restrict __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); +extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr, + int __pshared) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_key_create (pthread_key_t *__key, + void (*__destr_function) (void *)) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); +extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__)); +extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__)); +extern int pthread_setspecific (pthread_key_t __key, + const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int pthread_getcpuclockid (pthread_t __thread_id, + __clockid_t *__clock_id) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); +extern int pthread_atfork (void (*__prepare) (void), + void (*__parent) (void), + void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__)); + +int flag1 = 0, flag2 = 0; +int turn; +int x; +void *thr1(void *_) { + __VERIFIER_atomic_begin(); + flag1 = 1; + __VERIFIER_atomic_end(); + __VERIFIER_atomic_begin(); + int f2 = flag2; + __VERIFIER_atomic_end(); + while (f2 >= 1) { + __VERIFIER_atomic_begin(); + int t = turn; + __VERIFIER_atomic_end(); + if (t != 0) { + __VERIFIER_atomic_begin(); + flag1 = 0; + __VERIFIER_atomic_end(); + __VERIFIER_atomic_begin(); + t = turn; + __VERIFIER_atomic_end(); + while (t != 0) { + __VERIFIER_atomic_begin(); + t = turn; + __VERIFIER_atomic_end(); + }; + __VERIFIER_atomic_begin(); + flag1 = 1; + __VERIFIER_atomic_end(); + } + __VERIFIER_atomic_begin(); + f2 = flag2; + __VERIFIER_atomic_end(); + } + x = 0; + if (!(x<=0)) ERROR: reach_error(); + __VERIFIER_atomic_begin(); + turn = 1; + __VERIFIER_atomic_end(); + __VERIFIER_atomic_begin(); + flag1 = 0; + __VERIFIER_atomic_end(); + return 0; +} +void *thr2(void *_) { + __VERIFIER_atomic_begin(); + flag2 = 1; + __VERIFIER_atomic_end(); + __VERIFIER_atomic_begin(); + int f1 = flag1; + __VERIFIER_atomic_end(); + while (f1 >= 1) { + __VERIFIER_atomic_begin(); + int t = turn; + __VERIFIER_atomic_end(); + if (t != 1) { + __VERIFIER_atomic_begin(); + flag2 = 0; + __VERIFIER_atomic_end(); + __VERIFIER_atomic_begin(); + t = turn; + __VERIFIER_atomic_end(); + while (t != 1) { + __VERIFIER_atomic_begin(); + t = turn; + __VERIFIER_atomic_end(); + }; + __VERIFIER_atomic_begin(); + flag2 = 1; + __VERIFIER_atomic_end(); + } + __VERIFIER_atomic_begin(); + f1 = flag1; + __VERIFIER_atomic_end(); + } + x = 1; + if (!(x>=1)) ERROR: reach_error(); + __VERIFIER_atomic_begin(); + turn = 1; + __VERIFIER_atomic_end(); + __VERIFIER_atomic_begin(); + flag2 = 0; + __VERIFIER_atomic_end(); + return 0; +} +int main() { + pthread_t t1, t2; + assume_abort_if_not(0<=turn && turn<=1); + pthread_create(&t1, 0, thr1, 0); + pthread_create(&t2, 0, thr2, 0); + pthread_join(t1, 0); + pthread_join(t2, 0); + return 0; +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/example-expl.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/example-expl.c new file mode 100644 index 0000000000..82cac53286 --- /dev/null +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/example-expl.c @@ -0,0 +1,7 @@ +void reach_error(); +int main() { + int i = 0; + if(i == 1) { + reach_error(); + } +} \ No newline at end of file diff --git a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/example_binbitwiseop.c b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/example_binbitwiseop.c index 4ab9df1a58..a319ca3859 100644 --- a/subprojects/xcfa/llvm2xcfa/src/test/resources/c/example_binbitwiseop.c +++ b/subprojects/xcfa/llvm2xcfa/src/test/resources/c/example_binbitwiseop.c @@ -4,5 +4,9 @@ int main() { int a, b; scanf("%d", &a); scanf("%d", &b); +// +// int c = a << 2; +// int d = b >> 2; +// int e = c | d & 11; return a&&b; } \ No newline at end of file