rc.c (42,718 bytes)
2019-06-14 13:20 
# 1 "rotate_copy.c"
# 1 "<built-in>"
# 1 "<command-line>"
# 31 "<command-line>"
# 1 "/usr/include/stdc-predef.h" 1 3 4
# 1 "/usr/include/stdc-predef.h" 3 4
/* Copyright (C) 1991-2019 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
<http://www.gnu.org/licenses/>. */
/* 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 <features.h> or any other header that includes
<features.h> 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 10.0.0. Version 10.0 of the Unicode Standard is
synchronized with ISO/IEC 10646:2017, fifth edition, plus
the following additions from Amendment 1 to the fifth edition:
- 56 emoji characters
- 285 hentaigana
- 3 additional Zanabazar Square characters */
# 32 "<command-line>" 2
# 1 "rotate_copy.c"
# 1 "rotate_copy.h" 1
# 1 "../../Logic/EqualRanges.spec" 1
# 1 "../../typedefs.h" 1
# 1 "/usr/lib/gcc/x86_64-linux-gnu/8/include-fixed/limits.h" 1 3 4
/* Copyright (C) 1992-2018 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
<http://www.gnu.org/licenses/>. */
/* 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/8/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/8/include-fixed/limits.h" 1 3 4
/* Copyright (C) 1992-2018 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
<http://www.gnu.org/licenses/>. */
/* 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. */
# 194 "/usr/lib/gcc/x86_64-linux-gnu/8/include-fixed/limits.h" 3 4
# 1 "/usr/include/limits.h" 1 3 4
/* Copyright (C) 1991-2019 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
<http://www.gnu.org/licenses/>. */
/*
* ISO C99 Standard: 7.10/5.2.4.2.1 Sizes of integer types <limits.h>
*/
# 1 "/usr/include/x86_64-linux-gnu/bits/libc-header-start.h" 1 3 4
/* Handle feature test macros at the start of a header.
Copyright (C) 2016-2019 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
<http://www.gnu.org/licenses/>. */
/* This header is internal to glibc and should not be included outside
of glibc headers. Headers including it must define
__GLIBC_INTERNAL_STARTING_HEADER_IMPLEMENTATION first. This header
cannot have multiple include guards because ISO C feature test
macros depend on the definition of the macro when an affected
header is included, not when the first system header is
included. */
# 1 "/usr/include/features.h" 1 3 4
/* Copyright (C) 1991-2019 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
<http://www.gnu.org/licenses/>. */
/* 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.
__STDC_WANT_LIB_EXT2__
Extensions to ISO C99 from TR 27431-2:2010.
__STDC_WANT_IEC_60559_BFP_EXT__
Extensions to ISO C11 from TS 18661-1:2014.
__STDC_WANT_IEC_60559_FUNCS_EXT__
Extensions to ISO C11 from TS 18661-4:2015.
__STDC_WANT_IEC_60559_TYPES_EXT__
Extensions to ISO C11 from TS 18661-3:2015.
_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__).
_FORTIFY_SOURCE Add security hardening to many library functions.
Set to 1 or 2; 2 performs stricter checks than 1.
_REENTRANT, _THREAD_SAFE
Obsolete; equivalent to _POSIX_C_SOURCE=199506L.
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:
__GLIBC_USE (F) Define things from feature set F. This is defined
to 1 or 0; the subsequent macros are either defined
or undefined, and those tests should be moved to
__GLIBC_USE.
__USE_ISOC11 Define ISO C11 things.
__USE_ISOC99 Define ISO C99 things.
__USE_ISOC95 Define ISO C90 AMD1 (C95) things.
__USE_ISOCXX11 Define ISO C++11 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_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.
ISO C feature test macros depend on the definition of the macro
when an affected header is included, not when the first system
header is included, and so they are handled in
<bits/libc-header-start.h>, which does not have a multiple include
guard. Feature test macros that can be handled from the first
system header included are handled here. */
/* Undefine everything, so we get a clean slate. */
# 145 "/usr/include/features.h" 3 4
/* Suppress kernel-name space pollution unless user expressedly asks
for it. */
/* Convenience macro to test the version of gcc.
Use like this:
#if __GNUC_PREREQ (2,8)
... code requiring gcc 2.8 or later ...
#endif
Note: only works for GCC 2.0 and later, because __GNUC_MINOR__ was
added in 2.0. */
/* Similarly for clang. Features added to GCC after version 4.2 may
or may not also be available in clang, and clang's definitions of
__GNUC(_MINOR)__ are fixed at 4 and 2 respectively. Not all such
features can be queried via __has_extension/__has_feature. */
/* Whether to use feature set F. */
/* _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. */
# 214 "/usr/include/features.h" 3 4
/* If nothing (other than _GNU_SOURCE and _DEFAULT_SOURCE) is defined,
define _DEFAULT_SOURCE. */
# 225 "/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. */
# 256 "/usr/include/features.h" 3 4
/* 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). */
# 285 "/usr/include/features.h" 3 4
/* Some C libraries once required _REENTRANT and/or _THREAD_SAFE to be
defined in all multithreaded code. GNU libc has not required this
for many years. We now treat them as compatibility synonyms for
_POSIX_C_SOURCE=199506L, which is the earliest level of POSIX with
comprehensive support for multithreaded code. Using them never
lowers the selected level of POSIX conformance, only raises it. */
# 391 "/usr/include/features.h" 3 4
/* The function 'gets' existed in C89, but is impossible to use
safely. It has been removed from ISO C11 and ISO C++14. Note: for
compatibility with various implementations of <cstdio>, this test
must consider only the value of __cplusplus when compiling C++. */
/* GNU formerly extended the scanf functions with modified format
specifiers %as, %aS, and %a[...] that allocate a buffer for the
input using malloc. This extension conflicts with ISO C99, which
defines %a as a standalone format specifier that reads a floating-
point number; moreover, POSIX.1-2008 provides the same feature
using the modifier letter 'm' instead (%ms, %mS, %m[...]).
We now follow C99 unless GNU extensions are active and the compiler
is specifically in C89 or C++98 mode (strict or not). For
instance, with GCC, -std=gnu11 will have C99-compliant scanf with
or without -D_GNU_SOURCE, but -std=c89 -D_GNU_SOURCE will have the
old extension. */
# 422 "/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-2019 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
<http://www.gnu.org/licenses/>. */
# 425 "/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 <gnu/lib-names.h> 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-2019 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
<http://www.gnu.org/licenses/>. */
/* 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. */
# 88 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* Compilers that are not clang may object to
#if defined __clang__ && __has_extension(...)
even though they do not need to evaluate the right-hand side of the &&. */
/* 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++. */
# 122 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* Fortify support. */
# 138 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* Support for flexible arrays.
Headers that should use flexible arrays only if they're "real"
(e.g. only if they won't affect sizeof()) should test
#if __glibc_c99_flexarr_available. */
# 162 "/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); */
# 189 "/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. */
# 249 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* Since version 3.2, gcc allows marking deprecated functions. */
/* Since version 4.5, gcc also allows one to specify the message printed
when a deprecated function is used. clang claims to be gcc 4.2, but
may also support this feature. */
# 267 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* 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. */
# 313 "/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 for by using the __GNUC_STDC_INLINE_ and
__GNUC_GNU_INLINE__ macro definitions. */
# 359 "/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. */
# 383 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* ISO C99 also allows to declare arrays as non-overlapping. The syntax is
array_name[restrict]
GCC 3.1 supports this. */
# 426 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* Describes a char array whose address can safely be passed as the first
argument to strncpy and strncat, as the char array is not necessarily
a NUL-terminated string. */
/* Undefine (also defined in libc-symbols.h). */
# 452 "/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. */
# 13 "/usr/include/x86_64-linux-gnu/bits/wordsize.h" 3 4
/* Both x86-64 and x32 use the 64-bit system call interface. */
# 453 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 2 3 4
# 1 "/usr/include/x86_64-linux-gnu/bits/long-double.h" 1 3 4
/* Properties of long double type. ldbl-96 version.
Copyright (C) 2016-2019 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 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
<http://www.gnu.org/licenses/>. */
/* long double is distinct from double, so there is nothing to
define here. */
# 454 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 2 3 4
# 487 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* __glibc_macro_warning (MESSAGE) issues warning MESSAGE. This is
intended for use in preprocessor macros.
Note: MESSAGE must be a _single_ string; concatenation of string
literals is not supported. */
# 500 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
/* Generic selection (ISO C11) is a C-only feature, available in GCC
since version 4.9. Previous versions do not provide generic
selection, even though they might set __STDC_VERSION__ to 201112L,
when in -std=c11 mode. Thus, we must check for !defined __GNUC__
when testing __STDC_VERSION__ for generic selection support.
On the other hand, Clang also defines __GNUC__, so a clang-specific
check is required to enable the use of generic selection. */
# 447 "/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.
<gnu/stubs.h> 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
# 471 "/usr/include/features.h" 2 3 4
# 34 "/usr/include/x86_64-linux-gnu/bits/libc-header-start.h" 2 3 4
/* ISO/IEC TR 24731-2:2010 defines the __STDC_WANT_LIB_EXT2__
macro. */
# 45 "/usr/include/x86_64-linux-gnu/bits/libc-header-start.h" 3 4
/* ISO/IEC TS 18661-1:2014 defines the __STDC_WANT_IEC_60559_BFP_EXT__
macro. */
/* ISO/IEC TS 18661-4:2015 defines the
__STDC_WANT_IEC_60559_FUNCS_EXT__ macro. */
/* ISO/IEC TS 18661-3:2015 defines the
__STDC_WANT_IEC_60559_TYPES_EXT__ macro. */
# 27 "/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). */
# 117 "/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 <limits.h> 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
/* The integer width macros are not defined by GCC's <limits.h> before
GCC 7, or if _GNU_SOURCE rather than
__STDC_WANT_IEC_60559_BFP_EXT__ is used to enable this feature. */
# 182 "/usr/include/limits.h" 3 4
/* POSIX adds things to <limits.h>. */
# 1 "/usr/include/x86_64-linux-gnu/bits/posix1_lim.h" 1 3 4
/* Copyright (C) 1991-2019 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
<http://www.gnu.org/licenses/>. */
/*
* POSIX Standard: 2.9.2 Minimum Values Added to <limits.h>
*
* Never include this file directly; use <limits.h> instead.
*/
# 1 "/usr/include/x86_64-linux-gnu/bits/wordsize.h" 1 3 4
/* Determine the wordsize from the preprocessor defines. */
# 13 "/usr/include/x86_64-linux-gnu/bits/wordsize.h" 3 4
/* Both x86-64 and x32 use the 64-bit system call interface. */
# 28 "/usr/include/x86_64-linux-gnu/bits/posix1_lim.h" 2 3 4
/* 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. */
# 96 "/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'). */
# 156 "/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-2019 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 <http://www.gnu.org/licenses/>. */
/* 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
/* SPDX-License-Identifier: GPL-2.0 WITH Linux-syscall-note */
# 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. */
# 162 "/usr/include/x86_64-linux-gnu/bits/posix1_lim.h" 2 3 4
/* ssize_t is not formally required to be the signed type
corresponding to size_t, but it is for all configurations supported
by glibc. */
# 176 "/usr/include/x86_64-linux-gnu/bits/posix1_lim.h" 3 4
/* This value is a guaranteed minimum maximum.
The current maximum can be got from `sysconf'. */
# 184 "/usr/include/limits.h" 2 3 4
# 1 "/usr/include/x86_64-linux-gnu/bits/posix2_lim.h" 1 3 4
/* Copyright (C) 1991-2019 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
<http://www.gnu.org/licenses/>. */
/*
* Never include this file directly; include <limits.h> 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. */
# 188 "/usr/include/limits.h" 2 3 4
# 195 "/usr/lib/gcc/x86_64-linux-gnu/8/include-fixed/limits.h" 2 3 4
# 8 "/usr/lib/gcc/x86_64-linux-gnu/8/include-fixed/syslimits.h" 2 3 4
# 35 "/usr/lib/gcc/x86_64-linux-gnu/8/include-fixed/limits.h" 2 3 4
/* Copyright (C) 1991-2018 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
<http://www.gnu.org/licenses/>. */
/* 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/8/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). */
# 188 "/usr/lib/gcc/x86_64-linux-gnu/8/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/EqualRanges.spec" 2
/*@
predicate
EqualRanges{K,L}(value_type* a, integer n, value_type* b) =
\forall integer i; 0 <= i < n ==> \at(a[i],K) == \at(b[i],L);
predicate
EqualRanges{K,L}(value_type* a, integer m, integer n, value_type* b) =
\forall integer i; m <= i < n ==> \at(a[i],K) == \at(b[i],L);
predicate
EqualRanges{K,L}(value_type* a, integer m, integer n,
value_type* b, integer p) =
EqualRanges{K,L}(a+m, n-m, b+p);
predicate
EqualRanges{K,L}(value_type* a, integer m, integer n, integer p) =
EqualRanges{K,L}(a, m, n, a, p);
*/
# 6 "rotate_copy.h" 2
# 1 "../../Logic/Unchanged.spec" 1
# 1 "../../Logic/EqualRanges.spec" 1
# 6 "../../Logic/Unchanged.spec" 2
/*@
predicate
Unchanged{K,L}(value_type* a, integer m, integer n) =
\forall integer i; m <= i < n ==> \at(a[i],K) == \at(a[i],L);
predicate
Unchanged{K,L}(value_type* a, integer n) =
Unchanged{K,L}(a, 0, n);
*/
# 7 "rotate_copy.h" 2
/*@
requires bound: 0 <= m <= n;
requires valid: \valid_read(a + (0..n-1));
requires valid: \valid(b + (0..n-1));
requires sep: \separated(a + (0..n-1), b + (0..n-1));
assigns b[0..(n-1)];
ensures left: EqualRanges{Old,Here}(a, 0, m, b, n-m);
ensures right: EqualRanges{Old,Here}(a, m, n-m, b, 0);
ensures unchanged: Unchanged{Old,Here}(a, n);
*/
void
rotate_copy(const value_type* a, size_type m, size_type n, value_type* b);
# 3 "rotate_copy.c" 2
# 1 "../copy/copy.h" 1
/*@
requires valid: \valid_read(a + (0..n-1));
requires valid: \valid(b + (0..n-1));
requires sep: \separated(a + (0..n-1), b);
assigns b[0..n-1];
ensures equal: EqualRanges{Old,Here}(a, n, b);
*/
void
copy(const value_type* a, const size_type n, value_type* b);
# 4 "rotate_copy.c" 2
void
rotate_copy(const value_type* a, size_type m, size_type n, value_type* b)
{
copy(a, m, b + (n - m));
copy(a + m, n - m, b);
}
Relationships