2021-02-24 18:56 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002453Frama-CPlug-in > wppublic2019-07-05 11:41
Reporterjens 
Assigned Tobobot 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C 19-Potassium 
Summary0002453: number of generated files in Frama-C 18 vs 19. beta(2)
DescriptionThis entry references issue
    https://github.com/Frama-C/Frama-C-snapshot/issues/21
in order to be able to easily add files.
Steps To ReproduceRun the command

   frama-c -pp-annot -no-unicode -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast -wp-model Typed+ref -wp-out rc.wp rc.c

on the attached files.
As mentioned in the github issue, both 18.0 and 19.beta(2) report 17 VC of which 5 are discharged by Qed and the remaining 12 are verified by Alt-Ergo.

However, Frama-C 18.0 generates 12 .mlw and .out files, respectively.
Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files, respectively.
The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged by Alt-Ergo.
TagsNo tags attached.
Attached Files
  • c file icon 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);
    }
    
    c file icon rc.c (42,718 bytes) 2019-06-14 13:20 +

-Relationships
+Relationships

-Notes

~0006785

bobot (administrator)

The file names changed and they are perhaps not uniq anymore.

~0006786

correnson (manager)

The files are only generated when Qed did not solve the goals ; what happened is that v19 is much better than v18 at solving with Qed :-)

To get stable results, use the -wp-report option or, even better, the -report and -report-classify utilities.

~0006787

jens (reporter)

I don't understand the last remark as both versions claim that 5 VC were successfully handled by Qed and the remaining 12 by Alt-Ergo. In other words, for this particular example, Qed is not better.

~0006788

bobot (administrator)

Yes there is really a regression, it will be fixed. (However using -report could still be a better idea than looking at the files present ;).)

~0006789

jens (reporter)

Thanks for the clarification and the hints towards "-report"

~0006804

jens (reporter)

It looks like the issue os not present in the final release of Frama-C 19.0

~0006805

bobot (administrator)

Yes it has been fixed, thanks to your report!
+Notes

-Issue History
Date Modified Username Field Change
2019-06-14 13:20 jens New Issue
2019-06-14 13:20 jens Status new => assigned
2019-06-14 13:20 jens Assigned To => correnson
2019-06-14 13:20 jens File Added: rc.c
2019-06-14 14:03 bobot Note Added: 0006785
2019-06-14 14:06 correnson Note Added: 0006786
2019-06-14 14:10 jens Note Added: 0006787
2019-06-14 15:27 bobot Note Added: 0006788
2019-06-14 16:18 jens Note Added: 0006789
2019-06-26 11:52 jens Note Added: 0006804
2019-06-26 15:37 bobot Note Added: 0006805
2019-06-26 15:38 bobot Status assigned => resolved
2019-06-26 15:38 bobot Fixed in Version => Frama-C 19-Potassium
2019-06-26 15:38 bobot Resolution open => fixed
2019-06-26 15:38 bobot Assigned To correnson => bobot
2019-07-05 11:41 signoles Status resolved => closed
+Issue History