2021-01-25 14:04 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002353Frama-CPlug-in > wppublic2019-10-17 18:01
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionno change required 
PlatformSulfur-20171101OSOS VersionUbuntu 17.04
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002353: alt-ergo goals generated directly / via why3 differ in provability
DescriptionI generated an Alt-Ergo proof obligation for the ensures clause "xxx" (line 1140) of the attached program "search_n_standalone.c" (which was obtained from "search_n" in "Acsl by example" by "gcc -E -C"). When I did this directly (see attached script "fd"), it was proven without problems. However, when I did this via Why3 (see script "fw"), Alt-Ergo responded "Don't know" after 0.1 seconds.

In order to compare both mlw files given to Alt-Ergo, I moved the goal of the via-Why3 file into the direct file; it became provable there. Removing as many axioms and definitions as possible while keeping the (non-)provability, I obtained the files "xxx_direct.mlw" and "xxx_via_why3.mlw". It seems that the former defines and uses "shift_sint32", while the latter does not (it uses "shift" instead). Probably, this is the reason for the different outcomes of Alt-Ergo.

Although the observed issue may not be bug (both mlw files may be semanically equivalent), it might be desirable to unify the proof obligations given to Alt-Ergo on different pathways.
TagsNo tags attached.
Attached Files
  • c file icon search_n_standalone.c (35,513 bytes) 2018-02-01 13:27 -
    # 1 "search_n.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-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
       <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 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 <threads.h>.  */
    # 32 "<command-line>" 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
    <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/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
    <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.  */
    # 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
       <http://www.gnu.org/licenses/>.  */
    
    /*
     *	ISO C99 Standard: 7.10/5.2.4.2.1 Sizes of integer types	<limits.h>
     */
    
    
    
    
    # 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
       <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.
       _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
       <http://www.gnu.org/licenses/>.  */
    # 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 <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-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
       <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.  */
    # 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.
       <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
    # 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 <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
    /* POSIX adds things to <limits.h>.  */
    # 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
       <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.
     */
    
    
    
    
    
    /* 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 <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
    # 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
       <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.  */
    # 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
    <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/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;
    }
    
    c file icon search_n_standalone.c (35,513 bytes) 2018-02-01 13:27 +
  • ? file icon fd (382 bytes) 2018-02-01 13:27 -
    #!/bin/sh
    # Call alt-ergo directly
    
    frama-c							\
    	-pp-annot					\
    	-no-unicode					\
    	-wp						\
    	-wp-rte						\
    	-warn-unsigned-overflow				\
    	-warn-unsigned-downcast				\
    	-wp-model Typed+ref				\
    	-wp-prop xxx					\
    	-wp-prover alt-ergo				\
    	-wp-timeout 10					\
    	-wp-steps 10000					\
    	-wp-par 1					\
    	-wp-out search_n_standalone.wp_direct		\
    	search_n_standalone.c
    
    exit
    
    
    ? file icon fd (382 bytes) 2018-02-01 13:27 +
  • ? file icon fw (602 bytes) 2018-02-01 13:28 -
    #!/bin/sh
    # Call alt-ergo via why3
    
    frama-c							\
    	-pp-annot					\
    	-no-unicode					\
    	-wp						\
    	-wp-rte						\
    	-warn-unsigned-overflow				\
    	-warn-unsigned-downcast				\
    	-wp-model Typed+ref				\
    	-wp-prop xxx					\
    	-wp-prover why3					\
    	-wp-out search_n_standalone.wp_why				\
    	-wp-gen search_n_standalone.c
    
    why3							\
    	prove search_n_standalone.wp_why/typed_ref/search_n_Why3_ide.why \
    	-t 10						\
    	--extra-config $FRAMAC_SHARE/wp/why3/why3.conf	\
    	-L search_n_standalone.wp_why/typed_ref			\
    	-L $FRAMAC_SHARE/wp/why3			\
    	-T VCsearch_n_no_match_post_result_xxx		\
    	-P alt-ergo
    
    
    exit
    
    
    ? file icon fw (602 bytes) 2018-02-01 13:28 +
  • ? file icon xxx_direct.mlw (3,871 bytes) 2018-02-01 13:28
  • ? file icon xxx_via_why3.mlw (3,589 bytes) 2018-02-01 13:28

-Relationships
+Relationships

-Notes

~0006516

Jochen (reporter)

I changed some layout and capitalization in the mlw files to reduce their differences found by "diff"; this shouldn't have affected their semantics.

~0006904

correnson (manager)

Actually, the wp-native output for alt-ergo differs from the why3 output for alt-ergo.
The second one is now the default, and the former one will be deprecated.
+Notes

-Issue History
Date Modified Username Field Change
2018-02-01 13:27 Jochen New Issue
2018-02-01 13:27 Jochen Status new => assigned
2018-02-01 13:27 Jochen Assigned To => correnson
2018-02-01 13:27 Jochen File Added: search_n_standalone.c
2018-02-01 13:27 Jochen File Added: fd
2018-02-01 13:28 Jochen File Added: fw
2018-02-01 13:28 Jochen File Added: xxx_direct.mlw
2018-02-01 13:28 Jochen File Added: xxx_via_why3.mlw
2018-02-01 13:31 Jochen Note Added: 0006516
2019-10-17 17:13 correnson Note Added: 0006904
2019-10-17 17:13 correnson Status assigned => resolved
2019-10-17 17:13 correnson Resolution open => no change required
2019-10-17 18:01 signoles Status resolved => closed
+Issue History