From fc5867e12ba3d8947cf39d4d98c0093284e3c0a4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 27 Jan 2022 17:19:46 +0100
Subject: [PATCH] =?UTF-8?q?[libc]=20Avoid=20making=20knots=20=F0=9F=AA=A2?=
=?UTF-8?q?=20with=20includes=20in=20the=20libc?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
share/libc/__fc_gcc_builtins.h | 207 +++----
.../tests/bts/oracle/gen_issue-eacsl-40.c | 14 +-
.../bts/oracle/issue-eacsl-40.0.res.oracle | 36 +-
.../oracle/parallel_threads.res.oracle | 4 +-
.../oracle/threads_debug.res.oracle | 4 +-
.../e-acsl/tests/libc/oracle/file.res.oracle | 36 +-
.../e-acsl/tests/libc/oracle/gen_file.c | 14 +-
.../tests/erroneous/oracle/printf.res.oracle | 4 +-
.../tests/known/oracle/printf.res.oracle | 4 +-
.../oracle/printf_garbled_mix.res.oracle | 4 +-
.../oracle/printf_wrong_arity.res.oracle | 4 +-
.../oracle/printf_wrong_pointers.res.oracle | 4 +-
.../oracle/printf_wrong_types.res.oracle | 8 +-
.../tests/known/oracle/scanf.res.oracle | 4 +-
.../tests/known/oracle/scanf_loop.res.oracle | 4 +-
.../tests/known/oracle/scanf_wrong.res.oracle | 4 +-
.../tests/known/oracle/snprintf.res.oracle | 4 +-
.../tests/known/oracle/stdio_print.res.oracle | 4 +-
.../tests/known/oracle/stdio_scan.res.oracle | 4 +-
.../tests/known/oracle/swprintf.res.oracle | 4 +-
.../tests/known/oracle/wchar.res.oracle | 4 +-
tests/idct/oracle/ieee_1180_1990.res.oracle | 244 ++++----
tests/libc/oracle/fc_libc.1.res.oracle | 572 +++++++++++++++++-
tests/libc/oracle/time_misc.res.oracle | 2 +-
tests/rte/oracle/value_rte.res.oracle | 238 ++++----
25 files changed, 1003 insertions(+), 428 deletions(-)
diff --git a/share/libc/__fc_gcc_builtins.h b/share/libc/__fc_gcc_builtins.h
index 1335394831f..ea170e8855e 100644
--- a/share/libc/__fc_gcc_builtins.h
+++ b/share/libc/__fc_gcc_builtins.h
@@ -25,9 +25,8 @@
#ifndef __FC_GCC_BUILTINS
#define __FC_GCC_BUILTINS
-#include "features.h"
#include "__fc_machdep.h"
-#include "__fc_define_size_t.h"
+#include "features.h"
__PUSH_FC_STDLIB
@@ -40,7 +39,7 @@ __BEGIN_DECLS
ensures res_wrapped: *res == (int)(a + b);
ensures result_overflow: a + b == (int)(a + b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_sadd_overflow (int a, int b, int *res);
+_Bool __builtin_sadd_overflow(int a, int b, int* res);
/*@
requires valid_res: \valid(res);
@@ -49,7 +48,7 @@ _Bool __builtin_sadd_overflow (int a, int b, int *res);
ensures res_wrapped: *res == (long)(a + b);
ensures result_overflow: a + b == (long)(a + b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_saddl_overflow (long a, long b, long *res);
+_Bool __builtin_saddl_overflow(long a, long b, long* res);
/*@
requires valid_res: \valid(res);
@@ -58,7 +57,7 @@ _Bool __builtin_saddl_overflow (long a, long b, long *res);
ensures res_wrapped: *res == (long long)(a + b);
ensures result_overflow: a + b == (long long)(a + b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_saddll_overflow (long long a, long long b, long long *res);
+_Bool __builtin_saddll_overflow(long long a, long long b, long long* res);
/*@
requires valid_res: \valid(res);
@@ -67,7 +66,7 @@ _Bool __builtin_saddll_overflow (long long a, long long b, long long *res);
ensures res_wrapped: *res == (unsigned)(a + b);
ensures result_overflow: a + b == (unsigned)(a + b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_uadd_overflow (unsigned a, unsigned b, unsigned *res);
+_Bool __builtin_uadd_overflow(unsigned a, unsigned b, unsigned* res);
/*@
requires valid_res: \valid(res);
@@ -76,7 +75,7 @@ _Bool __builtin_uadd_overflow (unsigned a, unsigned b, unsigned *res);
ensures res_wrapped: *res == (unsigned long)(a + b);
ensures result_overflow: a + b == (unsigned long)(a + b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_uaddl_overflow (unsigned long a, unsigned long b, unsigned long *res);
+_Bool __builtin_uaddl_overflow(unsigned long a, unsigned long b, unsigned long* res);
/*@
requires valid_res: \valid(res);
@@ -85,7 +84,7 @@ _Bool __builtin_uaddl_overflow (unsigned long a, unsigned long b, unsigned long
ensures res_wrapped: *res == (unsigned long long)(a + b);
ensures result_overflow: a + b == (unsigned long long)(a + b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_uaddll_overflow (unsigned long long a, unsigned long long b, unsigned long long *res);
+_Bool __builtin_uaddll_overflow(unsigned long long a, unsigned long long b, unsigned long long* res);
/*@
requires valid_res: \valid(res);
@@ -94,7 +93,7 @@ _Bool __builtin_uaddll_overflow (unsigned long long a, unsigned long long b, uns
ensures res_wrapped: *res == (int)(a - b);
ensures result_overflow: a - b == (int)(a - b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_ssub_overflow (int a, int b, int *res);
+_Bool __builtin_ssub_overflow(int a, int b, int* res);
/*@
requires valid_res: \valid(res);
@@ -103,7 +102,7 @@ _Bool __builtin_ssub_overflow (int a, int b, int *res);
ensures res_wrapped: *res == (long)(a - b);
ensures result_overflow: a - b == (long)(a - b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_ssubl_overflow (long a, long b, long *res);
+_Bool __builtin_ssubl_overflow(long a, long b, long* res);
/*@
requires valid_res: \valid(res);
@@ -112,7 +111,7 @@ _Bool __builtin_ssubl_overflow (long a, long b, long *res);
ensures res_wrapped: *res == (long long)(a - b);
ensures result_overflow: a - b == (long long)(a - b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_ssubll_overflow (long long a, long long b, long long *res);
+_Bool __builtin_ssubll_overflow(long long a, long long b, long long* res);
/*@
requires valid_res: \valid(res);
@@ -121,7 +120,7 @@ _Bool __builtin_ssubll_overflow (long long a, long long b, long long *res);
ensures res_wrapped: *res == (unsigned)(a - b);
ensures result_overflow: a - b == (unsigned)(a - b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_usub_overflow (unsigned a, unsigned b, unsigned *res);
+_Bool __builtin_usub_overflow(unsigned a, unsigned b, unsigned* res);
/*@
requires valid_res: \valid(res);
@@ -130,7 +129,7 @@ _Bool __builtin_usub_overflow (unsigned a, unsigned b, unsigned *res);
ensures res_wrapped: *res == (unsigned long)(a - b);
ensures result_overflow: a - b == (unsigned long)(a - b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_usubl_overflow (unsigned long a, unsigned long b, unsigned long *res);
+_Bool __builtin_usubl_overflow(unsigned long a, unsigned long b, unsigned long* res);
/*@
requires valid_res: \valid(res);
@@ -139,7 +138,7 @@ _Bool __builtin_usubl_overflow (unsigned long a, unsigned long b, unsigned long
ensures res_wrapped: *res == (unsigned long long)(a - b);
ensures result_overflow: a - b == (unsigned long long)(a - b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_usubll_overflow (unsigned long long a, unsigned long long b, unsigned long long *res);
+_Bool __builtin_usubll_overflow(unsigned long long a, unsigned long long b, unsigned long long* res);
/*@
requires valid_res: \valid(res);
@@ -148,7 +147,7 @@ _Bool __builtin_usubll_overflow (unsigned long long a, unsigned long long b, uns
ensures res_wrapped: *res == (int)(a * b);
ensures result_overflow: a * b == (int)(a * b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_smul_overflow (int a, int b, int *res);
+_Bool __builtin_smul_overflow(int a, int b, int* res);
/*@
requires valid_res: \valid(res);
@@ -157,7 +156,7 @@ _Bool __builtin_smul_overflow (int a, int b, int *res);
ensures res_wrapped: *res == (long)(a * b);
ensures result_overflow: a * b == (long)(a * b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_smull_overflow (long a, long b, long *res);
+_Bool __builtin_smull_overflow(long a, long b, long* res);
/*@
requires valid_res: \valid(res);
@@ -166,7 +165,7 @@ _Bool __builtin_smull_overflow (long a, long b, long *res);
ensures res_wrapped: *res == (long long)(a * b);
ensures result_overflow: a * b == (long long)(a * b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_smulll_overflow (long long a, long long b, long long *res);
+_Bool __builtin_smulll_overflow(long long a, long long b, long long* res);
/*@
requires valid_res: \valid(res);
@@ -175,7 +174,7 @@ _Bool __builtin_smulll_overflow (long long a, long long b, long long *res);
ensures res_wrapped: *res == (unsigned)(a * b);
ensures result_overflow: a * b == (unsigned)(a * b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_umul_overflow (unsigned a, unsigned b, unsigned *res);
+_Bool __builtin_umul_overflow(unsigned a, unsigned b, unsigned* res);
/*@
requires valid_res: \valid(res);
@@ -184,7 +183,7 @@ _Bool __builtin_umul_overflow (unsigned a, unsigned b, unsigned *res);
ensures res_wrapped: *res == (unsigned long)(a * b);
ensures result_overflow: a * b == (unsigned long)(a * b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_umull_overflow (unsigned long a, unsigned long b, unsigned long *res);
+_Bool __builtin_umull_overflow(unsigned long a, unsigned long b, unsigned long* res);
/*@
requires valid_res: \valid(res);
@@ -193,67 +192,67 @@ _Bool __builtin_umull_overflow (unsigned long a, unsigned long b, unsigned long
ensures res_wrapped: *res == (unsigned long long)(a * b);
ensures result_overflow: a * b == (unsigned long long)(a * b) ? \result == 0 : \result == 1;
*/
-_Bool __builtin_umulll_overflow (unsigned long long a, unsigned long long b, unsigned long long *res);
+_Bool __builtin_umulll_overflow(unsigned long long a, unsigned long long b, unsigned long long* res);
/*@
requires x_nonzero: x != 0;
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
*/
-int __builtin_clz (unsigned int x);
+int __builtin_clz(unsigned int x);
/*@
requires x_nonzero: x != 0;
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
*/
-int __builtin_clzl (unsigned long x);
+int __builtin_clzl(unsigned long x);
/*@
requires x_nonzero: x != 0;
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
*/
-int __builtin_clzll (unsigned long long x);
+int __builtin_clzll(unsigned long long x);
/*@
requires x_nonzero: x != 0;
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
*/
-int __builtin_ctz (unsigned int x);
+int __builtin_ctz(unsigned int x);
/*@
requires x_nonzero: x != 0;
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
*/
-int __builtin_ctzl (unsigned long x);
+int __builtin_ctzl(unsigned long x);
/*@
requires x_nonzero: x != 0;
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
*/
-int __builtin_ctzll (unsigned long long x);
+int __builtin_ctzll(unsigned long long x);
/*@
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result <= __CHAR_BIT * sizeof(x);
*/
-int __builtin_popcount (unsigned int x);
+int __builtin_popcount(unsigned int x);
/*@
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result <= __CHAR_BIT * sizeof(x);
*/
-int __builtin_popcountl (unsigned long x);
+int __builtin_popcountl(unsigned long x);
/*@
assigns \result \from indirect:x;
ensures result_is_bit_count: 0 <= \result <= __CHAR_BIT * sizeof(x);
*/
-int __builtin_popcountll (unsigned long long x);
+int __builtin_popcountll(unsigned long long x);
// GCC specialized __atomic_* functions.
// TODO: add generic counterpart with some help from cabs2cil for typing
@@ -265,28 +264,28 @@ int __builtin_popcountll (unsigned long long x);
assigns \result \from *mem, indirect:model;
ensures load_value: \result == *mem;
*/
-__UINT8_T __atomic_load_1(__UINT8_T* mem, int model);
+__UINT8_T __atomic_load_1(const __UINT8_T* mem, int model);
/*@
requires validity: \valid_read(mem);
assigns \result \from *mem, indirect: model;
ensures load_value: \result == *mem;
*/
-__UINT16_T __atomic_load_2(__UINT16_T* mem, int model);
+__UINT16_T __atomic_load_2(const __UINT16_T* mem, int model);
/*@
requires validity: \valid_read(mem);
assigns \result \from *mem, indirect:model;
ensures load_value: \result == *mem;
*/
-__UINT32_T __atomic_load_4(__UINT32_T* mem, int model);
+__UINT32_T __atomic_load_4(const __UINT32_T* mem, int model);
/*@
requires validity: \valid_read(mem);
assigns \result \from *mem, indirect:model;
ensures load_value: \result == *mem;
*/
-__UINT64_T __atomic_load_8(__UINT64_T* mem, int model);
+__UINT64_T __atomic_load_8(const __UINT64_T* mem, int model);
/*@
requires validity: \valid(mem);
@@ -347,11 +346,12 @@ __UINT64_T __atomic_exchange_8(__UINT64_T* mem, __UINT64_T val, int model);
indirect: failure_model, indirect: weak;
assigns \result \from indirect: *mem, indirect: *expected;
*/
-_Bool __atomic_compare_exchange_1(
- __UINT8_T* mem,
- __UINT8_T* expected,
- __UINT8_T desired,
- _Bool weak, int success_model, int failure_model);
+_Bool __atomic_compare_exchange_1(__UINT8_T* mem,
+ __UINT8_T* expected,
+ __UINT8_T desired,
+ _Bool weak,
+ int success_model,
+ int failure_model);
/*@ requires validity: \valid(mem) && \valid_read(expected);
assigns *mem \from *mem, indirect: *expected, desired,
@@ -360,11 +360,12 @@ _Bool __atomic_compare_exchange_1(
indirect: failure_model, indirect: weak;
assigns \result \from indirect: *mem, indirect: *expected;
*/
-_Bool __atomic_compare_exchange_2(
- __UINT16_T* mem,
- __UINT16_T* expected,
- __UINT16_T desired,
- _Bool weak, int success_model, int failure_model);
+_Bool __atomic_compare_exchange_2(__UINT16_T* mem,
+ __UINT16_T* expected,
+ __UINT16_T desired,
+ _Bool weak,
+ int success_model,
+ int failure_model);
/*@ requires validity: \valid(mem) && \valid_read(expected);
assigns *mem \from *mem, indirect: *expected, desired,
@@ -373,11 +374,12 @@ _Bool __atomic_compare_exchange_2(
indirect: failure_model, indirect: weak;
assigns \result \from indirect: *mem, indirect: *expected;
*/
-_Bool __atomic_compare_exchange_4(
- __UINT32_T* mem,
- __UINT32_T* expected,
- __UINT32_T desired,
- _Bool weak, int success_model, int failure_model);
+_Bool __atomic_compare_exchange_4(__UINT32_T* mem,
+ __UINT32_T* expected,
+ __UINT32_T desired,
+ _Bool weak,
+ int success_model,
+ int failure_model);
/*@ requires validity: \valid(mem) && \valid_read(expected);
assigns *mem \from *mem, indirect: *expected, desired,
@@ -386,126 +388,127 @@ _Bool __atomic_compare_exchange_4(
indirect: failure_model, indirect: weak;
assigns \result \from indirect: *mem, indirect: *expected;
*/
-_Bool __atomic_compare_exchange_8(
- __UINT64_T* mem,
- __UINT64_T* expected,
- __UINT64_T desired,
- _Bool weak, int success_model, int failure_model);
+_Bool __atomic_compare_exchange_8(__UINT64_T* mem,
+ __UINT64_T* expected,
+ __UINT64_T desired,
+ _Bool weak,
+ int success_model,
+ int failure_model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_add_fetch_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_add_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_sub_fetch_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_sub_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_and_fetch_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_and_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_xor_fetch_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_xor_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_or_fetch_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_or_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_nand_fetch_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_nand_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_add_fetch_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_add_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_sub_fetch_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_sub_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_and_fetch_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_and_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_xor_fetch_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_xor_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_or_fetch_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_or_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_nand_fetch_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_nand_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_add_fetch_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_add_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_sub_fetch_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_sub_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_and_fetch_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_and_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_xor_fetch_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_xor_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_or_fetch_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_or_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_nand_fetch_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_nand_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_add_fetch_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_add_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_sub_fetch_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_sub_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_and_fetch_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_and_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_xor_fetch_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_xor_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_or_fetch_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_or_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
@@ -515,117 +518,117 @@ __UINT64_T __atomic_nand_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_fetch_add_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_fetch_add_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_fetch_sub_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_fetch_sub_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_fetch_and_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_fetch_and_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_fetch_xor_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_fetch_xor_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_fetch_or_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_fetch_or_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT8_T __atomic_fetch_nand_1 (__UINT8_T *ptr, __UINT8_T val, int model);
+__UINT8_T __atomic_fetch_nand_1(__UINT8_T* ptr, __UINT8_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_fetch_add_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_fetch_add_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_fetch_sub_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_fetch_sub_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_fetch_and_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_fetch_and_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_fetch_xor_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_fetch_xor_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_fetch_or_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_fetch_or_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT16_T __atomic_fetch_nand_2 (__UINT16_T *ptr, __UINT16_T val, int model);
+__UINT16_T __atomic_fetch_nand_2(__UINT16_T* ptr, __UINT16_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_fetch_add_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_fetch_add_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_fetch_sub_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_fetch_sub_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_fetch_and_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_fetch_and_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_fetch_xor_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_fetch_xor_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_fetch_or_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_fetch_or_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT32_T __atomic_fetch_nand_4 (__UINT32_T *ptr, __UINT32_T val, int model);
+__UINT32_T __atomic_fetch_nand_4(__UINT32_T* ptr, __UINT32_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_fetch_add_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_fetch_add_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_fetch_sub__8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_fetch_sub__8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_fetch_and_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_fetch_and_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_fetch_xor_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_fetch_xor_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
*/
-__UINT64_T __atomic_fetch_or_8 (__UINT64_T *ptr, __UINT64_T val, int model);
+__UINT64_T __atomic_fetch_or_8(__UINT64_T* ptr, __UINT64_T val, int model);
/*@ requires validity: \valid(ptr);
assigns \result, *ptr \from *ptr, val, indirect: model;
@@ -636,7 +639,7 @@ __UINT64_T __atomic_fetch_nand_8(__UINT64_T* ptr, __UINT64_T val, int model);
assigns \result \from *((char*)ptr);
assigns *((char*)ptr) \from \nothing;
*/
-_Bool __atomic_test_and_set (void *ptr, int model);
+_Bool __atomic_test_and_set(void* ptr, int model);
/*@ requires validity: \valid(ptr);
assigns *ptr \from \nothing;
@@ -650,10 +653,10 @@ void __atomic_thread_fence(int model);
void __atomic_signal_fence(int model);
/*@ assigns \result \from indirect: size, indirect: ptr; */
-_Bool __atomic_always_lock_free (size_t size, void *ptr);
+_Bool __atomic_always_lock_free(__SIZE_T size, void* ptr);
/*@ assigns \result \from indirect: size, indirect: ptr; */
-_Bool __atomic_lock_free (size_t size, void *ptr);
+_Bool __atomic_lock_free(__SIZE_T size, void* ptr);
// According to the GCC docs
// (https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html),
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
index ff974a15990..3929c369e31 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
@@ -145,7 +145,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_2.pred_txt = "(\\let size = sizeof(char) * (((nmemb * size - 1) - 0) + 1);\n size <= 0? 0: size)\n<= 18446744073709551615";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_2.fct = "fread";
- __gen_e_acsl_assert_data_2.line = 351;
+ __gen_e_acsl_assert_data_2.line = 353;
__gen_e_acsl_assert_data_2.name = "offset_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -176,7 +176,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data.pred_txt = "\\valid((char *)ptr + (0 .. nmemb * size - 1))";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data.fct = "fread";
- __gen_e_acsl_assert_data.line = 351;
+ __gen_e_acsl_assert_data.line = 353;
__gen_e_acsl_assert_data.name = "valid_ptr_block";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -195,7 +195,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_3.pred_txt = "\\valid(stream)";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_3.fct = "fread";
- __gen_e_acsl_assert_data_3.line = 352;
+ __gen_e_acsl_assert_data_3.line = 354;
__gen_e_acsl_assert_data_3.name = "valid_stream";
__e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -242,7 +242,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_4.pred_txt = "__retres * size <= 18446744073709551615";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_4.fct = "fread";
- __gen_e_acsl_assert_data_4.line = 350;
+ __gen_e_acsl_assert_data_4.line = 352;
__gen_e_acsl_assert_data_4.name = "size_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_3 <= 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -281,7 +281,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_5.pred_txt = "\\result <= \\old(nmemb)";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_5.fct = "fread";
- __gen_e_acsl_assert_data_5.line = 356;
+ __gen_e_acsl_assert_data_5.line = 358;
__gen_e_acsl_assert_data_5.name = "size_read";
__e_acsl_assert(__retres <= __gen_e_acsl_at_3,
& __gen_e_acsl_assert_data_5);
@@ -338,7 +338,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_7.pred_txt = "(\\let size = sizeof(char) * (((\\result * \\old(size) - 1) - 0) + 1);\n size <= 0? 0: size)\n<= 18446744073709551615";
__gen_e_acsl_assert_data_7.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_7.fct = "fread";
- __gen_e_acsl_assert_data_7.line = 357;
+ __gen_e_acsl_assert_data_7.line = 359;
__gen_e_acsl_assert_data_7.name = "offset_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_5 <= 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
@@ -372,7 +372,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_6.pred_txt = "\\initialized((char *)\\old(ptr) + (0 .. \\result * \\old(size) - 1))";
__gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_6.fct = "fread";
- __gen_e_acsl_assert_data_6.line = 357;
+ __gen_e_acsl_assert_data_6.line = 359;
__gen_e_acsl_assert_data_6.name = "initialization";
__e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle
index 42cba99e4ca..184cc7c43cb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle
@@ -5,7 +5,7 @@
[e-acsl] Warning: annotating undefined function `fopen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:352: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning:
@@ -30,51 +30,51 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert_register_mpz: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:354: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:354: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:354: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:356: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:358: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert_register_mpz: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert_register_mpz: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __gen_e_acsl_fread: postcondition 'initialization' got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
index 1dfe0498bed..2c771c66bd1 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
@@ -45,13 +45,13 @@
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:484: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:486: Warning:
no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:483: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:485: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/pthread.h:312: Warning:
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
index 1dfe0498bed..2c771c66bd1 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
@@ -45,13 +45,13 @@
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:484: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:486: Warning:
no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:483: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:485: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/pthread.h:312: Warning:
diff --git a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
index 7b2ac7b3ecf..8dca9f2bac2 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
@@ -5,7 +5,7 @@
[e-acsl] Warning: annotating undefined function `fopen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:352: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning:
@@ -32,51 +32,51 @@
[e-acsl] translation done in project "e-acsl".
[eva:alarm] file.c:12: Warning:
function __gen_e_acsl_fread: precondition 'valid_stream' got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:353: Warning:
function __e_acsl_assert_register_mpz: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:354: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:354: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:354: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:356: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:358: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert_register_mpz: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __e_acsl_assert_register_mpz: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:359: Warning:
function __gen_e_acsl_fread: postcondition 'initialization' got status unknown.
[eva:alarm] file.c:13: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
index 7f8b5b42d2c..c71892de480 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
@@ -145,7 +145,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_2.pred_txt = "(\\let size = sizeof(char) * (((nmemb * size - 1) - 0) + 1);\n size <= 0? 0: size)\n<= 18446744073709551615";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_2.fct = "fread";
- __gen_e_acsl_assert_data_2.line = 351;
+ __gen_e_acsl_assert_data_2.line = 353;
__gen_e_acsl_assert_data_2.name = "offset_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -176,7 +176,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data.pred_txt = "\\valid((char *)ptr + (0 .. nmemb * size - 1))";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data.fct = "fread";
- __gen_e_acsl_assert_data.line = 351;
+ __gen_e_acsl_assert_data.line = 353;
__gen_e_acsl_assert_data.name = "valid_ptr_block";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -195,7 +195,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_3.pred_txt = "\\valid(stream)";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_3.fct = "fread";
- __gen_e_acsl_assert_data_3.line = 352;
+ __gen_e_acsl_assert_data_3.line = 354;
__gen_e_acsl_assert_data_3.name = "valid_stream";
__e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -242,7 +242,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_4.pred_txt = "__retres * size <= 18446744073709551615";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_4.fct = "fread";
- __gen_e_acsl_assert_data_4.line = 350;
+ __gen_e_acsl_assert_data_4.line = 352;
__gen_e_acsl_assert_data_4.name = "size_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_3 <= 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -281,7 +281,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_5.pred_txt = "\\result <= \\old(nmemb)";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_5.fct = "fread";
- __gen_e_acsl_assert_data_5.line = 356;
+ __gen_e_acsl_assert_data_5.line = 358;
__gen_e_acsl_assert_data_5.name = "size_read";
__e_acsl_assert(__retres <= __gen_e_acsl_at_3,
& __gen_e_acsl_assert_data_5);
@@ -338,7 +338,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_7.pred_txt = "(\\let size = sizeof(char) * (((\\result * \\old(size) - 1) - 0) + 1);\n size <= 0? 0: size)\n<= 18446744073709551615";
__gen_e_acsl_assert_data_7.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_7.fct = "fread";
- __gen_e_acsl_assert_data_7.line = 357;
+ __gen_e_acsl_assert_data_7.line = 359;
__gen_e_acsl_assert_data_7.name = "offset_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le_5 <= 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
@@ -372,7 +372,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_6.pred_txt = "\\initialized((char *)\\old(ptr) + (0 .. \\result * \\old(size) - 1))";
__gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_6.fct = "fread";
- __gen_e_acsl_assert_data_6.line = 357;
+ __gen_e_acsl_assert_data_6.line = 359;
__gen_e_acsl_assert_data_6.name = "initialization";
__e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index d29a81d7692..709eade7c32 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic:libc:format] printf.c:8: Warning: Multiple usage of flag '-'.
[variadic:libc:format] printf.c:8: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 1dbb2458c3d..7ee761f24d5 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -24,9 +24,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] printf.c:37:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index bea7ff5f3c9..80bb3f1eae2 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] printf_garbled_mix.c:7:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index 14583255222..0769b43d1d7 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] printf_wrong_arity.c:8:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
index 71e13f3012f..61261c69b7f 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] printf_wrong_pointers.c:14:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 2e9b9b017a5..3b67607452b 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
@@ -426,9 +426,9 @@ int main(void)
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
index 15799fe60f4..8bc1110db48 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] scanf.c:7:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
index dd7a3d80783..577e5cfa4ed 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] scanf_loop.c:6:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
index c225e1ea160..292f987963a 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] scanf_wrong.c:8:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index 4e8e4cf6cbc..c96e7311094 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] snprintf.c:12:
Translating call to snprintf to a call to the specialized version snprintf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index 6b7bc896adc..ed6948688d7 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] stdio_print.c:9: Warning:
Call to function fprintf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index 7b439fc5fa6..02012fe664a 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -12,9 +12,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] stdio_scan.c:10: Warning:
Call to function fscanf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 4976f7d1494..c31c436e505 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -24,9 +24,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] swprintf.c:12:
Translating call to swprintf to a call to the specialized version swprintf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index 64c5c703458..f1a366040cb 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -24,9 +24,9 @@
Declaration of variadic function sprintf.
[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:548:
+[variadic] FRAMAC_SHARE/libc/stdio.h:550:
Declaration of variadic function dprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:608:
+[variadic] FRAMAC_SHARE/libc/stdio.h:610:
Declaration of variadic function asprintf.
[variadic] wchar.c:11:
Translating call to wprintf to a call to the specialized version wprintf_va_1.
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 6fcda71f59a..2b84b5e6d38 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1337,10 +1337,14 @@
--------------------------------------------------------------------------------
[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 220)
- assigns *stream;
+ assigns *stream, \result;
Unverifiable but considered Valid.
[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 220)
- assigns *stream \from *(format + (..)), arg;
+ assigns *stream \from *(format + (..)), (indirect: arg);
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 221)
+ assigns \result
+ \from (indirect: *(format + (..))), (indirect: arg);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1350,10 +1354,10 @@
--- Properties of Function 'vfscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 225)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 227)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 225)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 227)
assigns *stream \from *(format + (..)), *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1364,10 +1368,10 @@
--- Properties of Function 'vprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 231)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 233)
assigns *__fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 231)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 233)
assigns *__fc_stdout \from arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1378,10 +1382,10 @@
--- Properties of Function 'vscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 235)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 237)
assigns *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 235)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 237)
assigns *__fc_stdin \from *(format + (..));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1392,10 +1396,10 @@
--- Properties of Function 'vsnprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 240)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 242)
assigns *(s + (0 .. n - 1));
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 240)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 242)
assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1406,10 +1410,10 @@
--- Properties of Function 'vsprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 246)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 248)
assigns *(s + (0 ..));
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 246)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 248)
assigns *(s + (0 ..)) \from *(format + (..)), arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1424,13 +1428,13 @@
ensures
result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 259)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 261)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 259)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 261)
assigns *stream \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 260)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 262)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1455,14 +1459,14 @@
terminated_string_on_success:
\result ≢ \null ⇒ valid_string(\old(s))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 268)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 270)
assigns *(s + (0 .. size - 1)), \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 268)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 270)
assigns *(s + (0 .. size - 1))
\from (indirect: size), (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 269)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 271)
assigns \result \from s, (indirect: size), (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1473,13 +1477,13 @@
--- Properties of Function 'fputc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 282)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 284)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 282)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 284)
assigns *stream \from c, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 283)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 285)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1490,13 +1494,13 @@
--- Properties of Function 'fputs'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 289)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 291)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 289)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 291)
assigns *stream \from *(s + (0 .. strlen{Old}(s))), *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 290)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 292)
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))),
(indirect: *stream);
@@ -1509,13 +1513,13 @@
--- Properties of Function 'getc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 297)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 299)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 297)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 299)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 297)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 299)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1526,13 +1530,13 @@
--- Properties of Function 'getchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 302)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 304)
assigns \result, *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 302)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 304)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 302)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 304)
assigns *__fc_stdin \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1547,16 +1551,16 @@
ensures
result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 315)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 317)
assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 315)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 317)
assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 316)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 318)
assigns \result \from s, *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 317)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 319)
assigns *__fc_stdin \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1567,13 +1571,13 @@
--- Properties of Function 'putc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 324)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 326)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 324)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 326)
assigns *stream \from c, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 325)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 327)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1584,13 +1588,13 @@
--- Properties of Function 'putchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 330)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 332)
assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 330)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 332)
assigns *__fc_stdout \from c, *__fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 331)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 333)
assigns \result \from (indirect: *__fc_stdout);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1601,14 +1605,14 @@
--- Properties of Function 'puts'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 337)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 339)
assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 337)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 339)
assigns *__fc_stdout
\from *(s + (0 .. strlen{Old}(s))), *__fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 338)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 340)
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))),
(indirect: *__fc_stdout);
@@ -1625,13 +1629,13 @@
ensures
result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 344)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 346)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 344)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 346)
assigns *stream \from (indirect: c);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 345)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 347)
assigns \result \from (indirect: c), (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1651,19 +1655,19 @@
\initialized((char *)\old(ptr) +
(0 .. \result * \old(size) - 1))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 353)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 355)
assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream,
\result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 353)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 355)
assigns *((char *)ptr + (0 .. nmemb * size - 1))
\from (indirect: size), (indirect: nmemb), (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 353)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 355)
assigns *stream
\from (indirect: size), (indirect: nmemb), (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 355)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 357)
assigns \result \from size, (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1677,14 +1681,14 @@
[ Extern ] Post-condition 'size_written'
ensures size_written: \result ≤ \old(nmemb)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 366)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 368)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 366)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 368)
assigns *stream
\from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 366)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 368)
assigns \result
\from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
Unverifiable but considered Valid.
@@ -1699,13 +1703,13 @@
[ Extern ] Post-condition 'initialization,pos'
ensures initialization: pos: \initialized(\old(pos))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 377)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 379)
assigns \result, *pos;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 377)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 379)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 377)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 379)
assigns *pos \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1721,19 +1725,19 @@
errno_set:
__fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6}
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 386)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 388)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 386)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 388)
assigns *stream
\from *stream, (indirect: offset), (indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 387)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 389)
assigns \result
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 387)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 389)
assigns __fc_errno
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
@@ -1751,19 +1755,19 @@
errno_set:
__fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6}
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 397)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 399)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 397)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 399)
assigns *stream
\from *stream, (indirect: offset), (indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 398)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 400)
assigns \result
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 398)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 400)
assigns __fc_errno
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
@@ -1780,16 +1784,16 @@
ensures
errno_set: __fc_errno ∈ {11, 9, 27, 4, 5, 28, 32, 29, 6}
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 409)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 411)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 409)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 411)
assigns *stream \from *pos;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 410)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 412)
assigns \result \from (indirect: *stream), (indirect: *pos);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 411)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 413)
assigns __fc_errno
\from __fc_errno, (indirect: *stream), (indirect: *pos);
Unverifiable but considered Valid.
@@ -1810,13 +1814,13 @@
[ Extern ] Post-condition 'errno_set'
ensures errno_set: __fc_errno ∈ {9, 75, 29}
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 419)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 421)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 419)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 421)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 419)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 421)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1836,13 +1840,13 @@
[ Extern ] Post-condition 'errno_set'
ensures errno_set: __fc_errno ∈ {9, 75, 29}
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 428)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 430)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 428)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 430)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 428)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 430)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1853,10 +1857,10 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 437)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 439)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 437)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 439)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1867,10 +1871,10 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 443)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 445)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 443)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 445)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1884,7 +1888,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 449)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 451)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1898,7 +1902,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 455)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 457)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1909,10 +1913,10 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 461)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 463)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 461)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 463)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1923,10 +1927,10 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 467)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 469)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 467)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 469)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1937,13 +1941,13 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 473)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 475)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 473)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 475)
assigns \result \from \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 473)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 475)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1957,7 +1961,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 479)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 481)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1968,10 +1972,10 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 485)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 487)
assigns __fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 485)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 487)
assigns __fc_stdout
\from __fc_errno, *(s + (0 .. strlen{Old}(s)));
Unverifiable but considered Valid.
@@ -1983,13 +1987,13 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 491)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 493)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 491)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 493)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 491)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 493)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2003,7 +2007,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 496)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 498)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2014,13 +2018,13 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 502)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 504)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 502)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 504)
assigns *stream \from c;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 503)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 505)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2031,13 +2035,13 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 508)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 510)
assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 508)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 510)
assigns *__fc_stdout \from c;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 509)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 511)
assigns \result \from (indirect: *__fc_stdout);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2048,10 +2052,10 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 515)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 517)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 515)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 517)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2065,7 +2069,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 521)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 523)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2079,7 +2083,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 527)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 529)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2093,7 +2097,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 533)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 535)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2111,14 +2115,14 @@
(\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
is_open_pipe(\result))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 560)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 562)
assigns \result, __fc_fopen[0 ..];
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 560)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 562)
assigns \result
\from (indirect: *command), (indirect: *type), __fc_p_fopen;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 562)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 564)
assigns __fc_fopen[0 ..]
\from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
Unverifiable but considered Valid.
@@ -2136,7 +2140,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 574)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 576)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2157,15 +2161,15 @@
errno_set:
__fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ∈ {22, 24, 12}
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 590)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 592)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 590)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 592)
assigns __fc_errno
\from (indirect: buf), (indirect: size),
(indirect: *(mode + (0 .. strlen{Old}(mode))));
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 592)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 594)
assigns \result
\from __fc_p_fopen, (indirect: buf), (indirect: size),
(indirect: *(mode + (0 .. strlen{Old}(mode))));
@@ -2173,7 +2177,7 @@
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file FRAMAC_SHARE/libc/stdio.h, line 599)
+[ Extern ] Frees/Allocates nothing/(file FRAMAC_SHARE/libc/stdio.h, line 601)
allocates \old(buf);
Unverifiable but considered Valid.
@@ -2185,25 +2189,25 @@
ensures
result_error_or_written_byes: \result ≡ -1 ∨ \result ≥ 0
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 611)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 613)
assigns __fc_heap_status, \result, *strp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 611)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 613)
assigns __fc_heap_status
\from (indirect: *(fmt + (0 ..))), __fc_heap_status;
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 612)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 614)
assigns \result
\from (indirect: *(fmt + (0 ..))), (indirect: __fc_heap_status);
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 613)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 615)
assigns *strp
\from *(fmt + (0 ..)), (indirect: __fc_heap_status);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file FRAMAC_SHARE/libc/stdio.h, line 616)
+[ Extern ] Frees/Allocates nothing/(file FRAMAC_SHARE/libc/stdio.h, line 618)
allocates *\old(strp);
Unverifiable but considered Valid.
@@ -4256,7 +4260,7 @@
--------------------------------------------------------------------------------
194 Completely validated
16 Locally validated
- 569 Considered valid
+ 570 Considered valid
56 To be validated
- 835 Total
+ 836 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 57ab4d44afc..9ef75177e38 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5115,7 +5115,10 @@ extern struct tm *localtime(time_t const *timer);
/*@ requires dst_has_room: \valid(s + (0 .. max - 1));
requires valid_format: valid_read_string(format);
requires valid_tm: \valid_read(tm);
- ensures result_bounded: \result ≤ \old(max);
+ ensures result_bounded: \result < \old(max);
+ ensures result_valid_string: valid_string(\old(s));
+ ensures result_length: *(\old(s) + \result) ≡ 0;
+ ensures max: *(\old(s) + (\old(max) - 1)) ≡ 0;
assigns *(s + (0 .. max - 1)), \result;
assigns *(s + (0 .. max - 1))
\from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
@@ -6172,8 +6175,10 @@ extern int setvbuf(FILE * restrict stream, char * restrict buf, int mode,
}
*/
-/*@ assigns *stream;
- assigns *stream \from *(format + (..)), arg; */
+/*@ assigns *stream, \result;
+ assigns *stream \from *(format + (..)), (indirect: arg);
+ assigns \result \from (indirect: *(format + (..))), (indirect: arg);
+ */
extern int vfprintf(FILE * restrict stream, char const * restrict format,
va_list arg);
@@ -9233,6 +9238,567 @@ int __builtin_popcountl(unsigned long x);
*/
int __builtin_popcountll(unsigned long long x);
+/*@ requires validity: \valid_read(mem);
+ ensures load_value: \result ≡ *\old(mem);
+ assigns \result;
+ assigns \result \from *mem, (indirect: model);
+ */
+unsigned char __atomic_load_1(unsigned char const *mem, int model);
+
+/*@ requires validity: \valid_read(mem);
+ ensures load_value: \result ≡ *\old(mem);
+ assigns \result;
+ assigns \result \from *mem, (indirect: model);
+ */
+unsigned short __atomic_load_2(unsigned short const *mem, int model);
+
+/*@ requires validity: \valid_read(mem);
+ ensures load_value: \result ≡ *\old(mem);
+ assigns \result;
+ assigns \result \from *mem, (indirect: model);
+ */
+unsigned int __atomic_load_4(unsigned int const *mem, int model);
+
+/*@ requires validity: \valid_read(mem);
+ ensures load_value: \result ≡ *\old(mem);
+ assigns \result;
+ assigns \result \from *mem, (indirect: model);
+ */
+unsigned long long __atomic_load_8(unsigned long long const *mem, int model);
+
+/*@ requires validity: \valid(mem);
+ ensures store_value: *\old(mem) ≡ \old(val);
+ assigns *mem;
+ assigns *mem \from val, (indirect: model);
+ */
+void __atomic_store_1(unsigned char *mem, unsigned char val, int model);
+
+/*@ requires validity: \valid(mem);
+ ensures store_value: *\old(mem) ≡ \old(val);
+ assigns *mem;
+ assigns *mem \from val, (indirect: model);
+ */
+void __atomic_store_2(unsigned short *mem, unsigned short val, int model);
+
+/*@ requires validity: \valid(mem);
+ ensures store_value: *\old(mem) ≡ \old(val);
+ assigns *mem;
+ assigns *mem \from val, (indirect: model);
+ */
+void __atomic_store_4(unsigned int *mem, unsigned int val, int model);
+
+/*@ requires validity: \valid(mem);
+ ensures store_value: *\old(mem) ≡ \old(val);
+ assigns *mem;
+ assigns *mem \from val, (indirect: model);
+ */
+void __atomic_store_8(unsigned long long *mem, unsigned long long val,
+ int model);
+
+/*@ requires validity: \valid(mem);
+ assigns *mem, \result;
+ assigns *mem \from val, (indirect: model);
+ assigns \result \from *mem, (indirect: model);
+ */
+unsigned char __atomic_exchange_1(unsigned char *mem, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(mem);
+ assigns *mem, \result;
+ assigns *mem \from val, (indirect: model);
+ assigns \result \from *mem, (indirect: model);
+ */
+unsigned short __atomic_exchange_2(unsigned short *mem, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(mem);
+ assigns *mem, \result;
+ assigns *mem \from val, (indirect: model);
+ assigns \result \from *mem, (indirect: model);
+ */
+unsigned int __atomic_exchange_4(unsigned int *mem, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(mem);
+ assigns *mem, \result;
+ assigns *mem \from val, (indirect: model);
+ assigns \result \from *mem, (indirect: model);
+ */
+unsigned long long __atomic_exchange_8(unsigned long long *mem,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(mem) ∧ \valid_read(expected);
+ assigns *mem, *expected, \result;
+ assigns *mem
+ \from *mem, (indirect: *expected), desired, (indirect: success_model),
+ (indirect: weak);
+ assigns *expected
+ \from *expected, (indirect: *mem), desired, (indirect: failure_model),
+ (indirect: weak);
+ assigns \result \from (indirect: *mem), (indirect: *expected);
+ */
+_Bool __atomic_compare_exchange_1(unsigned char *mem,
+ unsigned char *expected,
+ unsigned char desired, _Bool weak,
+ int success_model, int failure_model);
+
+/*@ requires validity: \valid(mem) ∧ \valid_read(expected);
+ assigns *mem, *expected, \result;
+ assigns *mem
+ \from *mem, (indirect: *expected), desired, (indirect: success_model),
+ (indirect: weak);
+ assigns *expected
+ \from *expected, (indirect: *mem), desired, (indirect: failure_model),
+ (indirect: weak);
+ assigns \result \from (indirect: *mem), (indirect: *expected);
+ */
+_Bool __atomic_compare_exchange_2(unsigned short *mem,
+ unsigned short *expected,
+ unsigned short desired, _Bool weak,
+ int success_model, int failure_model);
+
+/*@ requires validity: \valid(mem) ∧ \valid_read(expected);
+ assigns *mem, *expected, \result;
+ assigns *mem
+ \from *mem, (indirect: *expected), desired, (indirect: success_model),
+ (indirect: weak);
+ assigns *expected
+ \from *expected, (indirect: *mem), desired, (indirect: failure_model),
+ (indirect: weak);
+ assigns \result \from (indirect: *mem), (indirect: *expected);
+ */
+_Bool __atomic_compare_exchange_4(unsigned int *mem, unsigned int *expected,
+ unsigned int desired, _Bool weak,
+ int success_model, int failure_model);
+
+/*@ requires validity: \valid(mem) ∧ \valid_read(expected);
+ assigns *mem, *expected, \result;
+ assigns *mem
+ \from *mem, (indirect: *expected), desired, (indirect: success_model),
+ (indirect: weak);
+ assigns *expected
+ \from *expected, (indirect: *mem), desired, (indirect: failure_model),
+ (indirect: weak);
+ assigns \result \from (indirect: *mem), (indirect: *expected);
+ */
+_Bool __atomic_compare_exchange_8(unsigned long long *mem,
+ unsigned long long *expected,
+ unsigned long long desired, _Bool weak,
+ int success_model, int failure_model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_add_fetch_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_sub_fetch_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_and_fetch_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_xor_fetch_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_or_fetch_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_nand_fetch_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_add_fetch_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_sub_fetch_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_and_fetch_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_xor_fetch_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_or_fetch_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_nand_fetch_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_add_fetch_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_sub_fetch_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_and_fetch_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_xor_fetch_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_or_fetch_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_nand_fetch_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_add_fetch_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_sub_fetch_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_and_fetch_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_xor_fetch_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_or_fetch_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_nand_fetch_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_fetch_add_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_fetch_sub_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_fetch_and_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_fetch_xor_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_fetch_or_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned char __atomic_fetch_nand_1(unsigned char *ptr, unsigned char val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_fetch_add_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_fetch_sub_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_fetch_and_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_fetch_xor_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_fetch_or_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned short __atomic_fetch_nand_2(unsigned short *ptr, unsigned short val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_fetch_add_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_fetch_sub_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_fetch_and_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_fetch_xor_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_fetch_or_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned int __atomic_fetch_nand_4(unsigned int *ptr, unsigned int val,
+ int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_fetch_add_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_fetch_sub__8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_fetch_and_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_fetch_xor_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_fetch_or_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns \result, *ptr;
+ assigns \result \from *ptr, val, (indirect: model);
+ assigns *ptr \from *ptr, val, (indirect: model);
+ */
+unsigned long long __atomic_fetch_nand_8(unsigned long long *ptr,
+ unsigned long long val, int model);
+
+/*@ requires validity: \valid((char *)ptr);
+ assigns \result, *((char *)ptr);
+ assigns \result \from *((char *)ptr);
+ assigns *((char *)ptr) \from \nothing;
+ */
+_Bool __atomic_test_and_set(void *ptr, int model);
+
+/*@ requires validity: \valid(ptr);
+ assigns *ptr;
+ assigns *ptr \from \nothing;
+ */
+void __atomic_clear(_Bool *ptr, int model);
+
+/*@ assigns \nothing; */
+void __atomic_thread_fence(int model);
+
+/*@ assigns \nothing; */
+void __atomic_signal_fence(int model);
+
+/*@ assigns \result;
+ assigns \result \from (indirect: size), (indirect: ptr);
+ */
+_Bool __atomic_always_lock_free(unsigned int size, void *ptr);
+
+/*@ assigns \result;
+ assigns \result \from (indirect: size), (indirect: ptr);
+ */
+_Bool __atomic_lock_free(unsigned int size, void *ptr);
+
/*@ assigns \nothing; */
void __sync_synchronize(void);
diff --git a/tests/libc/oracle/time_misc.res.oracle b/tests/libc/oracle/time_misc.res.oracle
index 67b9867047a..eae28b5cce8 100644
--- a/tests/libc/oracle/time_misc.res.oracle
+++ b/tests/libc/oracle/time_misc.res.oracle
@@ -66,7 +66,7 @@
outstr[0..199] ∈ [--..--] or UNINITIALIZED
t ∈ [--..--]
tmp ∈ {{ NULL ; &__fc_time_tm }}
- res ∈ [0..200] or UNINITIALIZED
+ res ∈ [0..199] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_ctime[0..25] ∈ [--..--]
__fc_time_tm ∈ [--..--]
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 3385aba34d1..f9740ed485b 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -326,6 +326,8 @@
Unverifiable but considered Valid.
[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 220)
Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 221)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -333,9 +335,9 @@
--- Properties of Function 'vfscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 225)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 227)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 225)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 227)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -344,9 +346,9 @@
--- Properties of Function 'vprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 231)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 233)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 231)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 233)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -355,9 +357,9 @@
--- Properties of Function 'vscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 235)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 237)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 235)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 237)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -366,9 +368,9 @@
--- Properties of Function 'vsnprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 240)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 242)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 240)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 242)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -377,9 +379,9 @@
--- Properties of Function 'vsprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 246)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 248)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 246)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 248)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -390,11 +392,11 @@
[ Extern ] Post-condition 'result_uchar_or_eof'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 259)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 261)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 259)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 261)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 260)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 262)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -409,11 +411,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'terminated_string_on_success'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 268)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 270)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 268)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 270)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 269)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 271)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -422,11 +424,11 @@
--- Properties of Function 'fputc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 282)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 284)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 282)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 284)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 283)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 285)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -435,11 +437,11 @@
--- Properties of Function 'fputs'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 289)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 291)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 289)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 291)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 290)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 292)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -448,11 +450,11 @@
--- Properties of Function 'getc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 297)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 299)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 297)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 299)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 297)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 299)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -461,11 +463,11 @@
--- Properties of Function 'getchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 302)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 304)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 302)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 304)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 302)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 304)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -476,13 +478,13 @@
[ Extern ] Post-condition 'result_null_or_same'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 315)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 317)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 315)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 317)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 316)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 318)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 317)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 319)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -491,11 +493,11 @@
--- Properties of Function 'putc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 324)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 326)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 324)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 326)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 325)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 327)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -504,11 +506,11 @@
--- Properties of Function 'putchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 330)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 332)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 330)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 332)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 331)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 333)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -517,11 +519,11 @@
--- Properties of Function 'puts'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 337)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 339)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 337)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 339)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 338)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 340)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -532,11 +534,11 @@
[ Extern ] Post-condition 'result_ok_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 344)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 346)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 344)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 346)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 345)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 347)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -549,14 +551,14 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'initialization'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 353)
- Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 353)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 355)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 353)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 355)
Unverifiable but considered Valid.
[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 355)
Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 357)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -566,11 +568,11 @@
[ Extern ] Post-condition 'size_written'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 366)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 368)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 366)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 368)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 366)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 368)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -581,11 +583,11 @@
[ Extern ] Post-condition 'initialization,pos'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 377)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 379)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 377)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 379)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 377)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 379)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -596,13 +598,13 @@
[ Extern ] Post-condition 'errno_set'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 386)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 388)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 386)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 388)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 387)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 389)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 387)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 389)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -613,13 +615,13 @@
[ Extern ] Post-condition 'errno_set'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 397)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 399)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 397)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 399)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 398)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 400)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 398)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 400)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -630,13 +632,13 @@
[ Extern ] Post-condition 'errno_set'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 409)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 411)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 409)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 411)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 410)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 412)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 411)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 413)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -649,11 +651,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'errno_set'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 419)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 421)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 419)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 421)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 419)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 421)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -666,11 +668,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'errno_set'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 428)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 430)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 428)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 430)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 428)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 430)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -679,9 +681,9 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 437)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 439)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 437)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 439)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -690,9 +692,9 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 443)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 445)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 443)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 445)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -703,7 +705,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 449)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 451)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -714,7 +716,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 455)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 457)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -723,9 +725,9 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 461)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 463)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 461)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 463)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -734,9 +736,9 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 467)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 469)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 467)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 469)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -745,11 +747,11 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 473)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 475)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 473)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 475)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 473)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 475)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -760,7 +762,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 479)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 481)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -769,9 +771,9 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 485)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 487)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 485)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 487)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -780,11 +782,11 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 491)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 493)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 491)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 493)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 491)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 493)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -795,7 +797,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 496)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 498)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -804,11 +806,11 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 502)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 504)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 502)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 504)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 503)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 505)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -817,11 +819,11 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 508)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 510)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 508)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 510)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 509)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 511)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -830,9 +832,9 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 515)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 517)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 515)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 517)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -843,7 +845,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 521)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 523)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -854,7 +856,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 527)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 529)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -865,7 +867,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 533)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 535)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -876,12 +878,12 @@
[ Extern ] Post-condition 'result_error_or_valid_open_pipe'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 560)
- Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 560)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 562)
Unverifiable but considered Valid.
[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 562)
Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 564)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -893,7 +895,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 574)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 576)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -906,15 +908,15 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'errno_set'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 590)
- Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 590)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 592)
Unverifiable but considered Valid.
[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 592)
Unverifiable but considered Valid.
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 594)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file FRAMAC_SHARE/libc/stdio.h, line 599)
+[ Extern ] Frees/Allocates nothing/(file FRAMAC_SHARE/libc/stdio.h, line 601)
Unverifiable but considered Valid.
--------------------------------------------------------------------------------
@@ -923,17 +925,17 @@
[ Extern ] Post-condition 'result_error_or_written_byes'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 611)
+[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 613)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 611)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 613)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 612)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 614)
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 613)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 615)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file FRAMAC_SHARE/libc/stdio.h, line 616)
+[ Extern ] Frees/Allocates nothing/(file FRAMAC_SHARE/libc/stdio.h, line 618)
Unverifiable but considered Valid.
--------------------------------------------------------------------------------
@@ -951,7 +953,7 @@
--- Status Report Summary
--------------------------------------------------------------------------------
77 Completely validated
- 227 Considered valid
+ 228 Considered valid
1 To be validated
- 305 Total
+ 306 Total
--------------------------------------------------------------------------------
--
GitLab