# 1 "search_n.c" # 1 "" # 1 "" # 31 "" # 1 "/usr/include/stdc-predef.h" 1 3 4 # 1 "/usr/include/stdc-predef.h" 3 4 /* Copyright (C) 1991-2016 Free Software Foundation, Inc. This file is part of the GNU C Library. The GNU C Library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. The GNU C Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with the GNU C Library; if not, see . */ /* This header is separate from features.h so that the compiler can include it implicitly at the start of every compilation. It must not itself include or any other header that includes because the implicit include comes before any feature test macros that may be defined in a source file before it first explicitly includes a system header. GCC knows the name of this header in order to preinclude it. */ /* glibc's intent is to support the IEC 559 math functionality, real and complex. If the GCC (4.9 and later) predefined macros specifying compiler intent are available, use them to determine whether the overall intent is to support these features; otherwise, presume an older compiler has intent to support these features and define these macros by default. */ # 52 "/usr/include/stdc-predef.h" 3 4 /* wchar_t uses Unicode 9.0.0. Version 9.0 of the Unicode Standard is synchronized with ISO/IEC 10646:2014, fourth edition, plus Amd. 1 and Amd. 2 and 273 characters from forthcoming 10646, fifth edition. (Amd. 2 was published 2016-05-01, see https://www.iso.org/obp/ui/#iso:std:iso-iec:10646:ed-4:v1:amd:2:v1:en) */ /* We do not support C11 . */ # 32 "" 2 # 1 "search_n.c" # 1 "search_n.h" 1 # 1 "../../Logic/HasConstantSubRange.h" 1 # 1 "../../Logic/ConstantRange.h" 1 # 1 "../../typedefs.h" 1 # 1 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/limits.h" 1 3 4 /* Copyright (C) 1992-2016 Free Software Foundation, Inc. This file is part of GCC. GCC is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3, or (at your option) any later version. GCC is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. Under Section 7 of GPL version 3, you are granted additional permissions described in the GCC Runtime Library Exception, version 3.1, as published by the Free Software Foundation. You should have received a copy of the GNU General Public License and a copy of the GCC Runtime Library Exception along with this program; see the files COPYING3 and COPYING.RUNTIME respectively. If not, see . */ /* This administrivia gets added to the beginning of limits.h if the system has its own version of limits.h. */ /* We use _GCC_LIMITS_H_ because we want this not to match any macros that the system's limits.h uses for its own purposes. */ /* Use "..." so that we find syslimits.h only in this same directory. */ # 1 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/syslimits.h" 1 3 4 /* syslimits.h stands for the system's own limits.h file. If we can use it ok unmodified, then we install this text. If fixincludes fixes it, then the fixed version is installed instead of this text. */ # 1 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/limits.h" 1 3 4 /* Copyright (C) 1992-2016 Free Software Foundation, Inc. This file is part of GCC. GCC is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3, or (at your option) any later version. GCC is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. Under Section 7 of GPL version 3, you are granted additional permissions described in the GCC Runtime Library Exception, version 3.1, as published by the Free Software Foundation. You should have received a copy of the GNU General Public License and a copy of the GCC Runtime Library Exception along with this program; see the files COPYING3 and COPYING.RUNTIME respectively. If not, see . */ /* This administrivia gets added to the beginning of limits.h if the system has its own version of limits.h. */ /* We use _GCC_LIMITS_H_ because we want this not to match any macros that the system's limits.h uses for its own purposes. */ # 168 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/limits.h" 3 4 # 1 "/usr/include/limits.h" 1 3 4 /* Copyright (C) 1991-2016 Free Software Foundation, Inc. This file is part of the GNU C Library. The GNU C Library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. The GNU C Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with the GNU C Library; if not, see . */ /* * ISO C99 Standard: 7.10/5.2.4.2.1 Sizes of integer types */ # 1 "/usr/include/features.h" 1 3 4 /* Copyright (C) 1991-2016 Free Software Foundation, Inc. This file is part of the GNU C Library. The GNU C Library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. The GNU C Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with the GNU C Library; if not, see . */ /* These are defined by the user (or the compiler) to specify the desired environment: __STRICT_ANSI__ ISO Standard C. _ISOC99_SOURCE Extensions to ISO C89 from ISO C99. _ISOC11_SOURCE Extensions to ISO C99 from ISO C11. _POSIX_SOURCE IEEE Std 1003.1. _POSIX_C_SOURCE If ==1, like _POSIX_SOURCE; if >=2 add IEEE Std 1003.2; if >=199309L, add IEEE Std 1003.1b-1993; if >=199506L, add IEEE Std 1003.1c-1995; if >=200112L, all of IEEE 1003.1-2004 if >=200809L, all of IEEE 1003.1-2008 _XOPEN_SOURCE Includes POSIX and XPG things. Set to 500 if Single Unix conformance is wanted, to 600 for the sixth revision, to 700 for the seventh revision. _XOPEN_SOURCE_EXTENDED XPG things and X/Open Unix extensions. _LARGEFILE_SOURCE Some more functions for correct standard I/O. _LARGEFILE64_SOURCE Additional functionality from LFS for large files. _FILE_OFFSET_BITS=N Select default filesystem interface. _ATFILE_SOURCE Additional *at interfaces. _GNU_SOURCE All of the above, plus GNU extensions. _DEFAULT_SOURCE The default set of features (taking precedence over __STRICT_ANSI__). _REENTRANT Select additionally reentrant object. _THREAD_SAFE Same as _REENTRANT, often used by other systems. _FORTIFY_SOURCE If set to numeric value > 0 additional security measures are defined, according to level. The `-ansi' switch to the GNU C compiler, and standards conformance options such as `-std=c99', define __STRICT_ANSI__. If none of these are defined, or if _DEFAULT_SOURCE is defined, the default is to have _POSIX_SOURCE set to one and _POSIX_C_SOURCE set to 200809L, as well as enabling miscellaneous functions from BSD and SVID. If more than one of these are defined, they accumulate. For example __STRICT_ANSI__, _POSIX_SOURCE and _POSIX_C_SOURCE together give you ISO C, 1003.1, and 1003.2, but nothing else. These are defined by this file and are used by the header files to decide what to declare or define: __USE_ISOC11 Define ISO C11 things. __USE_ISOC99 Define ISO C99 things. __USE_ISOC95 Define ISO C90 AMD1 (C95) things. __USE_POSIX Define IEEE Std 1003.1 things. __USE_POSIX2 Define IEEE Std 1003.2 things. __USE_POSIX199309 Define IEEE Std 1003.1, and .1b things. __USE_POSIX199506 Define IEEE Std 1003.1, .1b, .1c and .1i things. __USE_XOPEN Define XPG things. __USE_XOPEN_EXTENDED Define X/Open Unix things. __USE_UNIX98 Define Single Unix V2 things. __USE_XOPEN2K Define XPG6 things. __USE_XOPEN2KXSI Define XPG6 XSI things. __USE_XOPEN2K8 Define XPG7 things. __USE_XOPEN2K8XSI Define XPG7 XSI things. __USE_LARGEFILE Define correct standard I/O things. __USE_LARGEFILE64 Define LFS things with separate names. __USE_FILE_OFFSET64 Define 64bit interface as default. __USE_MISC Define things from 4.3BSD or System V Unix. __USE_ATFILE Define *at interfaces and AT_* constants for them. __USE_GNU Define GNU extensions. __USE_REENTRANT Define reentrant/thread-safe *_r functions. __USE_FORTIFY_LEVEL Additional security measures used, according to level. The macros `__GNU_LIBRARY__', `__GLIBC__', and `__GLIBC_MINOR__' are defined by this file unconditionally. `__GNU_LIBRARY__' is provided only for compatibility. All new code should use the other symbols to test for features. All macros listed above as possibly being defined by this file are explicitly undefined if they are not explicitly defined. Feature-test macros that are not defined by the user or compiler but are implied by the other feature-test macros defined (or by the lack of any definitions) are defined by the file. */ /* Undefine everything, so we get a clean slate. */ # 122 "/usr/include/features.h" 3 4 /* Suppress kernel-name space pollution unless user expressedly asks for it. */ /* Convenience macros to test the versions of glibc and gcc. Use them like this: #if __GNUC_PREREQ (2,8) ... code requiring gcc 2.8 or later ... #endif Note - they won't work for gcc1 or glibc1, since the _MINOR macros were not defined then. */ /* _BSD_SOURCE and _SVID_SOURCE are deprecated aliases for _DEFAULT_SOURCE. If _DEFAULT_SOURCE is present we do not issue a warning; the expectation is that the source is being transitioned to use the new macro. */ /* If _GNU_SOURCE was defined by the user, turn on all the other features. */ # 177 "/usr/include/features.h" 3 4 /* If nothing (other than _GNU_SOURCE and _DEFAULT_SOURCE) is defined, define _DEFAULT_SOURCE. */ # 188 "/usr/include/features.h" 3 4 /* This is to enable the ISO C11 extension. */ /* This is to enable the ISO C99 extension. */ /* This is to enable the ISO C90 Amendment 1:1995 extension. */ /* This is to enable compatibility for ISO C++11. So far g++ does not provide a macro. Check the temporary macro for now, too. */ /* If none of the ANSI/POSIX macros are defined, or if _DEFAULT_SOURCE is defined, use POSIX.1-2008 (or another version depending on _XOPEN_SOURCE). */ # 340 "/usr/include/features.h" 3 4 /* Get definitions of __STDC_* predefined macros, if the compiler has not preincluded this header automatically. */ # 1 "/usr/include/stdc-predef.h" 1 3 4 /* Copyright (C) 1991-2016 Free Software Foundation, Inc. This file is part of the GNU C Library. The GNU C Library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. The GNU C Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with the GNU C Library; if not, see . */ # 343 "/usr/include/features.h" 2 3 4 /* This macro indicates that the installed library is the GNU C Library. For historic reasons the value now is 6 and this will stay from now on. The use of this variable is deprecated. Use __GLIBC__ and __GLIBC_MINOR__ now (see below) when you want to test for a specific GNU C library version and use the values in to get the sonames of the shared libraries. */ /* Major and minor version number of the GNU C library package. Use these macros to test for features in specific releases. */ /* This is here only because every header file already includes this one. */ # 1 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 1 3 4 /* Copyright (C) 1992-2016 Free Software Foundation, Inc. This file is part of the GNU C Library. The GNU C Library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. The GNU C Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with the GNU C Library; if not, see . */ /* We are almost always included from features.h. */ /* The GNU libc does not support any K&R compilers or the traditional mode of ISO C compilers anymore. Check for some of the combinations not anymore supported. */ /* Some user header file might have defined this before. */ /* All functions, except those with callbacks or those that synchronize memory, are leaf functions. */ # 49 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* GCC can always grok prototypes. For C++ programs we add throw() to help it optimize the function calls. But this works only with gcc 2.8.x and egcs. For gcc 3.2 and up we even mark C functions as non-throwing using a function attribute since programs can use the -fexceptions options for C code as well. */ # 80 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* These two macros are not used in glibc anymore. They are kept here only because some other projects expect the macros to be defined. */ /* For these things, GCC behaves the ANSI way normally, and the non-ANSI way under -traditional. */ /* This is not a typedef so `const __ptr_t' does the right thing. */ /* C++ needs to know that types and declarations are C, not C++. */ # 106 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* The standard library needs the functions from the ISO C90 standard in the std namespace. At the same time we want to be safe for future changes and we include the ISO C99 code in the non-standard namespace __c99. The C++ wrapper header take case of adding the definitions to the global namespace. */ # 119 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* For compatibility we do not add the declarations into any namespace. They will end up in the global namespace which is what old code expects. */ # 131 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* Fortify support. */ # 147 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* Support for flexible arrays. */ /* GCC 2.97 supports C99 flexible array members. */ # 165 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* __asm__ ("xyz") is used throughout the headers to rename functions at the assembly language level. This is wrapped by the __REDIRECT macro, in order to support compilers that can do this some other way. When compilers don't support asm-names at all, we have to do preprocessor tricks instead (which don't have exactly the right semantics, but it's the best we can do). Example: int __REDIRECT(setpgrp, (__pid_t pid, __pid_t pgrp), setpgid); */ # 192 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* #elif __SOME_OTHER_COMPILER__ # define __REDIRECT(name, proto, alias) name proto; _Pragma("let " #name " = " #alias) ) */ /* GCC has various useful declarations that can be made with the `__attribute__' syntax. All of the ways we use this do fine if they are omitted for compilers that don't understand it. */ /* At some point during the gcc 2.96 development the `malloc' attribute for functions was introduced. We don't want to use it unconditionally (although this would be possible) since it generates warnings. */ /* Tell the compiler which arguments to an allocation function indicate the size of the allocation. */ /* At some point during the gcc 2.96 development the `pure' attribute for functions was introduced. We don't want to use it unconditionally (although this would be possible) since it generates warnings. */ /* This declaration tells the compiler that the value is constant. */ /* At some point during the gcc 3.1 development the `used' attribute for functions was introduced. We don't want to use it unconditionally (although this would be possible) since it generates warnings. */ # 252 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* gcc allows marking deprecated functions. */ /* At some point during the gcc 2.8 development the `format_arg' attribute for functions was introduced. We don't want to use it unconditionally (although this would be possible) since it generates warnings. If several `format_arg' attributes are given for the same function, in gcc-3.0 and older, all but the last one are ignored. In newer gccs, all designated arguments are considered. */ /* At some point during the gcc 2.97 development the `strfmon' format attribute for functions was introduced. We don't want to use it unconditionally (although this would be possible) since it generates warnings. */ /* The nonull function attribute allows to mark pointer parameters which must not be NULL. */ /* If fortification mode, we warn about unused results of certain function calls which can lead to problems. */ # 305 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* Forces a function to be always inlined. */ /* The Linux kernel defines __always_inline in stddef.h (283d7573), and it conflicts with this definition. Therefore undefine it first to allow either header to be included first. */ /* Associate error messages with the source location of the call site rather than with the source location inside the function. */ /* GCC 4.3 and above with -std=c99 or -std=gnu99 implements ISO C99 inline semantics, unless -fgnu89-inline is used. Using __GNUC_STDC_INLINE__ or __GNUC_GNU_INLINE is not a good enough check for gcc because gcc versions older than 4.3 may define these macros and still not guarantee GNU inlining semantics. clang++ identifies itself as gcc-4.2, but has support for GNU inlining semantics, that can be checked fot by using the __GNUC_STDC_INLINE_ and __GNUC_GNU_INLINE__ macro definitions. */ # 351 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 /* GCC 4.3 and above allow passing all anonymous arguments of an __extern_always_inline function to some other vararg function. */ /* It is possible to compile containing GCC extensions even if GCC is run in pedantic mode if the uses are carefully marked using the `__extension__' keyword. But this is not generally available before version 2.8. */ /* __restrict is known in EGCS 1.2 and above. */ /* ISO C99 also allows to declare arrays as non-overlapping. The syntax is array_name[restrict] GCC 3.1 supports this. */ # 415 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4 # 1 "/usr/include/x86_64-linux-gnu/bits/wordsize.h" 1 3 4 /* Determine the wordsize from the preprocessor defines. */ # 11 "/usr/include/x86_64-linux-gnu/bits/wordsize.h" 3 4 /* Both x86-64 and x32 use the 64-bit system call interface. */ # 416 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 2 3 4 # 365 "/usr/include/features.h" 2 3 4 /* If we don't have __REDIRECT, prototypes will be missing if __USE_FILE_OFFSET64 but not __USE_LARGEFILE[64]. */ /* Decide whether we can define 'extern inline' functions in headers. */ /* This is here only because every header file already includes this one. Get the definitions of all the appropriate `__stub_FUNCTION' symbols. contains `#define __stub_FUNCTION' when FUNCTION is a stub that will always return failure (and set errno to ENOSYS). */ # 1 "/usr/include/x86_64-linux-gnu/gnu/stubs.h" 1 3 4 /* This file is automatically generated. This file selects the right generated file of `__stub_FUNCTION' macros based on the architecture being compiled for. */ # 1 "/usr/include/x86_64-linux-gnu/gnu/stubs-64.h" 1 3 4 /* This file is automatically generated. It defines a symbol `__stub_FUNCTION' for each function in the C library which is a stub, meaning it will fail every time called, usually setting errno to ENOSYS. */ # 11 "/usr/include/x86_64-linux-gnu/gnu/stubs.h" 2 3 4 # 389 "/usr/include/features.h" 2 3 4 # 26 "/usr/include/limits.h" 2 3 4 /* Maximum length of any multibyte character in any locale. We define this value here since the gcc header does not define the correct value. */ /* If we are not using GNU CC we have to define all the symbols ourself. Otherwise use gcc's definitions (see below). */ # 116 "/usr/include/limits.h" 3 4 /* Get the compiler's limits.h, which defines almost all the ISO constants. We put this #include_next outside the double inclusion check because it should be possible to include this file more than once and still get the definitions from gcc's header. */ /* The files in some gcc versions don't define LLONG_MIN, LLONG_MAX, and ULLONG_MAX. Instead only the values gcc defined for ages are available. */ # 142 "/usr/include/limits.h" 3 4 /* POSIX adds things to . */ # 1 "/usr/include/x86_64-linux-gnu/bits/posix1_lim.h" 1 3 4 /* Copyright (C) 1991-2016 Free Software Foundation, Inc. This file is part of the GNU C Library. The GNU C Library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. The GNU C Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with the GNU C Library; if not, see . */ /* * POSIX Standard: 2.9.2 Minimum Values Added to * * Never include this file directly; use instead. */ /* These are the standard-mandated minimum values. */ /* Minimum number of operations in one list I/O call. */ /* Minimal number of outstanding asynchronous I/O operations. */ /* Maximum length of arguments to `execve', including environment. */ /* Maximum simultaneous processes per real user ID. */ /* Minimal number of timer expiration overruns. */ /* Maximum length of a host name (not including the terminating null) as returned from the GETHOSTNAME function. */ /* Maximum link count of a file. */ /* Maximum length of login name. */ /* Number of bytes in a terminal canonical input queue. */ /* Number of bytes for which space will be available in a terminal input queue. */ /* Maximum number of message queues open for a process. */ /* Maximum number of supported message priorities. */ /* Number of bytes in a filename. */ /* Number of simultaneous supplementary group IDs per process. */ /* Number of files one process can have open at once. */ # 95 "/usr/include/x86_64-linux-gnu/bits/posix1_lim.h" 3 4 /* Number of bytes in a pathname. */ /* Number of bytes than can be written atomically to a pipe. */ /* The number of repeated occurrences of a BRE permitted by the REGEXEC and REGCOMP functions when using the interval notation. */ /* Minimal number of realtime signals reserved for the application. */ /* Number of semaphores a process can have. */ /* Maximal value of a semaphore. */ /* Number of pending realtime signals. */ /* Largest value of a `ssize_t'. */ /* Number of streams a process can have open at once. */ /* The number of bytes in a symbolic link. */ /* The number of symbolic links that can be traversed in the resolution of a pathname in the absence of a loop. */ /* Number of timer for a process. */ /* Maximum number of characters in a tty name. */ /* Maximum length of a timezone name (element of `tzname'). */ # 155 "/usr/include/x86_64-linux-gnu/bits/posix1_lim.h" 3 4 /* Maximum clock resolution in nanoseconds. */ /* Get the implementation-specific values for the above. */ # 1 "/usr/include/x86_64-linux-gnu/bits/local_lim.h" 1 3 4 /* Minimum guaranteed maximum values for system limits. Linux version. Copyright (C) 1993-2016 Free Software Foundation, Inc. This file is part of the GNU C Library. The GNU C Library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. The GNU C Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with the GNU C Library; see the file COPYING.LIB. If not, see . */ /* The kernel header pollutes the namespace with the NR_OPEN symbol and defines LINK_MAX although filesystems have different maxima. A similar thing is true for OPEN_MAX: the limit can be changed at runtime and therefore the macro must not be defined. Remove this after including the header if necessary. */ # 37 "/usr/include/x86_64-linux-gnu/bits/local_lim.h" 3 4 /* The kernel sources contain a file with all the needed information. */ # 1 "/usr/include/linux/limits.h" 1 3 4 # 39 "/usr/include/x86_64-linux-gnu/bits/local_lim.h" 2 3 4 /* Have to remove NR_OPEN? */ /* Have to remove LINK_MAX? */ /* Have to remove OPEN_MAX? */ /* Have to remove ARG_MAX? */ /* The number of data keys per process. */ /* This is the value this implementation supports. */ /* Controlling the iterations of destructors for thread-specific data. */ /* Number of iterations this implementation does. */ /* The number of threads per process. */ /* We have no predefined limit on the number of threads. */ /* Maximum amount by which a process can descrease its asynchronous I/O priority level. */ /* Minimum size for a thread. We are free to choose a reasonable value. */ /* Maximum number of timer expiration overruns. */ /* Maximum tty name length. */ /* Maximum login name length. This is arbitrary. */ /* Maximum host name length. */ /* Maximum message queue priority level. */ /* Maximum value the semaphore can have. */ # 161 "/usr/include/x86_64-linux-gnu/bits/posix1_lim.h" 2 3 4 /* This value is a guaranteed minimum maximum. The current maximum can be got from `sysconf'. */ # 144 "/usr/include/limits.h" 2 3 4 # 1 "/usr/include/x86_64-linux-gnu/bits/posix2_lim.h" 1 3 4 /* Copyright (C) 1991-2016 Free Software Foundation, Inc. This file is part of the GNU C Library. The GNU C Library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. The GNU C Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with the GNU C Library; if not, see . */ /* * Never include this file directly; include instead. */ /* The maximum `ibase' and `obase' values allowed by the `bc' utility. */ /* The maximum number of elements allowed in an array by the `bc' utility. */ /* The maximum `scale' value allowed by the `bc' utility. */ /* The maximum length of a string constant accepted by the `bc' utility. */ /* The maximum number of weights that can be assigned to an entry of the LC_COLLATE `order' keyword in the locale definition file. */ /* The maximum number of expressions that can be nested within parentheses by the `expr' utility. */ /* The maximum length, in bytes, of an input line. */ /* The maximum number of repeated occurrences of a regular expression permitted when using the interval notation `\{M,N\}'. */ /* The maximum number of bytes in a character class name. We have no fixed limit, 2048 is a high number. */ /* These values are implementation-specific, and may vary within the implementation. Their precise values can be obtained from sysconf. */ # 87 "/usr/include/x86_64-linux-gnu/bits/posix2_lim.h" 3 4 /* This value is defined like this in regex.h. */ # 148 "/usr/include/limits.h" 2 3 4 # 169 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/limits.h" 2 3 4 # 8 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/syslimits.h" 2 3 4 # 35 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/limits.h" 2 3 4 /* Copyright (C) 1991-2016 Free Software Foundation, Inc. This file is part of GCC. GCC is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3, or (at your option) any later version. GCC is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. Under Section 7 of GPL version 3, you are granted additional permissions described in the GCC Runtime Library Exception, version 3.1, as published by the Free Software Foundation. You should have received a copy of the GNU General Public License and a copy of the GCC Runtime Library Exception along with this program; see the files COPYING3 and COPYING.RUNTIME respectively. If not, see . */ /* Number of bits in a `char'. */ /* Maximum length of a multibyte character. */ /* Minimum and maximum values a `signed char' can hold. */ /* Maximum value an `unsigned char' can hold. (Minimum is 0). */ /* Minimum and maximum values a `char' can hold. */ # 102 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/limits.h" 3 4 /* Minimum and maximum values a `signed short int' can hold. */ /* Maximum value an `unsigned short int' can hold. (Minimum is 0). */ /* Minimum and maximum values a `signed int' can hold. */ /* Maximum value an `unsigned int' can hold. (Minimum is 0). */ /* Minimum and maximum values a `signed long int' can hold. (Same as `int'). */ /* Maximum value an `unsigned long int' can hold. (Minimum is 0). */ /* Minimum and maximum values a `signed long long int' can hold. */ /* Maximum value an `unsigned long long int' can hold. (Minimum is 0). */ # 162 "/usr/lib/gcc/x86_64-linux-gnu/6/include-fixed/limits.h" 3 4 /* This administrivia gets added to the end of limits.h if the system has its own version of limits.h. */ # 5 "../../typedefs.h" 2 # 7 "../../typedefs.h" typedef int bool; typedef int value_type; typedef unsigned int size_type; # 6 "../../Logic/ConstantRange.h" 2 /*@ predicate ConstantRange(value_type* a, integer first, integer last, value_type val) = \forall integer i; first <= i < last ==> a[i] == val; */ # 6 "../../Logic/HasConstantSubRange.h" 2 /*@ predicate HasConstantSubRange{A}(value_type* a, integer m, integer n, value_type b) = \exists integer i; 0 <= i <= m-n && ConstantRange(a, i, i+n, b); lemma HasConstantSubRangeSizes: \forall value_type *a, v, integer m, n; HasConstantSubRange(a, m, n, v) ==> n <= m; */ # 6 "search_n.h" 2 /*@ requires valid: \valid_read(a + (0..m-1)); assigns \nothing; ensures result: 0 <= \result <= m; behavior has_match: assumes HasConstantSubRange(a, m, n, b); ensures result: 0 <= \result <= m-n; ensures match: ConstantRange(a, \result, \result+n, b); ensures first: !HasConstantSubRange(a, \result+n-1, n, b); behavior no_match: assumes !HasConstantSubRange(a, m, n, b); ensures result:xxx: \result == m; complete behaviors; disjoint behaviors; */ size_type search_n(const value_type* a, size_type m, size_type n, value_type b); # 3 "search_n.c" 2 size_type search_n(const value_type* a, size_type m, size_type n, value_type b) { if (0u < n) { if (n <= m) { size_type start = 0; /*@ loop invariant constant: ConstantRange(a, start, i, b); loop invariant start: 0 < start ==> a[start-1] != b; loop invariant bound: start <= i + 1; loop invariant not_found: !HasConstantSubRange(a, i, n, b); loop assigns i, start; loop variant m - i; */ for (size_type i = 0; i < m; ++i) { if (a[i] != b) { start = i + 1; } else if (n == i + 1 - start) { return start; } } } return m; } return 0; }