From 35db023b12724660a6e2209c864459187da4272b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 17 Mar 2023 17:43:32 +0100
Subject: [PATCH] [machdep] fixes various discrepancies and update tests
---
share/libc/limits.h | 4 +-
share/machdeps/machdep-schema.yaml | 6 ++
share/machdeps/machdep_avr_16.yaml | 1 +
share/machdeps/machdep_gcc_x86_16.yaml | 1 +
share/machdeps/machdep_gcc_x86_32.yaml | 1 +
share/machdeps/machdep_gcc_x86_64.yaml | 1 +
share/machdeps/machdep_msvc_x86_64.yaml | 32 +++++++-
share/machdeps/machdep_ppc_32.yaml | 1 +
share/machdeps/machdep_x86_16.yaml | 1 +
share/machdeps/machdep_x86_32.yaml | 1 +
share/machdeps/machdep_x86_64.yaml | 1 +
share/machdeps/make_machdep/make_machdep.py | 1 +
src/kernel_internals/runtime/machdep.ml | 5 +-
src/kernel_services/ast_data/cil_types.ml | 1 +
.../ast_queries/cil_datatype.ml | 1 +
src/kernel_services/ast_queries/file.ml | 1 +
.../tests/sarif/oracle/std_string.sarif | 8 +-
.../tests/erroneous/oracle/exec.res.oracle | 6 +-
.../tests/known/oracle/exec.res.oracle | 6 +-
.../oracle/exec_failed_requirement.res.oracle | 6 +-
.../tests/known/oracle/printf.res.oracle | 6 +-
tests/builtins/oracle/free.res.oracle | 2 +-
.../builtins/oracle/linked_list.0.res.oracle | 72 ++++++++---------
.../builtins/oracle/linked_list.1.res.oracle | 72 ++++++++---------
.../builtins/oracle/linked_list.2.res.oracle | 80 +++++++++----------
.../oracle/malloc-size-zero.0.res.oracle | 2 +-
.../oracle/malloc-size-zero.1.res.oracle | 2 +-
tests/builtins/oracle/realloc.res.oracle | 30 +++----
.../builtins/oracle_gauges/realloc.res.oracle | 24 +++---
tests/idct/oracle/ieee_1180_1990.res.oracle | 13 ++-
.../oracle_multidim/ieee_1180_1990.res.oracle | 22 ++---
tests/libc/oracle/fc_libc.1.res.oracle | 41 +++++-----
tests/libc/oracle/fc_libc.2.res.oracle | 2 -
tests/libc/oracle/libgen_h.res.oracle | 4 +-
tests/libc/oracle/limits_h.0.res.oracle | 2 +-
tests/libc/oracle/limits_h.3.res.oracle | 2 +-
tests/libc/oracle/signal_h.res.oracle | 2 +-
tests/libc/oracle/stdlib_c.0.res.oracle | 16 ++--
tests/libc/oracle/stdlib_c.1.res.oracle | 16 ++--
tests/libc/oracle/stdlib_c.2.res.oracle | 16 ++--
tests/misc/custom_machdep.c | 2 +-
tests/misc/custom_machdep.ml | 3 +-
tests/misc/custom_machdep.yaml | 4 +-
tests/misc/oracle/custom_machdep.0.res.oracle | 2 +-
tests/misc/oracle/custom_machdep.1.res.oracle | 2 +-
tests/misc/oracle/print_machdep.res.oracle | 2 +-
tests/syntax/cpp-command.c | 2 +-
tests/syntax/machdep_char_unsigned.ml | 1 +
tests/syntax/oracle/cpp-command.0.res.oracle | 2 +-
tests/syntax/oracle/cpp-command.1.res.oracle | 2 +-
tests/syntax/oracle/cpp-command.4.res.oracle | 2 +-
tests/syntax/oracle/cpp-command.6.res.oracle | 2 +-
tests/value/oracle_gauges/gauges.res.oracle | 4 +-
53 files changed, 296 insertions(+), 245 deletions(-)
diff --git a/share/libc/limits.h b/share/libc/limits.h
index 161f09ae491..c789c50081b 100644
--- a/share/libc/limits.h
+++ b/share/libc/limits.h
@@ -77,7 +77,6 @@
# define ULLONG_MAX __FC_ULLONG_MAX
// POSIX-specific definitions
-#ifdef __FC_POSIX_VERSION
/*** Most restrictive values for the constants below, as mandated by POSIX */
@@ -200,7 +199,7 @@
"... the total space used to store the environment and the arguments to the
process is limited to {ARG_MAX} bytes."
*/
-#ifdef __FC_ARG_NAME_MAX
+#ifdef __FC_ARG_MAX
# if __FC_ARG_MAX >= 0
_Static_assert(__FC_ARG_MAX >=_POSIX_ARG_MAX, "__FC_ARG_MAX is too small (" expand(__FC_ARG_MAX) "): minimal value is " expand(__POSIX_ARG_MAX));
# define ARG_MAX __FC_ARG_MAX
@@ -224,5 +223,4 @@
# define IOV_MAX 255
#endif
-#endif // __FC_POSIX_VERSION
#endif
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index b4d47f81ac0..2044ecac188 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -96,6 +96,12 @@ cpp_arch_flags:
- type: string
+custom_defs:
+ description: |
+ arbitrary text that will be reproduced verbatim in the generated
+ header
+ type: string
+
eof:
description: value of 'EOF' macro
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index 31f2b2ee060..bbf6aff51fb 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
- -target
- avr
- -m16
+custom_defs: ''
eof: (-1)
errno:
e2big: '7'
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index 49022b0b99b..1e1098967c0 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -13,6 +13,7 @@ char_is_unsigned: false
compiler: gcc
cpp_arch_flags:
- -m16
+custom_defs: ''
errno:
e2big: '7'
eacces: '13'
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index d474ec51725..31a960d7521 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -14,6 +14,7 @@ char_is_unsigned: false
compiler: gcc
cpp_arch_flags:
- -m32
+custom_defs: ''
eof: (-1)
errno:
e2big: '7'
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index 10ba75b7f13..f87a36a2596 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -14,6 +14,7 @@ char_is_unsigned: false
compiler: gcc
cpp_arch_flags:
- -m64
+custom_defs: ''
eof: (-1)
errno:
e2big: '7'
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index fd6b2580120..59f2f5d98f1 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -13,6 +13,36 @@ char_is_unsigned: false
compiler: msvc
cpp_arch_flags:
- -m64
+custom_defs: |
+ #define _MSC_FULL_VER 160040219
+ #define _MSC_VER 1600
+ #undef __ptr64
+ #define __ptr64
+ #undef __ptr32
+ #define __ptr32
+ #undef __unaligned
+ #define __unaligned
+ #undef __cdecl
+ #define __cdecl
+ #undef __possibly_notnullterminated
+ #define __possibly_notnullterminated
+ #ifndef errno_t
+ # define errno_t int
+ # define _ERRNO_T_DEFINED
+ #endif
+ #ifndef _WIN64
+ # define _WIN64 1
+ #endif
+ #ifndef _AMD64_
+ # define _AMD64_ 1
+ #endif
+ #ifndef _M_AMD64
+ # define _M_AMD64 1
+ #endif
+ #ifndef _M_X64
+ # define _M_X64 1
+ #endif
+
errno:
eperm: '1'
enoent: '2'
@@ -133,7 +163,7 @@ posix_version: ''
# taken from gnu
bufsiz: '8192'
eof: '(-1)'
-fopen_max: '16'
+fopen_max: '20'
host_name_max: '255'
path_max: '256'
tty_name_max: '32'
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index a9dfce1010a..3236aa762f2 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
- -target
- powerpc-apple-linux
- -mcpu=603
+custom_defs: ''
eof: (-1)
errno:
e2big: '7'
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index 00cd07f7ebf..119373b9943 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -13,6 +13,7 @@ char_is_unsigned: false
compiler: generic
cpp_arch_flags:
- -m16
+custom_defs: ''
errno:
e2big: '7'
eacces: '13'
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index d06c7f607bb..6cee4a37cb6 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -14,6 +14,7 @@ char_is_unsigned: false
compiler: generic
cpp_arch_flags:
- -m32
+custom_defs: ''
eof: (-1)
errno:
e2big: '7'
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index 049407efe1b..a9d4dfcb7c4 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -14,6 +14,7 @@ char_is_unsigned: false
compiler: generic
cpp_arch_flags:
- -m64
+custom_defs: ''
eof: (-1)
errno:
e2big: '7'
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index 9f8dd0b3f7b..ff6315492d8 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -328,6 +328,7 @@ version = version_output.stdout.splitlines()[0]
machdep["compiler"] = args.compiler
machdep["cpp_arch_flags"] = args.cpp_arch_flags
machdep["version"] = version
+machdep["custom_defs"] = ""
if args.from_file and args.in_place:
machdep["machdep_name"] = Path(args.from_file).stem
elif args.dest_file:
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 8b6a81c693d..a4cf0ee7240 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -76,7 +76,8 @@ let max_val bitsize is_signed kind =
v ^ suff
let min_val bitsize kind =
- "-" ^ (max_val bitsize true kind) ^ " - 1"
+ let suff = List.assoc kind suff_of_kind in
+ "(-" ^ (max_val bitsize true kind) ^ " - 1" ^ suff ^")"
let gen_define_stype fmt name kind =
gen_define_string fmt ("__INT" ^ name ^ "_T") ("signed " ^ kind)
@@ -282,6 +283,8 @@ let gen_all_defines fmt mach =
if mach.compiler = "gcc" then
gen_include fmt "__fc_gcc_builtins.h";
+ Format.fprintf fmt "%s@\n" mach.custom_defs;
+
Format.fprintf fmt "#endif // __FC_MACHDEP@\n"
let generate_machdep_header mach =
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index e1c9e7270e8..8366c9e4968 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1928,6 +1928,7 @@ type mach = {
nsig: string; (* expansion of non-standard NSIG macro, empty if undefined *)
errno: (string * string) list; (* list of macros defining errors in errno.h*)
machdep_name: string; (* name of the machdep *)
+ custom_defs: string; (* arbitrary text to be written in the header *)
}
(*
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 35810382a30..ffd2febd6b3 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2694,6 +2694,7 @@ let dummy_machdep =
"erange", "34";
];
machdep_name = "dummy";
+ custom_defs = "";
}
module Machdep = Datatype.Make_with_collections(struct
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index e9d681ce0af..183e475c5df 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -408,6 +408,7 @@ type mach = Cil_types.mach = {
nsig: string;
errno: (string * string) list [@of_yaml yaml_dict_to_list];
machdep_name: string;
+ custom_defs: string;
}
[@@deriving yaml]
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 8df66b349d8..1e15a794fc4 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -7278,8 +7278,8 @@
"startLine": 613,
"startColumn": 30,
"endLine": 613,
- "endColumn": 61,
- "byteLength": 31
+ "endColumn": 62,
+ "byteLength": 32
}
}
}
@@ -7746,8 +7746,8 @@
"startLine": 627,
"startColumn": 30,
"endLine": 627,
- "endColumn": 63,
- "byteLength": 33
+ "endColumn": 64,
+ "byteLength": 34
}
}
}
diff --git a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
index 085bd49daed..c490429033d 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:800:
+[variadic] FRAMAC_SHARE/libc/unistd.h:807:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:805:
+[variadic] FRAMAC_SHARE/libc/unistd.h:812:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:810:
+[variadic] FRAMAC_SHARE/libc/unistd.h:817:
Declaration of variadic function execlp.
[variadic:typing] exec.c:5: Warning:
Incorrect type for argument 3. The argument will be cast from int to char *.
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index d8d3c2140b9..f0bfef85da9 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:800:
+[variadic] FRAMAC_SHARE/libc/unistd.h:807:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:805:
+[variadic] FRAMAC_SHARE/libc/unistd.h:812:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:810:
+[variadic] FRAMAC_SHARE/libc/unistd.h:817:
Declaration of variadic function execlp.
[variadic] exec.c:9: Translating call to execle to a call to execve.
[variadic:typing] exec.c:11: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle b/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
index 1304870fba5..3d9efbe7988 100644
--- a/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
@@ -1,8 +1,8 @@
-[variadic] FRAMAC_SHARE/libc/unistd.h:800:
+[variadic] FRAMAC_SHARE/libc/unistd.h:807:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:805:
+[variadic] FRAMAC_SHARE/libc/unistd.h:812:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:810:
+[variadic] FRAMAC_SHARE/libc/unistd.h:817:
Declaration of variadic function execlp.
[variadic] exec_failed_requirement.c:7:
Translating call to execl to a call to execv.
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 00c76b71477..91a4df4a5fa 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -509,7 +509,7 @@ int printf_va_21(char const * restrict format, unsigned long param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_22(char const * restrict format, int param0);
+int printf_va_22(char const * restrict format, long param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -631,7 +631,7 @@ int main(void)
uint64_t u64 = 42ul;
int8_t i8 = (int8_t)42;
uint_least64_t uleast64 = (uint_least64_t)42u;
- int_fast32_t ifast32 = 42;
+ int_fast32_t ifast32 = (int_fast32_t)42;
printf("Hello world !\n"); /* printf_va_1 */
printf("%s%n",string,& i); /* printf_va_2 */
printf("%ls",wstring); /* printf_va_3 */
@@ -653,7 +653,7 @@ int main(void)
printf("%lu",u64); /* printf_va_19 */
printf("%hhi",(int)i8); /* printf_va_20 */
printf("%lx",uleast64); /* printf_va_21 */
- printf("%d",ifast32); /* printf_va_22 */
+ printf("%ld",ifast32); /* printf_va_22 */
printf("%f %Le\n",f,L); /* printf_va_23 */
printf("%c\n",(int)c); /* printf_va_24 */
printf("%p ",(void *)string); /* printf_va_25 */
diff --git a/tests/builtins/oracle/free.res.oracle b/tests/builtins/oracle/free.res.oracle
index 1f95b2c0061..4f5cb6ae56f 100644
--- a/tests/builtins/oracle/free.res.oracle
+++ b/tests/builtins/oracle/free.res.oracle
@@ -15,7 +15,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
diff --git a/tests/builtins/oracle/linked_list.0.res.oracle b/tests/builtins/oracle/linked_list.0.res.oracle
index c7cf1e94218..61083435b7a 100644
--- a/tests/builtins/oracle/linked_list.0.res.oracle
+++ b/tests/builtins/oracle/linked_list.0.res.oracle
@@ -15,12 +15,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -58,12 +58,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -97,12 +97,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -139,12 +139,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -180,12 +180,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -225,12 +225,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -268,12 +268,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -315,12 +315,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -360,12 +360,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -409,12 +409,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -456,12 +456,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -507,12 +507,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -800,12 +800,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -1095,12 +1095,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -1386,12 +1386,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -1681,12 +1681,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -1973,12 +1973,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -2269,12 +2269,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..2047] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index a6456f3e810..ab1cd53fb4a 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -15,12 +15,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -58,12 +58,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -97,12 +97,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -139,12 +139,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -180,12 +180,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -225,12 +225,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -268,12 +268,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -315,12 +315,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -360,12 +360,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -409,12 +409,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -457,12 +457,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -509,12 +509,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -556,12 +556,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -601,12 +601,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -642,12 +642,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -687,12 +687,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -731,12 +731,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -775,12 +775,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
diff --git a/tests/builtins/oracle/linked_list.2.res.oracle b/tests/builtins/oracle/linked_list.2.res.oracle
index 43dbed7de1e..72eef5ce30b 100644
--- a/tests/builtins/oracle/linked_list.2.res.oracle
+++ b/tests/builtins/oracle/linked_list.2.res.oracle
@@ -15,12 +15,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -58,12 +58,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -96,12 +96,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -138,12 +138,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -179,12 +179,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -224,12 +224,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -267,12 +267,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -314,12 +314,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -359,12 +359,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -408,12 +408,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -455,12 +455,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -506,12 +506,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -555,12 +555,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -608,12 +608,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -659,12 +659,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -714,12 +714,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -767,12 +767,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -824,12 +824,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -879,12 +879,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -938,12 +938,12 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_tmpnam[0..19] ∈ {0}
__fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {0x7FFF}
+ __fc_rand_max ∈ {0x7FFFFFFF}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
diff --git a/tests/builtins/oracle/malloc-size-zero.0.res.oracle b/tests/builtins/oracle/malloc-size-zero.0.res.oracle
index 144bf5624b3..1b725ab6061 100644
--- a/tests/builtins/oracle/malloc-size-zero.0.res.oracle
+++ b/tests/builtins/oracle/malloc-size-zero.0.res.oracle
@@ -50,7 +50,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
diff --git a/tests/builtins/oracle/malloc-size-zero.1.res.oracle b/tests/builtins/oracle/malloc-size-zero.1.res.oracle
index 79f6728188c..511d5f834c3 100644
--- a/tests/builtins/oracle/malloc-size-zero.1.res.oracle
+++ b/tests/builtins/oracle/malloc-size-zero.1.res.oracle
@@ -32,7 +32,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
diff --git a/tests/builtins/oracle/realloc.res.oracle b/tests/builtins/oracle/realloc.res.oracle
index 3441c23c27b..df107558a52 100644
--- a/tests/builtins/oracle/realloc.res.oracle
+++ b/tests/builtins/oracle/realloc.res.oracle
@@ -13,7 +13,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -41,7 +41,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -87,7 +87,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -129,7 +129,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -161,7 +161,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -226,7 +226,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -280,7 +280,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -342,7 +342,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -371,7 +371,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -436,7 +436,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -463,7 +463,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -501,7 +501,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -538,7 +538,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -576,7 +576,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -606,7 +606,7 @@
# cvalue:
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
+ __fc_rand_max ∈ {2147483647}
__fc_random48_init ∈ {0}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
diff --git a/tests/builtins/oracle_gauges/realloc.res.oracle b/tests/builtins/oracle_gauges/realloc.res.oracle
index 05fc14b03b3..7db5bb28555 100644
--- a/tests/builtins/oracle_gauges/realloc.res.oracle
+++ b/tests/builtins/oracle_gauges/realloc.res.oracle
@@ -8,7 +8,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -36,7 +36,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -64,7 +64,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -92,7 +92,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -120,7 +120,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -148,7 +148,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -176,7 +176,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -204,7 +204,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -232,7 +232,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -261,7 +261,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -289,7 +289,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -317,7 +317,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 2b84b5e6d38..76dc3eb09e9 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1136,16 +1136,15 @@
\result ≡ __fc_p_tmpnam
Unverifiable but considered Valid.
[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 109)
- assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)),
- \result;
+ assigns *(__fc_p_tmpnam + (0 .. 20)), *(s + (0 .. 20)), \result;
Unverifiable but considered Valid.
[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 109)
- assigns *(__fc_p_tmpnam + (0 .. 2048))
- \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
+ assigns *(__fc_p_tmpnam + (0 .. 20))
+ \from *(__fc_p_tmpnam + (0 .. 20)), (indirect: s);
Unverifiable but considered Valid.
[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 111)
- assigns *(s + (0 .. 2048))
- \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
+ assigns *(s + (0 .. 20))
+ \from (indirect: s), *(__fc_p_tmpnam + (0 .. 20));
Unverifiable but considered Valid.
[ Extern ] Froms (file FRAMAC_SHARE/libc/stdio.h, line 112)
assigns \result \from s, __fc_p_tmpnam;
@@ -1426,7 +1425,7 @@
[ Extern ] Post-condition 'result_uchar_or_eof'
ensures
- result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1
+ result_uchar_or_eof: (0 ≤ \result ≤ 255U) ∨ \result ≡ -1
Unverifiable but considered Valid.
[ Extern ] Assigns (file FRAMAC_SHARE/libc/stdio.h, line 261)
assigns *stream, \result;
diff --git a/tests/idct/oracle_multidim/ieee_1180_1990.res.oracle b/tests/idct/oracle_multidim/ieee_1180_1990.res.oracle
index 51a1a894ad9..47aa5d3e5dd 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]
-3910,3932d3744
+3909,3931d3743
< [ - ] 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)
-3936,3958d3747
+3935,3957d3746
< [ - ] 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)
-3980,3982d3768
+3979,3981d3767
< [ - ] Assertion 'Eva,initialization' (file ieee_1180_1990.c, line 109)
< assert Eva: initialization: \initialized(&tmp1[i][j]);
< tried with Eva.
-3986,4019d3771
+3985,4018d3770
< [ - ] 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.
-4040,4042d3791
+4039,4041d3790
< [ - ] Assertion 'Eva,initialization' (file ieee_1180_1990.c, line 150)
< assert Eva: initialization: \initialized(&tmp1[i][j]);
< tried with Eva.
-4046,4079d3794
+4045,4078d3793
< [ - ] 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.
-4179,4195c3894,3900
+4178,4194c3893,3899
< [ 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)
-4199,4200c3904,3907
+4198,4199c3903,3906
< 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,18 +425,18 @@
> 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)
-4204c3911,3913
+4203c3910,3912
< by Eva.
---
> Locally valid, but unreachable.
> By Eva because:
> - Unreachable call 'printf_va_2' (file ieee_1180_1990.c, line 196)
-4261,4262c3970
+4260,4261c3969
< 194 Completely validated
< 16 Locally validated
---
> 192 Completely validated
-4264,4265c3972,3975
+4263,4264c3971,3974
< 56 To be validated
< 836 Total
---
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6e0aac24eeb..af69919cfaa 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1162,7 +1162,7 @@ extern unsigned long long strtoull(char const * restrict nptr,
/*@ ghost extern int __fc_random_counter __attribute__((__unused__)); */
-unsigned long const __fc_rand_max = (unsigned long)32767;
+unsigned long const __fc_rand_max = (unsigned long)2147483647;
/*@ ensures result_range: 0 ≤ \result ≤ __fc_rand_max;
assigns \result, __fc_random_counter;
assigns \result \from __fc_random_counter;
@@ -4068,7 +4068,7 @@ extern int volatile __fc_fds[1024];
0 ≤ i < iovcnt ⇒
\valid((char *)(&(iov + i)->iov_base) +
(0 .. (iov + i)->iov_len - 1));
- requires bounded_iovcnt: 0 ≤ iovcnt ≤ 1024;
+ requires bounded_iovcnt: 0 ≤ iovcnt ≤ 255;
ensures
result_error_or_read_bytes:
\result ≡ -1 ∨
@@ -4101,7 +4101,7 @@ extern ssize_t readv(int fd, struct iovec const *iov, int iovcnt);
0 ≤ i < iovcnt ⇒
\valid_read((char *)(iov + i)->iov_base +
(0 .. (iov + i)->iov_len - 1));
- requires bounded_iovcnt: 0 ≤ iovcnt ≤ 1024;
+ requires bounded_iovcnt: 0 ≤ iovcnt ≤ 255;
requires
bounded_lengths:
\sum(0, iovcnt - 1, \lambda ℤ k; (iov + k)->iov_len) ≤ 2147483647;
@@ -4559,7 +4559,7 @@ int getaddrinfo(char const * restrict nodename,
while (i < 14) {
{
int tmp_4;
- tmp_4 = Frama_C_interval(-128,127);
+ tmp_4 = Frama_C_interval(-127 - 1,127);
sa->sa_data[i] = (char)tmp_4;
}
i ++;
@@ -4595,7 +4595,7 @@ static int res_search(char const *dname, int rec_class, int type,
{
int i = 0;
while (i < anslen - 1) {
- *(answer + i) = Frama_C_char_interval((char)(-128),(char)127);
+ *(answer + i) = Frama_C_char_interval((char)(-127 - 1),(char)127);
i ++;
}
}
@@ -6063,18 +6063,18 @@ FILE * const __fc_p_fopen = __fc_fopen;
*/
extern FILE *tmpfile(void);
-char __fc_tmpnam[2048];
+char __fc_tmpnam[20];
char * const __fc_p_tmpnam = __fc_tmpnam;
-/*@ requires valid_s_or_null: s ≡ \null ∨ \valid(s + (0 .. 2048));
+/*@ requires valid_s_or_null: s ≡ \null ∨ \valid(s + (0 .. 20));
ensures
result_string_or_null:
\result ≡ \null ∨ \result ≡ \old(s) ∨
\result ≡ __fc_p_tmpnam;
- assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)), \result;
- assigns *(__fc_p_tmpnam + (0 .. 2048))
- \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
- assigns *(s + (0 .. 2048))
- \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
+ assigns *(__fc_p_tmpnam + (0 .. 20)), *(s + (0 .. 20)), \result;
+ assigns *(__fc_p_tmpnam + (0 .. 20))
+ \from *(__fc_p_tmpnam + (0 .. 20)), (indirect: s);
+ assigns *(s + (0 .. 20))
+ \from (indirect: s), *(__fc_p_tmpnam + (0 .. 20));
assigns \result \from s, __fc_p_tmpnam;
*/
extern char *tmpnam(char *s);
@@ -6727,7 +6727,7 @@ char *fgets(char * restrict s, int size, FILE * restrict stream)
__retres = s;
goto return_label;
}
- tmp_2 = Frama_C_interval(-128,127);
+ tmp_2 = Frama_C_interval(-127 - 1,127);
char c = (char)tmp_2;
*(s + i) = c;
if ((int)c == '\n') {
@@ -6744,7 +6744,7 @@ char *fgets(char * restrict s, int size, FILE * restrict stream)
}
/*@ requires valid_stream: \valid(stream);
- ensures result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1;
+ ensures result_uchar_or_eof: (0 ≤ \result ≤ 255U) ∨ \result ≡ -1;
assigns *stream, \result;
assigns *stream \from *stream;
assigns \result \from (indirect: *stream);
@@ -6772,7 +6772,7 @@ int fgetc(FILE * restrict stream)
else {
unsigned char tmp_1;
tmp_1 = Frama_C_unsigned_char_interval((unsigned char)0,
- (unsigned char)255);
+ (unsigned char)255U);
__retres = (int)tmp_1;
goto return_label;
}
@@ -7225,9 +7225,9 @@ char *realpath(char const * restrict file_name, char * restrict resolved_name)
goto return_label;
default: break;
}
- int realpath_len = Frama_C_interval(1,256);
+ int realpath_len = Frama_C_interval(1,4096);
if (! resolved_name) {
- resolved_name = (char *)malloc((size_t)256);
+ resolved_name = (char *)malloc((size_t)4096);
if (! resolved_name) {
__fc_errno = 12;
__retres = (char *)0;
@@ -8607,7 +8607,8 @@ int getopt(int argc, char * const *argv, char const *optstring)
optarg = (char *)Frama_C_nondet_ptr((void *)0,
(void *)(*(argv + nondet_ind) + nondet_indlen));
optind = Frama_C_interval(1,argc + 1);
- tmp_2 = Frama_C_unsigned_char_interval((unsigned char)0,(unsigned char)255);
+ tmp_2 = Frama_C_unsigned_char_interval((unsigned char)0,
+ (unsigned char)255U);
tmp_3 = Frama_C_nondet(-1,(int)tmp_2);
__retres = tmp_3;
return_label: return __retres;
@@ -10210,7 +10211,7 @@ extern int iconv_close(iconv_t __x0);
*/
extern iconv_t iconv_open(char const *tocode, char const *fromcode);
-extern char __fc_basename[256];
+extern char __fc_basename[4096];
char *__fc_p_basename = __fc_basename;
/*@ requires
@@ -10225,7 +10226,7 @@ char *__fc_p_basename = __fc_basename;
*/
extern char *basename(char *path);
-extern char __fc_dirname[256];
+extern char __fc_dirname[4096];
char *__fc_p_dirname = __fc_dirname;
/*@ requires
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index dc3e1747f8b..b8e07f4d510 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -44,8 +44,6 @@
[kernel] Parsing FRAMAC_SHARE/libc/__fc_inet.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_integer.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_libc.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_machdep.h (with preprocessing)
-skipping FRAMAC_SHARE/libc/__fc_machdep_linux_shared.h
[kernel] Parsing FRAMAC_SHARE/libc/__fc_select.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_string_axiomatic.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/aio.h (with preprocessing)
diff --git a/tests/libc/oracle/libgen_h.res.oracle b/tests/libc/oracle/libgen_h.res.oracle
index 2eeaf40c580..4d57e4b9a64 100644
--- a/tests/libc/oracle/libgen_h.res.oracle
+++ b/tests/libc/oracle/libgen_h.res.oracle
@@ -38,8 +38,8 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- __fc_basename[0..255] ∈ [--..--]
- __fc_dirname[0..255] ∈ [--..--]
+ __fc_basename[0..4095] ∈ [--..--]
+ __fc_dirname[0..4095] ∈ [--..--]
path[0..127] ∈ [--..--]
base ∈ {{ &__fc_basename[0] ; &path[0] }}
base2 ∈ {{ NULL ; &__fc_basename[0] }}
diff --git a/tests/libc/oracle/limits_h.0.res.oracle b/tests/libc/oracle/limits_h.0.res.oracle
index 5efc6b677c1..4d600cd2ba9 100644
--- a/tests/libc/oracle/limits_h.0.res.oracle
+++ b/tests/libc/oracle/limits_h.0.res.oracle
@@ -32,7 +32,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
size_max ∈ {65535}
- ssize_max ∈ {2147483647}
+ ssize_max ∈ {32767}
intptr_max ∈ {2147483647}
intptr_min ∈ {-2147483648}
uintptr_max ∈ {4294967295}
diff --git a/tests/libc/oracle/limits_h.3.res.oracle b/tests/libc/oracle/limits_h.3.res.oracle
index 5efc6b677c1..4d600cd2ba9 100644
--- a/tests/libc/oracle/limits_h.3.res.oracle
+++ b/tests/libc/oracle/limits_h.3.res.oracle
@@ -32,7 +32,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
size_max ∈ {65535}
- ssize_max ∈ {2147483647}
+ ssize_max ∈ {32767}
intptr_max ∈ {2147483647}
intptr_min ∈ {-2147483648}
uintptr_max ∈ {4294967295}
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 7c70744fb71..efade1922a0 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -126,7 +126,7 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:48:
function sigaction: precondition 'separation,separated_acts' got status valid.
-[eva] FRAMAC_SHARE/libc/signal.h:223:
+[eva] FRAMAC_SHARE/libc/signal.h:229:
cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index cb22bbb0198..276e662d50c 100644
--- a/tests/libc/oracle/stdlib_c.0.res.oracle
+++ b/tests/libc/oracle/stdlib_c.0.res.oracle
@@ -256,21 +256,21 @@
resolved_name ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- realpath_len ∈ [1..256]
+ realpath_len ∈ [1..4096]
__retres ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_main_l44[0..4095] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224_0[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function canonicalize_file_name:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
__malloc_realpath_l224_0[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -289,8 +289,8 @@
canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }}
__retres ∈ {0; 1}
__calloc_w_main_l33[0..1073741823] ∈ {0; 42}
- __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_main_l44[0..4095] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224_0[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle
index 96a5d173a35..95a6a6d6b06 100644
--- a/tests/libc/oracle/stdlib_c.1.res.oracle
+++ b/tests/libc/oracle/stdlib_c.1.res.oracle
@@ -274,21 +274,21 @@
resolved_name ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- realpath_len ∈ [1..256]
+ realpath_len ∈ [1..4096]
__retres ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_main_l44[0..4095] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224_0[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function canonicalize_file_name:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
__malloc_realpath_l224_0[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -307,8 +307,8 @@
canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }}
__retres ∈ {0}
__calloc_w_main_l33[0..1073741823] ∈ {0; 42}
- __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_main_l44[0..4095] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
__malloc_realpath_l224_0[0] ∈ [--..--]
- [1..255] ∈ [--..--] or UNINITIALIZED
+ [1..4095] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index ff5db5635ef..8090933af98 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -228,18 +228,18 @@
resolved_name ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- realpath_len ∈ [1..256]
+ realpath_len ∈ [1..4096]
__retres ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
- __malloc_realpath_l224[0..255] ∈ [--..--] or UNINITIALIZED
- __malloc_realpath_l224_0[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_main_l44[0..4095] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224[0..4095] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0..4095] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function canonicalize_file_name:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
- __malloc_realpath_l224_0[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0..4095] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -260,6 +260,6 @@
__malloc_calloc_l72[0..3] ∈ [--..--] or UNINITIALIZED
__malloc_calloc_l72_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
__malloc_w_calloc_l72_1[0..4294967291] ∈ [--..--] or UNINITIALIZED
- __malloc_main_l44[0..255] ∈ [--..--] or UNINITIALIZED
- __malloc_realpath_l224[0..255] ∈ [--..--] or UNINITIALIZED
- __malloc_realpath_l224_0[0..255] ∈ [--..--] or UNINITIALIZED
+ __malloc_main_l44[0..4095] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224[0..4095] ∈ [--..--] or UNINITIALIZED
+ __malloc_realpath_l224_0[0..4095] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c
index 0fb4129d94d..9e4443c8886 100644
--- a/tests/misc/custom_machdep.c
+++ b/tests/misc/custom_machdep.c
@@ -25,4 +25,4 @@
#include <time.h>
#include <wchar.h>
-int main() { return INT_MAX; }
+int main() { return INT_MAX - CUSTOM_MACHDEP; }
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index 5997c0388e3..f6431f1f5a5 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -53,7 +53,7 @@ let mach =
eof = "(-1)";
fopen_max = "128";
filename_max = "1023";
- path_max = "255";
+ path_max = "256";
tty_name_max = "255";
host_name_max = "255";
l_tmpnam = "255";
@@ -81,6 +81,7 @@ let mach =
"enotsup", "48";
];
machdep_name = "custom_machdep";
+ custom_defs = "#define CUSTOM_MACHDEP 1\n";
}
let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index 1f6ef8d4b4e..7872b93e4dd 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -51,7 +51,7 @@ l_tmpnam: '255'
tmp_max: '255'
tty_name_max: '255'
host_name_max: '255'
-path_max: '255'
+path_max: '256'
rand_max: '0xFFFFFE'
mb_cur_max: '16'
sig_atomic_t: int
@@ -76,3 +76,5 @@ errno:
enomem: "47"
enotsup: "48"
machdep_name: custom_machdep
+custom_defs: |
+ #define CUSTOM_MACHDEP 1
diff --git a/tests/misc/oracle/custom_machdep.0.res.oracle b/tests/misc/oracle/custom_machdep.0.res.oracle
index b91b58058f4..5ef336d10b9 100644
--- a/tests/misc/oracle/custom_machdep.0.res.oracle
+++ b/tests/misc/oracle/custom_machdep.0.res.oracle
@@ -19,7 +19,7 @@
int main(void)
{
int __retres;
- __retres = 8388607;
+ __retres = 8388607 - 1;
return __retres;
}
diff --git a/tests/misc/oracle/custom_machdep.1.res.oracle b/tests/misc/oracle/custom_machdep.1.res.oracle
index 3675c7e7488..85375c33f50 100644
--- a/tests/misc/oracle/custom_machdep.1.res.oracle
+++ b/tests/misc/oracle/custom_machdep.1.res.oracle
@@ -18,7 +18,7 @@
int main(void)
{
int __retres;
- __retres = 8388607;
+ __retres = 8388607 - 1;
return __retres;
}
diff --git a/tests/misc/oracle/print_machdep.res.oracle b/tests/misc/oracle/print_machdep.res.oracle
index 704eecd604f..9c22a9e43ae 100644
--- a/tests/misc/oracle/print_machdep.res.oracle
+++ b/tests/misc/oracle/print_machdep.res.oracle
@@ -1,4 +1,4 @@
-Machine: clang version 15.0.7
+Machine: gcc (GCC) 12.2.1 20230201
sizeof short = 2 (16 bits, aligned on 16 bits)
sizeof int = 4 (32 bits, aligned on 32 bits)
sizeof long = 8 (64 bits, aligned on 64 bits)
diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c
index af14a03a707..5d014018167 100644
--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
@@ -1,5 +1,5 @@
/* run.config*
- FILTER: sed "s:/[^ ]*[/]cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::g; s:$(realpath @FRAMAC_SHARE@)/:FRAMAC_SHARE/:g; s:@PTEST_MAKE_DIR@/result@PTEST_CONFIG@/::g; s: -m32::; s: -m64::"
+ FILTER: sed "s:/[^ ]*[/]cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:[^ ]*[/]__fc_machdep.*\.dir:-ITMP_MACHDEP:g; s:$PWD/::g; s:$(realpath @FRAMAC_SHARE@)/:FRAMAC_SHARE/:g; s:@PTEST_MAKE_DIR@/result@PTEST_CONFIG@/::g; s: -m32::; s: -m64::"
OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 98030ed4398..034b0ca6fe7 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -66,6 +66,7 @@ let md = {
"erange", "34";
];
machdep_name = "machdep_char_unsigned";
+ custom_defs = "";
}
let () =
diff --git a/tests/syntax/oracle/cpp-command.0.res.oracle b/tests/syntax/oracle/cpp-command.0.res.oracle
index e10baa0dfad..914862fa5a3 100644
--- a/tests/syntax/oracle/cpp-command.0.res.oracle
+++ b/tests/syntax/oracle/cpp-command.0.res.oracle
@@ -1,2 +1,2 @@
[kernel] Parsing cpp-command.c (with preprocessing)
-[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i] [-IFRAMAC_SHARE/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc]
+[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i] -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc]
diff --git a/tests/syntax/oracle/cpp-command.1.res.oracle b/tests/syntax/oracle/cpp-command.1.res.oracle
index f0b357a6deb..6d8ee3a2017 100644
--- a/tests/syntax/oracle/cpp-command.1.res.oracle
+++ b/tests/syntax/oracle/cpp-command.1.res.oracle
@@ -1,2 +1,2 @@
[kernel] Parsing cpp-command.c (with preprocessing)
-%1 = cpp-command.c %2 = TMPDIR/FILE.i %args = -IFRAMAC_SHARE/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc
+%1 = cpp-command.c %2 = TMPDIR/FILE.i %args = -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc
diff --git a/tests/syntax/oracle/cpp-command.4.res.oracle b/tests/syntax/oracle/cpp-command.4.res.oracle
index c53f47b8877..e42375af420 100644
--- a/tests/syntax/oracle/cpp-command.4.res.oracle
+++ b/tests/syntax/oracle/cpp-command.4.res.oracle
@@ -1,2 +1,2 @@
[kernel] Preprocessing command:
- gcc -E -C -I. -IFRAMAC_SHARE/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc 'cpp-command.c' -o 'TMPDIR/FILE.i'
+ gcc -E -C -I. -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc 'cpp-command.c' -o 'TMPDIR/FILE.i'
diff --git a/tests/syntax/oracle/cpp-command.6.res.oracle b/tests/syntax/oracle/cpp-command.6.res.oracle
index b27c0fedfd6..ef44555760e 100644
--- a/tests/syntax/oracle/cpp-command.6.res.oracle
+++ b/tests/syntax/oracle/cpp-command.6.res.oracle
@@ -1,7 +1,7 @@
[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Warning: your preprocessor is not known to handle option `-dD'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Parsing cpp-command.c (with preprocessing)
-extra_args: -IFRAMAC_SHARE/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_64 -dD -nostdinc file_extra global_extra
+extra_args: -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc file_extra global_extra
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
/* Generated by Frama-C */
diff --git a/tests/value/oracle_gauges/gauges.res.oracle b/tests/value/oracle_gauges/gauges.res.oracle
index bd0f8dbd9eb..89bba971700 100644
--- a/tests/value/oracle_gauges/gauges.res.oracle
+++ b/tests/value/oracle_gauges/gauges.res.oracle
@@ -135,7 +135,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
@@ -199,7 +199,7 @@
> # cvalue:
> __fc_heap_status ∈ [--..--]
> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
+> __fc_rand_max ∈ {2147483647}
> __fc_random48_init ∈ {0}
> __fc_random48_counter[0..2] ∈ [--..--]
> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
--
GitLab