diff --git a/share/libc/__fc_gcc_builtins.h b/share/libc/__fc_gcc_builtins.h
index 6de0859076e9a5872c97fa40170976037446ec74..bf47a4f812296434ab94b067ad460cd3b7e99f7f 100644
--- a/share/libc/__fc_gcc_builtins.h
+++ b/share/libc/__fc_gcc_builtins.h
@@ -25,8 +25,8 @@
#ifndef __FC_GCC_BUILTINS
#define __FC_GCC_BUILTINS
-#include "features.h"
#include "__fc_machdep.h"
+#include "features.h"
__PUSH_FC_STDLIB
@@ -39,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);
@@ -48,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);
@@ -57,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);
@@ -66,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);
@@ -75,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);
@@ -84,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);
@@ -93,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);
@@ -102,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);
@@ -111,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);
@@ -120,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);
@@ -129,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);
@@ -138,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);
@@ -147,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);
@@ -156,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);
@@ -165,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);
@@ -174,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);
@@ -183,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);
@@ -192,67 +192,543 @@ _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
+// NB: __atomic_* operations do not seem to make a distinction between
+// signed and unsigned: this may lead to some warnings by Frama-C
+
+/*@
+ requires validity: \valid_read(mem);
+ requires initialization: \initialized(mem);
+ assigns \result \from *mem, indirect:model;
+ ensures load_value: \result == *mem;
+*/
+__UINT8_T __atomic_load_1(const __UINT8_T* mem, int model);
+
+/*@
+ requires validity: \valid_read(mem);
+ requires initialization: \initialized(mem);
+ assigns \result \from *mem, indirect: model;
+ ensures load_value: \result == *mem;
+*/
+__UINT16_T __atomic_load_2(const __UINT16_T* mem, int model);
+
+/*@
+ requires validity: \valid_read(mem);
+ requires initialization: \initialized(mem);
+ assigns \result \from *mem, indirect:model;
+ ensures load_value: \result == *mem;
+*/
+__UINT32_T __atomic_load_4(const __UINT32_T* mem, int model);
+
+/*@
+ requires validity: \valid_read(mem);
+ requires initialization: \initialized(mem);
+ assigns \result \from *mem, indirect:model;
+ ensures load_value: \result == *mem;
+*/
+__UINT64_T __atomic_load_8(const __UINT64_T* mem, int model);
+
+/*@
+ requires validity: \valid(mem);
+ assigns *mem \from val, indirect: model;
+ ensures initialization: \initialized(mem);
+ ensures store_value: *mem == val;
+*/
+void __atomic_store_1(__UINT8_T* mem, __UINT8_T val, int model);
+
+/*@
+ requires validity: \valid(mem);
+ assigns *mem \from val, indirect: model;
+ ensures initialization: \initialized(mem);
+ ensures store_value: *mem == val;
+*/
+void __atomic_store_2(__UINT16_T* mem, __UINT16_T val, int model);
+
+/*@
+ requires validity: \valid(mem);
+ assigns *mem \from val, indirect: model;
+ ensures initialization: \initialized(mem);
+ ensures store_value: *mem == val;
+*/
+void __atomic_store_4(__UINT32_T* mem, __UINT32_T val, int model);
+
+/*@
+ requires validity: \valid(mem);
+ assigns *mem \from val, indirect: model;
+ ensures initialization: \initialized(mem);
+ ensures store_value: *mem == val;
+*/
+void __atomic_store_8(__UINT64_T* mem, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(mem);
+ requires initialization: \initialized(mem);
+ assigns *mem \from val, indirect:model;
+ assigns \result \from *mem, indirect:model;
+ */
+__UINT8_T __atomic_exchange_1(__UINT8_T* mem, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(mem);
+ requires initialization: \initialized(mem);
+ assigns *mem \from val, indirect:model;
+ assigns \result \from *mem, indirect:model;
+ */
+__UINT16_T __atomic_exchange_2(__UINT16_T* mem, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(mem);
+ requires initialization: \initialized(mem);
+ assigns *mem \from val, indirect:model;
+ assigns \result \from *mem, indirect:model;
+ */
+__UINT32_T __atomic_exchange_4(__UINT32_T* mem, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(mem);
+ requires initialization: \initialized(mem);
+ assigns *mem \from val, indirect:model;
+ assigns \result \from *mem, indirect:model;
+ */
+__UINT64_T __atomic_exchange_8(__UINT64_T* mem, __UINT64_T val, int model);
+
+/*@
+ requires validity: \valid(mem) && \valid(expected);
+ requires initialization:mem: \initialized(mem);
+ requires initialization:expected: \initialized(expected);
+ assigns *mem \from *mem, desired, indirect: *expected,
+ indirect: success_model, indirect: weak;
+ assigns *expected \from *expected, *mem, indirect: desired,
+ 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);
+
+/*@
+ requires validity: \valid(mem) && \valid(expected);
+ requires initialization:mem: \initialized(mem);
+ requires initialization:expected: \initialized(expected);
+ assigns *mem \from *mem, desired, indirect: *expected,
+ indirect: success_model, indirect: weak;
+ assigns *expected \from *expected, *mem, indirect: desired,
+ 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);
+
+/*@
+ requires validity: \valid(mem) && \valid(expected);
+ requires initialization:mem: \initialized(mem);
+ requires initialization:expected: \initialized(expected);
+ assigns *mem \from *mem, desired, indirect: *expected,
+ indirect: success_model, indirect: weak;
+ assigns *expected \from *expected, *mem, indirect: desired,
+ 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);
+
+/*@
+ requires validity: \valid(mem) && \valid(expected);
+ requires initialization:mem: \initialized(mem);
+ requires initialization:expected: \initialized(expected);
+ assigns *mem \from *mem, desired, indirect: *expected,
+ indirect: success_model, indirect: weak;
+ assigns *expected \from *expected, *mem, indirect: desired,
+ 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);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_add_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_sub_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_and_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_xor_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_or_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_nand_fetch_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_add_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_sub_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_and_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_xor_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_or_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_nand_fetch_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_add_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_sub_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_and_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_xor_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_or_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_nand_fetch_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_add_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_sub_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_and_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_xor_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_or_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_nand_fetch_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_fetch_add_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_fetch_sub_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_fetch_and_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_fetch_xor_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_fetch_or_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT8_T __atomic_fetch_nand_1(__UINT8_T* ptr, __UINT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_fetch_add_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_fetch_sub_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_fetch_and_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_fetch_xor_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_fetch_or_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT16_T __atomic_fetch_nand_2(__UINT16_T* ptr, __UINT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_fetch_add_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_fetch_sub_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_fetch_and_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_fetch_xor_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_fetch_or_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT32_T __atomic_fetch_nand_4(__UINT32_T* ptr, __UINT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_fetch_add_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_fetch_sub__8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_fetch_and_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_fetch_xor_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_fetch_or_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+ requires initialization: \initialized(ptr);
+ assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__UINT64_T __atomic_fetch_nand_8(__UINT64_T* ptr, __UINT64_T val, int model);
+
+/*@ requires validity: \valid((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 \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 \from indirect: size, indirect: ptr; */
+_Bool __atomic_always_lock_free(__SIZE_T size, void* ptr);
+
+/*@ assigns \result \from indirect: size, indirect: ptr; */
+_Bool __atomic_is_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/share/libc/stdio.h b/share/libc/stdio.h
index 0b38e916296180787c2b51d7d57bf3555475df2a..eb9282338d5d02a068833c6b89765bf6cac52ff3 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -217,7 +217,9 @@ extern int sprintf(char * restrict s,
extern int sscanf(const char * restrict s,
const char * restrict format, ...);
-/*@ assigns *stream \from format[..], arg; */
+/*@ assigns *stream \from format[..], indirect: arg;
+ assigns \result \from indirect:format[..], indirect:arg;
+*/
extern int vfprintf(FILE * restrict stream,
const char * restrict format,
va_list arg);
diff --git a/share/libc/time.h b/share/libc/time.h
index 217669b778a757c79d5c5e2c1a407a8111bfb8e3..a0958995d762046f0bbb91844369da0b190750b9 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -158,7 +158,9 @@ extern struct tm *localtime(const time_t *timer);
requires valid_tm: \valid_read(tm);
assigns s[0 .. max-1] \from indirect:max, indirect:format[0..], indirect:*tm;
assigns \result \from indirect:max, indirect:format[0..], indirect:*tm;
- ensures result_bounded: \result <= max;
+ ensures result_bounded: \result < max;
+ ensures result_valid_string: \result > 0 ==> valid_string(s);
+ ensures result_length: \result > 0 ==> s[\result] == 0;
*/
extern size_t strftime(char * restrict s,
size_t max,
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b673e39e428a92ac009e9444945c57a289235c6e..f483a6695bbc582f8bf4d4fa5f2b1a74d0d009e4 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6722,6 +6722,43 @@ and doExp local_env
"Too few arguments for builtin %s" n;
n
end
+
+ (* contrarily to the other builtins, __atomic_load and
+ __atomic_exchange generic versions do not share the same
+ signature as their specialized counterparts.
+ Hence, we'd have to change the args list as well.
+ *)
+ | "__atomic_load" | "__atomic_exchange" ->
+ Kernel.error ~once:true ~current:true
+ "Generic %s is not yet supported" n;
+ n
+ (* for store and compare_exchange, the generic version is also
+ able to handle types of arbitrary size, via an external
+ function that takes the size of the type as argument as well.
+ Here too, we'd need to change the args list to support that.
+ *)
+ | "__atomic_store" | "__atomic_compare_exchange"
+ | "__atomic_add_fetch"
+ | "__atomic_sub_fetch" | "__atomic_and_fetch"
+ | "__atomic_xor_fetch" | "__atomic_or_fetch"
+ | "__atomic_nand_fetch" | "__atomic_fetch_add"
+ | "__atomic_fetch_sub" | "__atomic_fetch_and"
+ | "__atomic_fetch_xor" | "__atomic_fetch_or"
+ | "__atomic_fetch_nand" ->
+ begin
+ match args with
+ | a1 :: _ ->
+ let _,c,_,t =
+ doExp (no_paren_local_env local_env) CNoConst a1 AType
+ in
+ clean_up_chunk_locals c;
+ let t = typeOf_pointed t in
+ Format.sprintf "%s_%d" n (bytesSizeOf t)
+ | [] ->
+ Kernel.error ~once:true ~current:true
+ "Too few arguments for builtin %s" n;
+ n
+ end
| _ -> n
in
let vi, _ = lookupVar ghost n in
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 ff974a15990493fc1ff382718a01ec6baa6ba8f1..3929c369e311404b5864331f7b2cd16d1fa41f72 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 42cba99e4ca3d95a97530e0abced583e29429625..184cc7c43cb0d75f71518fbf5bb280f1f106c08c 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 1dfe0498bed0112fac1d2f66b88acc3283fc62d6..2c771c66bd1bdcf46f73936f65aea84f732108ff 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 1dfe0498bed0112fac1d2f66b88acc3283fc62d6..2c771c66bd1bdcf46f73936f65aea84f732108ff 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 7b2ac7b3ecfaaee74530b636fd6fe37f6ab863e8..8dca9f2bac2c97a2596b057ccf813cdcda652172 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 7f8b5b42d2cca3a1925dcd51153a2e8dbaf72484..c71892de48014543d30c8555794adacf3a65e450 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 d29a81d76920c34343277a707a916abced463703..709eade7c321855ea7a2963541cef50217e5691a 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 1dbb2458c3ded4562958a33ca52c675718794048..7ee761f24d504c42269186b8ff7fffa29191c376 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 bea7ff5f3c9a6b7d349387951d468a7bdde94cd7..80bb3f1eae266b322096f78f4f179906b72f6833 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 14583255222c01351a04906e414a25235e3cc49d..0769b43d1d763736adff4dc7b500113f45e6e56f 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 71e13f3012fb292ad49009070d7409db1037a452..61261c69b7f3e3af3676c8f2ecadcda889a2b9fa 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 2e9b9b017a577139a5a2b11eba96fa49ee979bcd..3b67607452bdcfe8fa313f2f737c266505abb507 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 15799fe60f4ea379d2ee0a853fa237af3d5204c3..8bc1110db48496516154b355e5757c58286bddd3 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 dd7a3d80783ad909b386a7c1f57a70059f6ebb6a..577e5cfa4edd4d40c5e45b922a44073c5bb0bc97 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 c225e1ea1605c86556bbfd799bf3c74b0e057015..292f987963aa8135de346c2d8673b489d1ecf862 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 4e8e4cf6cbcbe1ba07bfbe7c83d84bf3e4bc27ff..c96e7311094d281800f6f1e454cf8adf89ff2116 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 6b7bc896adcb1f582e52461164a3e7580c5b0282..ed6948688d7bbde2d6b07be63fbc3c1cea3bc45e 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 7b439fc5fa64b23f243297110f974949934438df..02012fe664a97801649e27471cfecfacf25194db 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 4976f7d14946dfc6267dd2bf9e232e6baf329d19..c31c436e505d57cd2728188cdb8bad388f31249d 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 64c5c7034588d61edc26dc55f786fe160552a208..f1a366040cbd837b60f664d8e632a2e5128fd36d 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 6fcda71f59aca61888f5bbc6424bb9b961d628ea..2b84b5e6d38b4bc9695b2eac24820d8a7b12bfde 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/idct/oracle_multidim/ieee_1180_1990.res.oracle b/tests/idct/oracle_multidim/ieee_1180_1990.res.oracle
index d16224c12bc5709aa446612f842ba7beb78ac431..51a1a894ad988e333fa9e44015a7e7498df8a2d8 100644
--- a/tests/idct/oracle_multidim/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle_multidim/ieee_1180_1990.res.oracle
@@ -265,7 +265,7 @@
< "output.\n"[bits 0 to 71]
---
> idct_init; idct_mc1[0..7][0..7]; idct_mc2[0..7][0..7]
-3906,3928d3740
+3910,3932d3744
< [ - ] Assertion 'Eva,initialization' (file idct.c, line 129)
< assert Eva: initialization: \initialized(&tmp1[i][j]);
< tried with Eva.
@@ -289,7 +289,7 @@
< assert Eva: initialization: \initialized(&tmp1[i][j]);
< By RedundantAlarms, with pending:
< - Assertion 'Eva,initialization' (file idct.c, line 145)
-3932,3954d3743
+3936,3958d3747
< [ - ] Assertion 'Eva,initialization' (file idct.c, line 163)
< assert Eva: initialization: \initialized(&tmp1[i][j]);
< tried with Eva.
@@ -313,11 +313,11 @@
< assert Eva: initialization: \initialized(&tmp1[i][j]);
< By RedundantAlarms, with pending:
< - Assertion 'Eva,initialization' (file idct.c, line 180)
-3976,3978d3764
+3980,3982d3768
< [ - ] Assertion 'Eva,initialization' (file ieee_1180_1990.c, line 109)
< assert Eva: initialization: \initialized(&tmp1[i][j]);
< tried with Eva.
-3982,4015d3767
+3986,4019d3771
< [ - ] Assertion 'Eva,initialization' (file ieee_1180_1990.c, line 116)
< assert Eva: initialization: \initialized(&tmp2[i][j]);
< tried with Eva.
@@ -352,11 +352,11 @@
< [ - ] Assertion 'Eva,float_to_int' (file ieee_1180_1990.c, line 124)
< assert Eva: float_to_int: tmp2[i][j] - 0.5 < 2147483648;
< tried with Eva.
-4036,4038d3787
+4040,4042d3791
< [ - ] Assertion 'Eva,initialization' (file ieee_1180_1990.c, line 150)
< assert Eva: initialization: \initialized(&tmp1[i][j]);
< tried with Eva.
-4042,4075d3790
+4046,4079d3794
< [ - ] Assertion 'Eva,initialization' (file ieee_1180_1990.c, line 157)
< assert Eva: initialization: \initialized(&tmp2[i][j]);
< tried with Eva.
@@ -391,7 +391,7 @@
< [ - ] Assertion 'Eva,float_to_int' (file ieee_1180_1990.c, line 165)
< assert Eva: float_to_int: tmp2[i][j] - 0.5 < 2147483648;
< tried with Eva.
-4175,4191c3890,3896
+4179,4195c3894,3900
< [ Partial ] Assertion 'Eva,initialization' (file ieee_1180_1990.c, line 358)
< assert Eva: initialization: \initialized(&res[i].pmse[j][k]);
< By RedundantAlarms, with pending:
@@ -417,7 +417,7 @@
> reachability of stmt line 196 in main
> by Eva.
> [ Dead ] Instance of 'Pre-condition (file FRAMAC_SHARE/libc/stdio.h, line 211)' at call 'printf_va_1' (file ieee_1180_1990.c, line 195)
-4195,4196c3900,3903
+4199,4200c3904,3907
< by Eva.
< [ Valid ] Instance of 'Pre-condition (file FRAMAC_SHARE/libc/stdio.h, line 211)' at call 'printf_va_2' (file ieee_1180_1990.c, line 196)
---
@@ -425,22 +425,22 @@
> By Eva because:
> - Unreachable call 'printf_va_1' (file ieee_1180_1990.c, line 195)
> [ Dead ] Instance of 'Pre-condition (file FRAMAC_SHARE/libc/stdio.h, line 211)' at call 'printf_va_2' (file ieee_1180_1990.c, line 196)
-4200c3907,3909
+4204c3911,3913
< by Eva.
---
> Locally valid, but unreachable.
> By Eva because:
> - Unreachable call 'printf_va_2' (file ieee_1180_1990.c, line 196)
-4257,4258c3966
+4261,4262c3970
< 194 Completely validated
< 16 Locally validated
---
> 192 Completely validated
-4260,4261c3968,3971
+4264,4265c3972,3975
< 56 To be validated
-< 835 Total
+< 836 Total
---
> 32 To be validated
> 2 Dead properties
> 2 Unreachable
-> 797 Total
+> 798 Total
diff --git a/tests/libc/more_gcc_builtins.c b/tests/libc/more_gcc_builtins.c
index 614aae666d6e492da1fd8807c239cfe0b305cff8..875f454c827b26214451be568f65e6e2f9a3204d 100644
--- a/tests/libc/more_gcc_builtins.c
+++ b/tests/libc/more_gcc_builtins.c
@@ -69,5 +69,23 @@ int main() {
//@ assert 0 <= res <= CHAR_BIT * sizeof(long);
res = __builtin_popcountll(ULLONG_MAX);
//@ assert 0 <= res <= CHAR_BIT * sizeof(long long);
+
+ // Atomic builtins
+ __UINT8_T u8_1, u8_2 = 42;
+ u8_1 = __atomic_load_1(&u8_2, __ATOMIC_RELAXED);
+ __UINT16_T u16_1, u16_2 = 4200;
+ __atomic_store(&u16_1, u16_2, __ATOMIC_ACQ_REL);
+ __UINT32_T u32_1, u32_2 = 1234567, u32_3 = 420000;
+ u32_1 = __atomic_exchange_4(&u32_2, u32_3, __ATOMIC_RELEASE);
+ __UINT64_T u64_1 = 12345678901UL, u64_2 = 42000000000UL, u64_3 = 42000000001UL;
+ r = __atomic_compare_exchange(&u64_1, &u64_2, u64_3, 1, __ATOMIC_SEQ_CST, __ATOMIC_ACQUIRE);
+ u8_2 = __atomic_add_fetch(&u8_1, u8_2, __ATOMIC_CONSUME);
+ u16_2 = __atomic_fetch_sub(&u16_1, u16_2, __ATOMIC_RELAXED);
+ u32_2 = __atomic_fetch_xor(&u32_1, u32_2, __ATOMIC_RELAXED);
+ u64_2 = __atomic_fetch_nand(&u64_1, u64_2, __ATOMIC_RELAXED);
+ r = __atomic_test_and_set(&u32_3, __ATOMIC_ACQUIRE);
+ __atomic_clear(&r, __ATOMIC_ACQ_REL);
+ r = __atomic_always_lock_free(sizeof(long long), 0);
+ r = __atomic_is_lock_free(sizeof(long), &u32_1);
return 0;
}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 57ab4d44afcf9a6fc36b3eda8ce4e28836227c5a..45092e46f291f3ead9cfe6dae97543f9ee079c99 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5115,7 +5115,9 @@ 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: \result > 0 ⇒ valid_string(\old(s));
+ ensures result_length: \result > 0 ⇒ *(\old(s) + \result) ≡ 0;
assigns *(s + (0 .. max - 1)), \result;
assigns *(s + (0 .. max - 1))
\from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
@@ -6172,8 +6174,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 +9237,635 @@ int __builtin_popcountl(unsigned long x);
*/
int __builtin_popcountll(unsigned long long x);
+/*@ requires validity: \valid_read(mem);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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 initialization: \initialized(\old(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 initialization: \initialized(\old(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 initialization: \initialized(\old(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 initialization: \initialized(\old(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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(expected);
+ requires initialization: mem: \initialized(mem);
+ requires initialization: expected: \initialized(expected);
+ assigns *mem, *expected, \result;
+ assigns *mem
+ \from *mem, desired, (indirect: *expected), (indirect: success_model),
+ (indirect: weak);
+ assigns *expected
+ \from *expected, *mem, (indirect: 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(expected);
+ requires initialization: mem: \initialized(mem);
+ requires initialization: expected: \initialized(expected);
+ assigns *mem, *expected, \result;
+ assigns *mem
+ \from *mem, desired, (indirect: *expected), (indirect: success_model),
+ (indirect: weak);
+ assigns *expected
+ \from *expected, *mem, (indirect: 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(expected);
+ requires initialization: mem: \initialized(mem);
+ requires initialization: expected: \initialized(expected);
+ assigns *mem, *expected, \result;
+ assigns *mem
+ \from *mem, desired, (indirect: *expected), (indirect: success_model),
+ (indirect: weak);
+ assigns *expected
+ \from *expected, *mem, (indirect: 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(expected);
+ requires initialization: mem: \initialized(mem);
+ requires initialization: expected: \initialized(expected);
+ assigns *mem, *expected, \result;
+ assigns *mem
+ \from *mem, desired, (indirect: *expected), (indirect: success_model),
+ (indirect: weak);
+ assigns *expected
+ \from *expected, *mem, (indirect: 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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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);
+ requires initialization: \initialized(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_is_lock_free(unsigned int size, void *ptr);
+
/*@ assigns \nothing; */
void __sync_synchronize(void);
diff --git a/tests/libc/oracle/more_gcc_builtins.res.oracle b/tests/libc/oracle/more_gcc_builtins.res.oracle
index a8298a52cb48efaa458598edee14089db96eaa99..3ee3de3f18e2a603da693c7ae9e92d277e2936ba 100644
--- a/tests/libc/oracle/more_gcc_builtins.res.oracle
+++ b/tests/libc/oracle/more_gcc_builtins.res.oracle
@@ -149,15 +149,110 @@
[eva] using specification for function __builtin_popcountll
[eva] Done for function __builtin_popcountll
[eva] more_gcc_builtins.c:71: assertion got status valid.
+[eva] computing for function __atomic_load_1 <- main.
+ Called from more_gcc_builtins.c:75.
+[eva] using specification for function __atomic_load_1
+[eva] more_gcc_builtins.c:75:
+ function __atomic_load_1: precondition 'validity' got status valid.
+[eva] more_gcc_builtins.c:75:
+ function __atomic_load_1: precondition 'initialization' got status valid.
+[eva] Done for function __atomic_load_1
+[eva] computing for function __atomic_store_2 <- main.
+ Called from more_gcc_builtins.c:77.
+[eva] using specification for function __atomic_store_2
+[eva] more_gcc_builtins.c:77:
+ function __atomic_store_2: precondition 'validity' got status valid.
+[eva] Done for function __atomic_store_2
+[eva] computing for function __atomic_exchange_4 <- main.
+ Called from more_gcc_builtins.c:79.
+[eva] using specification for function __atomic_exchange_4
+[eva] more_gcc_builtins.c:79:
+ function __atomic_exchange_4: precondition 'validity' got status valid.
+[eva] more_gcc_builtins.c:79:
+ function __atomic_exchange_4: precondition 'initialization' got status valid.
+[eva] Done for function __atomic_exchange_4
+[eva] computing for function __atomic_compare_exchange_8 <- main.
+ Called from more_gcc_builtins.c:81.
+[eva] using specification for function __atomic_compare_exchange_8
+[eva] more_gcc_builtins.c:81:
+ function __atomic_compare_exchange_8: precondition 'validity' got status valid.
+[eva] more_gcc_builtins.c:81:
+ function __atomic_compare_exchange_8: precondition 'initialization,mem' got status valid.
+[eva] more_gcc_builtins.c:81:
+ function __atomic_compare_exchange_8: precondition 'initialization,expected' got status valid.
+[eva] Done for function __atomic_compare_exchange_8
+[eva] computing for function __atomic_add_fetch_1 <- main.
+ Called from more_gcc_builtins.c:82.
+[eva] using specification for function __atomic_add_fetch_1
+[eva] more_gcc_builtins.c:82:
+ function __atomic_add_fetch_1: precondition 'validity' got status valid.
+[eva] more_gcc_builtins.c:82:
+ function __atomic_add_fetch_1: precondition 'initialization' got status valid.
+[eva] Done for function __atomic_add_fetch_1
+[eva] computing for function __atomic_fetch_sub_2 <- main.
+ Called from more_gcc_builtins.c:83.
+[eva] using specification for function __atomic_fetch_sub_2
+[eva] more_gcc_builtins.c:83:
+ function __atomic_fetch_sub_2: precondition 'validity' got status valid.
+[eva] more_gcc_builtins.c:83:
+ function __atomic_fetch_sub_2: precondition 'initialization' got status valid.
+[eva] Done for function __atomic_fetch_sub_2
+[eva] computing for function __atomic_fetch_xor_4 <- main.
+ Called from more_gcc_builtins.c:84.
+[eva] using specification for function __atomic_fetch_xor_4
+[eva] more_gcc_builtins.c:84:
+ function __atomic_fetch_xor_4: precondition 'validity' got status valid.
+[eva] more_gcc_builtins.c:84:
+ function __atomic_fetch_xor_4: precondition 'initialization' got status valid.
+[eva] Done for function __atomic_fetch_xor_4
+[eva] computing for function __atomic_fetch_nand_8 <- main.
+ Called from more_gcc_builtins.c:85.
+[eva] using specification for function __atomic_fetch_nand_8
+[eva] more_gcc_builtins.c:85:
+ function __atomic_fetch_nand_8: precondition 'validity' got status valid.
+[eva] more_gcc_builtins.c:85:
+ function __atomic_fetch_nand_8: precondition 'initialization' got status valid.
+[eva] Done for function __atomic_fetch_nand_8
+[eva] computing for function __atomic_test_and_set <- main.
+ Called from more_gcc_builtins.c:86.
+[eva] using specification for function __atomic_test_and_set
+[eva] more_gcc_builtins.c:86:
+ function __atomic_test_and_set: precondition 'validity' got status valid.
+[eva] Done for function __atomic_test_and_set
+[eva] computing for function __atomic_clear <- main.
+ Called from more_gcc_builtins.c:87.
+[eva] using specification for function __atomic_clear
+[eva] more_gcc_builtins.c:87:
+ function __atomic_clear: precondition 'validity' got status valid.
+[eva] Done for function __atomic_clear
+[eva] computing for function __atomic_always_lock_free <- main.
+ Called from more_gcc_builtins.c:88.
+[eva] using specification for function __atomic_always_lock_free
+[eva] Done for function __atomic_always_lock_free
+[eva] computing for function __atomic_is_lock_free <- main.
+ Called from more_gcc_builtins.c:89.
+[eva] using specification for function __atomic_is_lock_free
+[eva] Done for function __atomic_is_lock_free
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
res ∈ [0..64]
- r ∈ {1}
+ r ∈ [--..--]
lres ∈ {2147483647}
llres ∈ {-9223372036854775808}
ures ∈ {8}
ulres ∈ {8}
ullres ∈ {18446744073709551612}
+ u8_1 ∈ [--..--]
+ u8_2 ∈ [--..--]
+ u16_1 ∈ [--..--]
+ u16_2 ∈ [--..--]
+ u32_1 ∈ [--..--]
+ u32_2 ∈ [--..--]
+ u32_3[bits 0 to 7] ∈ [--..--]
+ [bits 8 to 31]# ∈ {420000}%32, bits 8 to 31
+ u64_1 ∈ [--..--]
+ u64_2 ∈ [--..--]
+ u64_3 ∈ {42000000001}
__retres ∈ {0}
diff --git a/tests/libc/oracle/time_misc.res.oracle b/tests/libc/oracle/time_misc.res.oracle
index 67b9867047a8d8912e89992703b7a7f9ba116a0c..eae28b5cce8847a6a0a62ce8d2933b74bbf99a5d 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 3385aba34d1244c4b5711a2e50ec2ecfc414dc49..f9740ed485b2967d35d36e530e30debbf9ebc48e 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
--------------------------------------------------------------------------------