diff --git a/regression/cbmc-library/getrandom-01/main.c b/regression/cbmc-library/getrandom-01/main.c index 01334f7ac09..9325690b789 100644 --- a/regression/cbmc-library/getrandom-01/main.c +++ b/regression/cbmc-library/getrandom-01/main.c @@ -1,8 +1,9 @@ -#ifdef __linux__ -# include - # include +#if defined(__GLIBC__) && \ + (__GLIBC__ > 2 || (__GLIBC__ == 2 && __GLIBC_MINOR__ >= 25)) +# include + int main() { char zero_bytes[6] = {0}; diff --git a/src/ansi-c/library/random.c b/src/ansi-c/library/random.c index 9a7cff665ad..65d2ef7947a 100644 --- a/src/ansi-c/library/random.c +++ b/src/ansi-c/library/random.c @@ -1,6 +1,12 @@ /* FUNCTION: getrandom */ -#ifdef __linux__ +#ifndef __CPROVER_ERRNO_H_INCLUDED +#include +#define __CPROVER_ERRNO_H_INCLUDED +#endif + +#if defined(__GLIBC__) && \ + (__GLIBC__ > 2 || (__GLIBC__ == 2 && __GLIBC_MINOR__ >= 25)) # ifndef __CPROVER_SYS_RANDOM_H_INCLUDED # include