diff --git a/Changelog b/Changelog
index feb9fbd3b5f7370d162bd509f5fafbee17feb9d6..c46d534ad769b7d9bb0d1fb6c5b9d83edb7a1dc9 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,10 @@
Open Source Release <next-release>
##################################
+###################################
+Open Source Release 24.0 (Chromium)
+###################################
+
- Kernel [2021-09-02] 0-sized flexible array members only available in
gcc_* machdeps, that now also support FAM in nested struct.
- Eva [2021-07-26] Removes the maximum limit of option -eva-ilevel.
diff --git a/Makefile b/Makefile
index a5f8daa3d76f371459e0586a27400b34d9037aee..fbcc54a8fb3c0966658a4a3e3b418e582244dd4b 100644
--- a/Makefile
+++ b/Makefile
@@ -894,11 +894,11 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
domains/cvalue/cvalue_specification \
domains/cvalue/cvalue_domain \
- engine/subdivided_evaluation engine/evaluation engine/abstractions \
- engine/recursion engine/transfer_stmt engine/transfer_specification \
partitioning/auto_loop_unroll \
partitioning/partition partitioning/partitioning_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
+ engine/subdivided_evaluation engine/evaluation engine/abstractions \
+ engine/recursion engine/transfer_stmt engine/transfer_specification \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
domains/taint_domain \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 95e9f72a6f9d21e5558b33525c9cf242887155e0..87f24681b2572e9ab46479914004e7934bc928e5 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -180,6 +180,7 @@ share/libc/__fc_define_clockid_t.h: CEA_LGPL
share/libc/__fc_define_dev_t.h: CEA_LGPL
share/libc/__fc_define_eof.h: CEA_LGPL
share/libc/__fc_define_fd_set_t.h: CEA_LGPL
+share/libc/__fc_define_fds.h: CEA_LGPL
share/libc/__fc_define_file.h: CEA_LGPL
share/libc/__fc_define_fpos_t.h: CEA_LGPL
share/libc/__fc_define_fs_cnt.h: CEA_LGPL
@@ -206,6 +207,7 @@ share/libc/__fc_define_suseconds_t.h: CEA_LGPL
share/libc/__fc_define_time_t.h: CEA_LGPL
share/libc/__fc_define_timer_t.h: CEA_LGPL
share/libc/__fc_define_timespec.h: CEA_LGPL
+share/libc/__fc_define_timeval.h: CEA_LGPL
share/libc/__fc_define_uid_and_gid.h: CEA_LGPL
share/libc/__fc_define_useconds_t.h: CEA_LGPL
share/libc/__fc_define_wchar_t.h: CEA_LGPL
diff --git a/share/Makefile.plugin.template b/share/Makefile.plugin.template
index ca77423063136672f4335cfd2192a467e2580977..9d10617bd82b958d477087115c17e3fd8583c11f 100644
--- a/share/Makefile.plugin.template
+++ b/share/Makefile.plugin.template
@@ -444,7 +444,7 @@ $(NAME_OFLAGS):=$(OFLAGS) $(INCLUDE_FLAGS) $(PLUGIN_OFLAGS)
# DO NOT include the plugin's own directory as search path for compiling
# ml test scripts: they will be loaded in a separate phase, and will only see
# the plugin through its static API
-$(NAME_TEST_BFLAGS):= $(BFLAGS) -w -70 $(INCLUDE_EXT_FLAGS) $(PLUGIN_BFLAGS)
+$(NAME_TEST_BFLAGS):= $(BFLAGS) $(INCLUDE_EXT_FLAGS) $(PLUGIN_BFLAGS) -w -70
$(NAME_TEST_OFLAGS):= $(OFLAGS) $(INCLUDE_EXT_FLAGS) $(PLUGIN_OFLAGS)
$(TARGET_BFLAGS):= $(PLUGIN_LINK_BFLAGS)
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index 2fa09b4071263c4e8a86aad0726fffee8da0a601..0ae1736eebe66d66ca052706a244501f4d6f643b 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/share/analysis-scripts/make_wrapper.py
@@ -22,7 +22,7 @@
# #
##########################################################################
-# This script serves as wrapper to 'make' (when using the analysis-scripts
+# This script serves as wrapper to GNU make (when using the analysis-scripts
# GNUmakefile template): it parses the output and suggests useful commands
# whenever it can, by calling frama-c-script itself.
@@ -38,6 +38,16 @@ MIN_PYTHON = (3, 6) # for automatic Path conversions
if sys.version_info < MIN_PYTHON:
sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
+# Check if GNU make is available and has the minimal required version
+# (4.0). Otherwise, this script will fail.
+# We first test with 'gmake', then 'make', then fail.
+make_cmd = "gmake"
+get_make_major_version_args = r" --version | grep 'GNU Make\s\+\([0-9]\+\)\..*$' | sed -E 's|GNU Make +([0-9]+)\..*|\1|'"
+if os.system(f"test $({make_cmd} {get_make_major_version_args}) -ge 4") != 0:
+ make_cmd = "make"
+ if os.system(f"test $({make_cmd} {get_make_major_version_args}) -ge 4") != 0:
+ sys.exit("error: could not find GNU make >= 4.0 (tried 'gmake' and 'make')")
+
parser = argparse.ArgumentParser(description="""
Builds the specified target, parsing the output to identify and recommend
actions in case of failure.""")
@@ -54,7 +64,7 @@ if not framac_bin:
framac_script = f"{framac_bin}/frama-c-script"
output_lines = []
-cmd_list = ['make', "-C", make_dir] + args
+cmd_list = [make_cmd, "-C", make_dir] + args
with subprocess.Popen(cmd_list,
stdout=subprocess.PIPE,
stderr=subprocess.PIPE) as proc:
diff --git a/share/libc/__fc_define_fd_set_t.h b/share/libc/__fc_define_fd_set_t.h
index 5f9b7c721b2124a2158961a07c7db38eda5506e3..5e6bbe0272593c03712707a3966a0cd086f32250 100644
--- a/share/libc/__fc_define_fd_set_t.h
+++ b/share/libc/__fc_define_fd_set_t.h
@@ -29,40 +29,6 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
typedef struct __fc_fd_set { long __fc_fd_set[FD_SETSIZE / NFDBITS]; } fd_set;
-/*@
- requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset \from *fdset, indirect:fd;
-*/
-extern void FD_CLR(int fd, fd_set *fdset);
-#define FD_CLR FD_CLR
-
-// Note: the 2nd argument in FD_ISSET is not const in some implementations
-// due to historical and compatibility reasons.
-/*@
- requires valid_fdset: \valid_read(fdset);
- requires initialization: \initialized(fdset);
- assigns \result \from indirect:*fdset, indirect:fd;
-*/
-extern int FD_ISSET(int fd, const fd_set *fdset);
-#define FD_ISSET FD_ISSET
-
-/*@
- requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset \from *fdset, indirect:fd;
-*/
-extern void FD_SET(int fd, fd_set *fdset);
-#define FD_SET FD_SET
-
-/*@
- requires valid_fdset: \valid(fdset);
- assigns *fdset \from \nothing;
- ensures initialization: \initialized(fdset);
-*/
-extern void FD_ZERO(fd_set *fdset);
-#define FD_ZERO FD_ZERO
-
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/__fc_define_fds.h b/share/libc/__fc_define_fds.h
new file mode 100644
index 0000000000000000000000000000000000000000..6905aad49acb612be5e77082bcd23d64356053a9
--- /dev/null
+++ b/share/libc/__fc_define_fds.h
@@ -0,0 +1,40 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_FDS
+#define __FC_DEFINE_FDS
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+
+// arbitrary number
+#ifndef __FC_MAX_OPEN_FILES
+#define __FC_MAX_OPEN_FILES 1024
+#endif
+
+// __fc_fds represents the state of open file descriptors.
+extern volatile int __fc_fds[__FC_MAX_OPEN_FILES];
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/__fc_define_timeval.h b/share/libc/__fc_define_timeval.h
new file mode 100644
index 0000000000000000000000000000000000000000..34db8894a582b2e7a28779182505194efadaed79
--- /dev/null
+++ b/share/libc/__fc_define_timeval.h
@@ -0,0 +1,36 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_TIMEVAL
+#define __FC_DEFINE_TIMEVAL
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+#include "__fc_define_suseconds_t.h"
+#include "__fc_define_time_t.h"
+struct timeval {
+ time_t tv_sec;
+ suseconds_t tv_usec;
+};
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/__fc_select.h b/share/libc/__fc_select.h
index 4fc0f3b0aa6e161a24d6daefa686adb5e5223392..1fad5956e876ce077f8db6bfccda7db5ddd8c7d4 100644
--- a/share/libc/__fc_select.h
+++ b/share/libc/__fc_select.h
@@ -24,13 +24,11 @@
#define __FC_SELECT__
#include "features.h"
__PUSH_FC_STDLIB
-#include "__fc_define_time_t.h"
-#include "__fc_define_suseconds_t.h"
#include "__fc_define_fd_set_t.h"
#include "__fc_define_sigset_t.h"
-
-#include "sys/time.h"
-
+#include "__fc_define_suseconds_t.h"
+#include "__fc_define_timeval.h"
+#include "__fc_define_timespec.h"
__BEGIN_DECLS
/* assigns \result \from nfds, *readfds, *writefds,*errorfds,*timeout,*sigmask;
diff --git a/share/libc/getopt.h b/share/libc/getopt.h
index ed3f45384b71e51ed761a1e0d67c7f38462eb608..380abc7f5aba56b890fa82bd197dbce6e5acead3 100644
--- a/share/libc/getopt.h
+++ b/share/libc/getopt.h
@@ -24,10 +24,9 @@
#define __FC_GETOPT_H
#include "features.h"
__PUSH_FC_STDLIB
-
+#include "unistd.h"
__BEGIN_DECLS
-#include "unistd.h"
/* GNU specific */
struct option
diff --git a/share/libc/limits.h b/share/libc/limits.h
index be32d497acd2883f59ef9096978290932287fc37..7c19508f17883e2954384f61b9d79f6ca228440a 100644
--- a/share/libc/limits.h
+++ b/share/libc/limits.h
@@ -95,4 +95,9 @@
*/
#define ARG_MAX 4096
+// POSIX; used by <sys/uio.h>.
+// Must be >= _XOPEN_IOV_MAX, which is 16.
+// 1024 is the value used by some Linux implementations.
+#define IOV_MAX 1024
+
#endif
diff --git a/share/libc/sys/select.h b/share/libc/sys/select.h
index c680c04d2e2ec48a879ee4b74dccc8468abfbdd2..d3ceb4b58487f35543d5c5fdf13ec56deea00c6a 100644
--- a/share/libc/sys/select.h
+++ b/share/libc/sys/select.h
@@ -28,6 +28,40 @@ __BEGIN_DECLS
#include "../__fc_select.h"
+/*@
+ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset \from *fdset, indirect:fd;
+*/
+extern void FD_CLR(int fd, fd_set *fdset);
+#define FD_CLR FD_CLR
+
+// Note: the 2nd argument in FD_ISSET is not const in some implementations
+// due to historical and compatibility reasons.
+/*@
+ requires valid_fdset: \valid_read(fdset);
+ requires initialization: \initialized(fdset);
+ assigns \result \from indirect:*fdset, indirect:fd;
+*/
+extern int FD_ISSET(int fd, const fd_set *fdset);
+#define FD_ISSET FD_ISSET
+
+/*@
+ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset \from *fdset, indirect:fd;
+*/
+extern void FD_SET(int fd, fd_set *fdset);
+#define FD_SET FD_SET
+
+/*@
+ requires valid_fdset: \valid(fdset);
+ assigns *fdset \from \nothing;
+ ensures initialization: \initialized(fdset);
+*/
+extern void FD_ZERO(fd_set *fdset);
+#define FD_ZERO FD_ZERO
+
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index fbd3da31927d47879bb7ef0c81bf878ba4b5fbc7..db0a5b17b0b5ce5a9eaac4e983ac9bdd0eb45abd 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -24,17 +24,12 @@
#define __FC_SYS_TIME_H__
#include "../features.h"
__PUSH_FC_STDLIB
-__BEGIN_DECLS
-
-#include "../__fc_define_time_t.h"
-#include "../__fc_define_suseconds_t.h"
#include "../__fc_define_fd_set_t.h"
-#include "../__fc_define_timespec.h"
+#include "../__fc_define_suseconds_t.h"
+#include "../__fc_define_time_t.h"
+#include "../__fc_define_timeval.h"
#include "../__fc_string_axiomatic.h"
-struct timeval {
- time_t tv_sec;
- suseconds_t tv_usec;
-};
+__BEGIN_DECLS
struct timezone {
int tz_minuteswest;
diff --git a/share/libc/sys/uio.h b/share/libc/sys/uio.h
index 7ef6ce26a73b7c58c36a3413b228658349faa9ff..b46a65c70647568e1d8dd517c2be12e83bd64bc7 100644
--- a/share/libc/sys/uio.h
+++ b/share/libc/sys/uio.h
@@ -28,15 +28,49 @@ __PUSH_FC_STDLIB
#include "../__fc_define_ssize_t.h"
#include "../__fc_define_size_t.h"
#include "../__fc_define_iovec.h"
+#include "../__fc_define_fds.h"
+#include "../limits.h"
__BEGIN_DECLS
-/*@ requires valid_read_iov: \valid_read( &iov[0..iovcnt-1] );
-// Value cannot yet interpret the precise assigns clause; we use the weaker one as a fallback.
-//@ assigns { ((char *) iov[i].iov_base)[0..iov[i].iov_len - 1] | integer i; 0 <= i < iovcnt };
- @ assigns ((char *) iov[0..iovcnt -1].iov_base)[0..];
+
+
+/*@
+ requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
+ requires initialization:initialized_inputs:
+ \forall integer i; 0 <= i < iovcnt ==>
+ \initialized(&iov[i].iov_base) && \initialized(&iov[i].iov_len);
+ requires valid_iov: \forall integer i; 0 <= i < iovcnt ==>
+ \valid( ((char*)&iov[i].iov_base)+(0 .. iov[i].iov_len-1));
+ requires bounded_iovcnt: 0 <= iovcnt <= IOV_MAX;
+ assigns { ((char*)iov[i].iov_base)[j] |
+ integer i, j; 0 <= i < iovcnt && 0 <= j < iov[i].iov_len }
+ \from indirect:fd, indirect:iovcnt, indirect:__fc_fds[fd];
+ assigns \result \from indirect:fd, indirect:__fc_fds[fd], indirect:iov[0 ..],
+ indirect:iovcnt;
+ ensures result_error_or_read_bytes: \result == -1 ||
+ 0 <= \result <= \sum(0,iovcnt-1, \lambda integer k; iov[k].iov_len);
*/
extern ssize_t readv(int fd, const struct iovec *iov, int iovcnt);
+
+/*@
+ requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
+ requires initialization:initialized_inputs:
+ \forall integer i; 0 <= i < iovcnt ==>
+ \initialized(&iov[i].iov_base) && \initialized(&iov[i].iov_len);
+ requires valid_read_iov: \valid_read(&iov[0 .. iovcnt-1]);
+ requires valid_read_iov_bases:
+ \forall integer i; 0 <= i < iovcnt ==>
+ \valid_read(((char*)iov[i].iov_base) + (0 .. iov[i].iov_len-1));
+ requires bounded_iovcnt: 0 <= iovcnt <= IOV_MAX;
+ requires bounded_lengths:
+ \sum(0, iovcnt-1, \lambda integer k; iov[k].iov_len) <= SSIZE_MAX;
+ assigns \result \from indirect:fd, indirect:__fc_fds[fd], indirect:iov[0 ..],
+ indirect:iovcnt;
+ assigns __fc_fds[fd] \from indirect:iov[0 ..], indirect:iovcnt;
+ ensures result_error_or_written_bytes: \result == -1 ||
+ 0 <= \result <= \sum(0, iovcnt-1, \lambda integer k; iov[k].iov_len);
+ */
extern ssize_t writev(int fd, const struct iovec *iov, int iovcnt);
__END_DECLS
diff --git a/share/libc/time.h b/share/libc/time.h
index d156b59c620e759c9709a9b8da294049b57e0476..fe6304ce88d58490ddb41494e6608c6ffed332b0 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -24,14 +24,16 @@
#define __FC_TIME_H
#include "features.h"
__PUSH_FC_STDLIB
+#include "__fc_define_clockid_t.h"
#include "__fc_define_null.h"
#include "__fc_define_size_t.h"
-#include "__fc_define_clockid_t.h"
+#include "__fc_define_time_t.h"
#include "__fc_define_timer_t.h"
+#include "__fc_define_timespec.h"
#include "__fc_string_axiomatic.h"
-
#include "errno.h"
#include "signal.h"
+
/*
* Names of the interval timers, and structure
* defining a timer setting:
@@ -47,7 +49,6 @@ __BEGIN_DECLS
typedef unsigned int clock_t;
#define __clock_t_defined
#endif
-#include "__fc_define_time_t.h"
// From POSIX.1-2008: "The value of CLOCKS_PER_SEC shall be 1 million on
// XSI-conformant systems. [...]"
#define CLOCKS_PER_SEC ((time_t)1000000)
@@ -64,8 +65,6 @@ struct tm {
int tm_isdst; // Daylight Saving Time flag
};
-#include "__fc_define_timespec.h"
-
struct itimerspec {
struct timespec it_interval;
struct timespec it_value;
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index a8c71c4da66bfde812e77250d56ab9b6192509b8..5979b51c4d998f8883c3d332861a36a51cd86688 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -29,16 +29,16 @@ __PUSH_FC_STDLIB
#include "__fc_define_max_open_files.h"
#include "__fc_define_size_t.h"
#include "__fc_define_null.h"
+#include "__fc_define_seek_macros.h"
#include "__fc_define_ssize_t.h"
#include "__fc_define_uid_and_gid.h"
#include "__fc_define_off_t.h"
#include "__fc_define_pid_t.h"
#include "__fc_define_useconds_t.h"
#include "__fc_define_intptr_t.h"
-
-
-
+#include "__fc_define_fds.h"
#include "limits.h"
+__BEGIN_DECLS
extern volatile int Frama_C_entropy_source;
@@ -54,8 +54,6 @@ extern volatile int Frama_C_entropy_source;
#define STDOUT_FILENO 1 /* Standard output. */
#define STDERR_FILENO 2 /* Standard error output. */
-#include "__fc_define_seek_macros.h"
-
/* compatibility macros */
#ifndef __FC_NO_MONOTONIC_CLOCK
@@ -66,8 +64,6 @@ extern volatile int Frama_C_entropy_source;
#define _POSIX_MONOTONIC_CLOCK 0
#endif
-__BEGIN_DECLS
-
/* Values for the NAME argument to `pathconf' and `fpathconf'. */
enum __fc_pathconf_name
{
@@ -722,16 +718,6 @@ enum __fc_confstr_name
#define _CS_V7_ENV _CS_V7_ENV
};
-
-// arbitrary number
-#define __FC_MAX_OPEN_FILES 1024
-
-// __fc_fds represents the state of open file descriptors.
-//@ ghost int __fc_fds[__FC_MAX_OPEN_FILES];
-// TODO: Model the state of some functions more precisely.
-// TODO: define __fc_fds as volatile.
-
-
/*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG, ENOENT,
// ENOTDIR, EROFS, ETXTBSY
// (EINVAL prevented by precondition)
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index d5fa853278e19b22221722a1c0f9ea1304cb2c28..5fe9660ff361769705090186ba8aaec7dd5486e7 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -594,6 +594,27 @@ let build_automaton ~annotations kf =
in
G.iter_edges_e bind_labels g;
+ (* Recursively removes unreachable vertices, except those bound to a statement
+ in [table]. *)
+ let stmt_vertices =
+ let add _stmt (v1, v2) acc = Vertex.Set.(add v1 (add v2 acc)) in
+ StmtTable.fold add table Vertex.Set.empty
+ in
+ let is_unreachable vertex =
+ G.in_degree g vertex = 0
+ && not (Vertex.equal vertex entry_point)
+ && not (Vertex.Set.mem vertex stmt_vertices)
+ in
+ let rec remove_unreachable vertex =
+ let succs = G.succ g vertex in
+ G.remove_vertex g vertex;
+ List.iter remove_unreachable (List.filter is_unreachable succs)
+ in
+ let unreachables =
+ G.fold_vertex (fun v l -> if is_unreachable v then v :: l else l) g []
+ in
+ List.iter remove_unreachable unreachables;
+
(* Return the result *)
{graph = g; entry_point; return_point; stmt_table = table}
diff --git a/src/plugins/aorai/tests/Aorai_test.mli b/src/plugins/aorai/tests/Aorai_test.mli
deleted file mode 100644
index 93dd0917c8512b2e33b4b288d70faf3435badb4a..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/Aorai_test.mli
+++ /dev/null
@@ -1 +0,0 @@
-(* Nothing is exported. *)
diff --git a/src/plugins/aorai/tests/ya/name_projects.mli b/src/plugins/aorai/tests/ya/name_projects.mli
deleted file mode 100644
index 257f4adfc7668a67011f2f6a5043a211ae5b882a..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/ya/name_projects.mli
+++ /dev/null
@@ -1 +0,0 @@
-(* nothing is exported. *)
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index 1a7afd5bee9eaa585b2e079469cfdabf548079f3..313fcf00ef198538e9a90fa4e936f8e944731937 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -342,7 +342,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 487f9d89b834415fa5940e86bf8bd1822b28bedc..cb77e05860c921f2af86471a47a16fd3556fad20 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -187,7 +187,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 2e37d64c5d53416ced6c10ada81782b526bf3fb9..bb72f2bbc63f1b9bba44621ad6fa764bf561cf00 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -366,7 +366,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 44170551c065847fe09d7c0e1cebbfc1f4e0d11b..5288ad885239b257ee03115041beef1d1b10e5e5 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -161,7 +161,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
index e5596bda75141d559c531b4d72aeb27b6bf732cd..355bf7bb1f029994a75c785588cf61c82170aeb9 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
@@ -8,7 +8,7 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index 077e7e1b7111003c5ae82c748c084ea16eaf0819..62a192f51bb497bafc4593371ad9b0a29aa1e3ef 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -66,7 +66,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 406978ac5f39a280b111b1dc00a11a06c240af64..6d74b78c4afc235b980f246374e40a7ed1a19c5c 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -60,7 +60,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index b1e0c13ab7c0c81ddca966a75862fbafdb2ce343..2a293aeb5a71df9b7843ceaf791a0bc6ab4ed61f 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -63,7 +63,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index 2ce7032a3b70da634ea4cb3411354f33cc617c46..665e3c0b1cc2ecddafda0d677d2f1f1a72337ef9 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -19,7 +19,7 @@
`logic functions or predicates with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index 0fb3e03f963f1ca84c2d99208f7a971bf4e3ab08..09a3554adf54d4a676e021dc16c0d7fb3e087768 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -110,7 +110,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 3db1acf837ee0515dc48f8c484b27563489afa38..a4f24c803d736d1fbbdf9803ba71b612cb937a6a 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -903,7 +903,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",860);
+ "FRAMAC_SHARE/libc/unistd.h",846);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 98b179a6be2383e26aac0d389ef7972ac799ecac..b09140dee729c28a7f1f65cee93f96e57c0e5fdc 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -96,7 +96,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
diff --git a/src/plugins/e-acsl/tests/print.mli b/src/plugins/e-acsl/tests/print.mli
deleted file mode 100644
index 9e846eed54c8875c271b1dd7eb248405cf485798..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/print.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 5d0cf41b0baab78657e85110dd86b5c3bd2cae33..718da24a52985bef50b701c9ca5e90154106c37e 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -278,8 +278,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let join_states = function
| [] -> `Bottom
- | [state] -> `Value state
- | s :: l -> `Value (List.fold_left Abstract.Dom.join s l)
+ | (_k,s) :: l ->
+ `Value (List.fold_left Abstract.Dom.join s (List.map snd l))
let compute_call_or_builtin stmt call recursion state =
match Builtins.find_builtin_override call.kf with
@@ -299,7 +299,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Spec.compute_using_specification ~warn:false kinstr call spec state
in
Locations.Location_Bytes.do_track_garbled_mix true;
- let final_state = states >>- join_states in
+ let final_state = join_states states in
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
@@ -314,9 +314,10 @@ module Make (Abstract: Abstractions.Eva) = struct
Builtins.apply_builtin builtin cvalue_call ~pre:cvalue_state ~post
in
let insert cvalue_state =
+ Partition.Key.empty,
Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
in
- let states = Bottom.bot_of_list (List.map insert cvalue_states) in
+ let states = List.map insert cvalue_states in
Transfer.{states; cacheable; builtin=true}
let compute_call =
@@ -344,8 +345,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let final_result =
compute_using_spec_or_body Kglobal call None init_state
in
- let final_states = final_result.Transfer.states in
- let final_state = PowersetDomain.(final_states >>-: of_list >>- join) in
+ let final_states = List.map snd (final_result.Transfer.states) in
+ let final_state = PowersetDomain.(final_states |> of_list |> join) in
Value_util.pop_call_stack ();
Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
Abstract.Dom.Store.mark_as_computed ();
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 933035419a65831bb45ff24fc2c41ae84fd27181..773be0b00ab90f64fae7ca4f1b72b32c17e62b67 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -95,12 +95,12 @@ module Make_Dataflow
(* --- Abstract values storage --- *)
- module Partition = Trace_partitioning.Make (Abstract) (AnalysisParam)
+ module Partitioning = Trace_partitioning.Make (Abstract) (AnalysisParam)
- type store = Partition.store
- type flow = Partition.flow
- type tank = Partition.tank
- type widening = Partition.widening
+ type store = Partitioning.store
+ type flow = Partitioning.flow
+ type tank = Partitioning.tank
+ type widening = Partitioning.widening
type edge_info = {
mutable fireable : bool (* Does any states survive the transition ? *)
@@ -141,9 +141,9 @@ module Make_Dataflow
| `Value state -> state
let initial_tank =
- Partition.initial_tank (States.to_list initial_states)
+ Partitioning.initial_tank (States.to_list initial_states)
let get_initial_flow () =
- -1 (* Dummy edge id *), Partition.drain initial_tank
+ -1 (* Dummy edge id *), Partitioning.drain initial_tank
let post_conditions = ref false
@@ -180,11 +180,11 @@ module Make_Dataflow
(* Default (Initial) stores on vertex and edges *)
let default_vertex_store (v : vertex) () : store =
- Partition.empty_store ~stmt:v.vertex_start_of
+ Partitioning.empty_store ~stmt:v.vertex_start_of
let default_vertex_widening (v : vertex) () : widening =
- Partition.empty_widening ~stmt:v.vertex_start_of
+ Partitioning.empty_widening ~stmt:v.vertex_start_of
let default_edge_tank () : tank * edge_info =
- Partition.empty_tank (), { fireable = false }
+ Partitioning.empty_tank (), { fireable = false }
(* Get the stores associated to a control point or edge *)
let get_vertex_store (v : vertex) : store =
@@ -217,20 +217,24 @@ module Make_Dataflow
(* --- Transfer functions application --- *)
+ type key = Partition.key
type state = Domain.t
- type transfer_function = state -> state list
+ type transfer_function = (key * state) -> (key * state) list
- let id : transfer_function = fun x -> [x]
+ let id : transfer_function = fun (k,x) -> [(k,x)]
(* Thse lifting function helps to uniformize the transfer functions to a
common signature *)
let lift (f : state -> state) : transfer_function =
- fun x -> [f x]
+ fun (k,x) -> [(k,f x)]
let lift' (f : state -> state or_bottom) : transfer_function =
- fun x -> Bottom.to_list (f x)
+ fun (k,x) -> Bottom.to_list (f x >>-: fun y -> k,y)
+
+ let lift'' (f : state -> state list) : transfer_function =
+ fun (k,x) -> List.map (fun y -> k,y) (f x)
let sequence (f1 : transfer_function) (f2 : transfer_function)
: transfer_function =
@@ -269,14 +273,15 @@ module Make_Dataflow
if vars = [] then id else lift (Domain.leave_scope kf vars)
let transfer_call (stmt : stmt) (dest : lval option) (callee : exp)
- (args : exp list) (state : state) : state list =
+ (args : exp list) (key, state : key * state) : (key * state) list =
let result, call_cacheable =
Transfer.call stmt dest callee args state
in
if call_cacheable = Eval.NoCacheCallers then
(* Propagate info that the current call cannot be cached either *)
cacheable := Eval.NoCacheCallers;
- Bottom.list_of_bot result
+ (* Recombine callee partitioning keys with caller key *)
+ Partitioning.call_return ~caller:key result
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
match instr with
@@ -289,13 +294,13 @@ module Make_Dataflow
lift' transfer
| Local_init (vi, ConsInit (f, args, k), loc) ->
let kind = Abstract_domain.Local kf in
- let as_func dest callee args _loc state =
+ let as_func dest callee args _loc (key, state) =
(* This variable enters the scope too early, as it should
be introduced after the call to [f] but before the assignment
to [v]. This is currently not possible, at least without
splitting Transfer.call in two. *)
let state = Domain.enter_scope kind [vi] state in
- transfer_call stmt dest callee args state
+ transfer_call stmt dest callee args (key, state)
in
Cil.treat_constructor_as_func as_func vi f args k loc
| Set (dest, exp, _loc) ->
@@ -331,7 +336,7 @@ module Make_Dataflow
(* Assign the return value *)
and assign_retval =
match return_exp with
- | None -> id
+ | None -> fun state -> [state]
| Some return_exp ->
let vi_ret = Option.get (Library_functions.get_retres_vi kf) in
let return_lval = Var vi_ret, NoOffset in
@@ -342,7 +347,7 @@ module Make_Dataflow
let state' = Transfer.assign state kstmt return_lval return_exp in
Bottom.to_list state'
in
- sequence check_postconditions assign_retval
+ sequence (lift'' check_postconditions) (lift'' assign_retval)
let transfer_transition (t : vertex transition) : transfer_function =
match t with
@@ -357,7 +362,8 @@ module Make_Dataflow
| Leave (block) -> transfer_leave block
| Prop _ -> id (* Annotations are interpreted in [transfer_statement]. *)
- let transfer_annotations (stmt : stmt) ~(record : bool) : transfer_function =
+ let transfer_annotations (stmt : stmt) ~(record : bool)
+ : state -> state list =
let annots =
(* We do not interpret annotations that come from statement contracts
and everything previously emitted by Value (currently, alarms) *)
@@ -395,20 +401,20 @@ module Make_Dataflow
(transition : vertex transition) (flow : flow) : flow =
(* Split return *)
let flow = match transition with
- | Return (return_exp, _) -> Partition.split_return flow return_exp
+ | Return (return_exp, _) -> Partitioning.split_return flow return_exp
| _ -> flow
in
(* Loop transitions *)
let the_stmt v = Option.get v.vertex_start_of in
let enter_loop f v =
- let f = Partition.enter_loop f (the_stmt v) in
- Partition.transfer (lift (Domain.enter_loop (the_stmt v))) f
+ let f = Partitioning.enter_loop f (the_stmt v) in
+ Partitioning.transfer (lift (Domain.enter_loop (the_stmt v))) f
and leave_loop f v =
- let f = Partition.leave_loop f (the_stmt v) in
- Partition.transfer (lift (Domain.leave_loop (the_stmt v))) f
+ let f = Partitioning.leave_loop f (the_stmt v) in
+ Partitioning.transfer (lift (Domain.leave_loop (the_stmt v))) f
and incr_loop_counter f v =
- let f = Partition.next_loop_iteration f (the_stmt v) in
- Partition.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f
+ let f = Partitioning.next_loop_iteration f (the_stmt v) in
+ Partitioning.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f
in
let loops_left, loops_entered =
Interpreted_automata.get_wto_index_diff kf v1 v2
@@ -422,14 +428,14 @@ module Make_Dataflow
let process_edge (v1,e,v2 : G.edge) : flow =
let {edge_transition=transition; edge_kinstr=kinstr} = e in
let tank,edge_info = get_edge_data e in
- let flow = Partition.drain tank in
+ let flow = Partitioning.drain tank in
Db.yield ();
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
- let flow = Partition.transfer (transfer_transition transition) flow in
+ let flow = Partitioning.transfer (transfer_transition transition) flow in
let flow = process_partitioning_transitions v1 v2 transition flow in
- if not (Partition.is_empty_flow flow) then
+ if not (Partitioning.is_empty_flow flow) then
edge_info.fireable <- true;
flow
@@ -439,7 +445,7 @@ module Make_Dataflow
let call_statement_callbacks (stmt : stmt) (f : flow) : unit =
(* TODO: apply on all domains. *)
- let states = Partition.contents f in
+ let states = Partitioning.contents f in
let cvalue_states = gather_cvalues states in
Db.Value.Compute_Statement_Callbacks.apply
(stmt, Value_util.call_stack (), cvalue_states)
@@ -457,36 +463,37 @@ module Make_Dataflow
(* Get vertex store *)
let store = get_vertex_store v in
(* Join incoming s tates *)
- let flow = Partition.join sources store in
+ let flow = Partitioning.join sources store in
let flow =
match v.vertex_start_of with
| Some stmt ->
(* Callbacks *)
call_statement_callbacks stmt flow;
(* Transfer function associated to the statement *)
- Partition.transfer (transfer_statement stmt) flow
+ Partitioning.transfer (lift'' (transfer_statement stmt)) flow
| _ -> flow
in
(* Widen if necessary *)
let flow =
- if widening && not (Partition.is_empty_flow flow) then begin
- let flow = Partition.widen (get_vertex_widening v) flow in
+ if widening && not (Partitioning.is_empty_flow flow) then begin
+ let flow = Partitioning.widen (get_vertex_widening v) flow in
(* Try to correct over-widenings *)
let correct_over_widening stmt =
(* Do *not* record the status after interpreting the annotation
here. Possible unproven assertions have already been recorded
when the assertion has been interpreted the first time higher
in this function. *)
- Partition.transfer (transfer_annotations stmt ~record:false) flow
+ Partitioning.transfer
+ (lift'' (transfer_annotations stmt ~record:false)) flow
in
Option.fold ~some:correct_over_widening ~none:flow v.vertex_start_of
end else
flow
in
(* Dispatch to successors *)
- List.iter (fun into -> Partition.fill flow ~into) (get_succ_tanks v);
+ List.iter (fun into -> Partitioning.fill flow ~into) (get_succ_tanks v);
(* Return whether the iterator should stop or not *)
- Partition.is_empty_flow flow
+ Partitioning.is_empty_flow flow
let process_vertex ?(widening : bool = false) (v : vertex) : bool =
(* Process predecessors *)
@@ -509,7 +516,7 @@ module Make_Dataflow
(* Try every possible successor *)
let add_if_fireable (_,e,succ as edge) acc =
let f = process_edge edge in
- if Partition.is_empty_flow f
+ if Partitioning.is_empty_flow f
then acc
else (e.edge_key,f,succ) :: acc
in
@@ -525,13 +532,13 @@ module Make_Dataflow
let reset_component (vertex_list : vertex list) : unit =
let reset_edge (_,e,_) =
let t,_ = get_edge_data e in
- Partition.reset_tank t
+ Partitioning.reset_tank t
in
let reset_vertex v =
let s = get_vertex_store v
and w = get_vertex_widening v in
- Partition.reset_store s;
- Partition.reset_widening w;
+ Partitioning.reset_store s;
+ Partitioning.reset_widening w;
List.iter reset_edge (G.succ_e graph v)
in
List.iter reset_vertex vertex_list
@@ -547,7 +554,7 @@ module Make_Dataflow
is especially useful for nested loops. *)
if hierachical_convergence
then reset_component (v :: Wto.flatten w)
- else Partition.reset_widening_counter (get_vertex_widening v);
+ else Partitioning.reset_widening_counter (get_vertex_widening v);
(* Iterate until convergence *)
let iteration_count = ref 0 in
while
@@ -578,7 +585,7 @@ module Make_Dataflow
let mark_degeneration () =
let f stmt (v,_) =
let l = get_succ_tanks v in
- if not (List.for_all Partition.is_empty_tank l) then
+ if not (List.for_all Partitioning.is_empty_tank l) then
Value_util.DegenerationPoints.replace stmt false
in
StmtTable.iter f automaton.stmt_table;
@@ -594,7 +601,7 @@ module Make_Dataflow
ignore (Logic.check_fct_postconditions kf active_behaviors Normal
~pre_state:initial_state ~post_states:States.empty ~result:None)
- let compute () : state list or_bottom =
+ let compute () : (key * state) list =
if interpreter_mode then
simulate automaton.entry_point (get_initial_flow ())
else begin
@@ -603,7 +610,7 @@ module Make_Dataflow
end;
if not !post_conditions then mark_postconds_as_true ();
let final_store = get_vertex_store automaton.return_point in
- Bottom.bot_of_list (Partition.expanded final_store)
+ Partitioning.expanded final_store
(* --- Results conversion --- *)
@@ -664,7 +671,7 @@ module Make_Dataflow
let merged_states = VertexTable.create control_point_count
and get_smashed_store v =
let store = get_vertex_store v in
- Partition.smashed store
+ Partitioning.smashed store
in
fun ~all stmt (v : vertex) ->
if all || is_instr stmt
@@ -685,8 +692,8 @@ module Make_Dataflow
let unmerged_pre_cvalues = lazy
(StmtTable.map (fun _stmt (v,_) ->
let store = get_vertex_store v in
- let states = Partition.expanded store in
- List.map (fun x -> Domain.get_cvalue_or_top x) states)
+ let states = Partitioning.expanded store in
+ List.map (fun (_k,x) -> Domain.get_cvalue_or_top x) states)
automaton.stmt_table)
in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
@@ -772,12 +779,10 @@ module Computer
Kernel_function.pretty kf;
Dataflow.merge_results ();
let f = Kernel_function.get_definition kf in
- (match results with
- | `Value (_::_) when Cil.hasAttribute "noreturn" f.svar.vattr ->
- Value_util.warning_once_current
- "function %a may terminate but has the noreturn attribute"
- Kernel_function.pretty kf;
- | _ -> ());
+ if Cil.hasAttribute "noreturn" f.svar.vattr && results <> [] then
+ Value_util.warning_once_current
+ "function %a may terminate but has the noreturn attribute"
+ Kernel_function.pretty kf;
results, !Dataflow.cacheable
in
let cleanup () =
diff --git a/src/plugins/value/engine/iterator.mli b/src/plugins/value/engine/iterator.mli
index 163796d15e9f89c74a07ebdc070d07dbd5e92352..b76ecae19a4dfb7d01a4a1a431ab8f245f067dc7 100644
--- a/src/plugins/value/engine/iterator.mli
+++ b/src/plugins/value/engine/iterator.mli
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Eval
(** Mark the analysis as aborted. It will be stopped at the next safe point *)
val signal_abort: unit -> unit
@@ -46,7 +45,7 @@ module Computer
val compute:
kernel_function -> kinstr -> Abstract.Dom.t ->
- Abstract.Dom.t list or_bottom * Eval.cacheable
+ (Partition.key * Abstract.Dom.t) list * Eval.cacheable
end
diff --git a/src/plugins/value/engine/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml
index 7a8e035182171a115ef14e51c0f8b27a4a4790e0..54c5d3f5e9fed0290d05a783a031fb9d0db34f70 100644
--- a/src/plugins/value/engine/mem_exec.ml
+++ b/src/plugins/value/engine/mem_exec.ml
@@ -53,7 +53,7 @@ module Make
incr counter;
- module CallOutput = Datatype.List (Domain)
+ module CallOutput = Datatype.List (Datatype.Pair (Partition.Key) (Domain))
module StoredResult =
Datatype.Triple
@@ -145,7 +145,7 @@ module Make
else expand_inputs_with_relations (count - 1) kf expanded_bases state
let store_computed_call kf input_state args
- (call_result: Domain.t list Bottom.or_bottom) =
+ (call_result: (Partition.key * Domain.t) list) =
match Transfer_stmt.current_kf_inout () with
| None -> ()
| Some inout ->
@@ -196,10 +196,8 @@ module Make
let all_output_bases =
Extlib.opt_fold Base.Hptset.add return_base all_output_bases
in
- let clear state = Domain.filter kf `Post all_output_bases state in
- let call_result = match call_result with
- | `Bottom -> []
- | `Value list -> list
+ let clear (key,state) =
+ key, Domain.filter kf `Post all_output_bases state
in
let outputs = List.map clear call_result in
let call_number = current_counter () in
@@ -248,7 +246,8 @@ module Make
let bases, outputs, i = Domain.Hashtbl.find hstates st_filtered in
(* We have found a previous execution, in which the outputs are
[outputs]. Copy them in [state] and return this result. *)
- let process output =
+ let process (key,output) =
+ key,
Domain.reuse kf bases ~current_input:state ~previous_output:output
in
let outputs = List.map process outputs in
@@ -268,7 +267,7 @@ module Make
| Not_found -> None
| Result_found (outputs, i) ->
let call_result = outputs in
- Some (Bottom.bot_of_list call_result, i)
+ Some (call_result, i)
end
diff --git a/src/plugins/value/engine/mem_exec.mli b/src/plugins/value/engine/mem_exec.mli
index afc29371ac5d18fcf22ff5951e266d3a33a63448..cb2a641032a00a2411246ebba9a16d8a0230b072 100644
--- a/src/plugins/value/engine/mem_exec.mli
+++ b/src/plugins/value/engine/mem_exec.mli
@@ -41,7 +41,7 @@ module Make
to be reused in subsequent calls *)
val store_computed_call:
kernel_function -> Domain.t -> Value.t or_bottom list ->
- Domain.t list or_bottom ->
+ (Partition.key * Domain.t) list ->
unit
(** [reuse_previous_call kf init_state args] searches amongst the previous
@@ -52,7 +52,7 @@ module Make
by the plugins that have registered Value callbacks.) *)
val reuse_previous_call:
kernel_function -> Domain.t -> Value.t or_bottom list ->
- (Domain.t list or_bottom * int) option
+ ((Partition.key * Domain.t) list * int) option
end
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 5e782e06f03b02524bd062c667909e29cc063d00..1bd620279bfbd9acdfb0797536bcc5f5e71d3e19 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -567,7 +567,7 @@ module Make
let compute_using_specification ~warn kinstr call spec state =
let vi = Kernel_function.get_vi call.kf in
if Cil.hasAttribute "noreturn" vi.vattr
- then `Bottom
+ then []
else
(* Initializes the variable returned by the function. *)
let state = match call.return with
@@ -582,8 +582,6 @@ module Make
let states =
compute_specification ~warn kinstr call.kf call.return spec state
in
- if States.is_empty states
- then `Bottom
- else `Value (States.to_list states)
+ List.map (fun s -> Partition.Key.empty, s) (States.to_list states)
end
diff --git a/src/plugins/value/engine/transfer_specification.mli b/src/plugins/value/engine/transfer_specification.mli
index 06af47c468ce3f30d5eeb4acc8d9f8e8f63e79df..93ea891b66ca643709c14845b09d4b984bf4f2a6 100644
--- a/src/plugins/value/engine/transfer_specification.mli
+++ b/src/plugins/value/engine/transfer_specification.mli
@@ -35,6 +35,6 @@ module Make
val compute_using_specification:
warn:bool ->
kinstr -> (Abstract.Loc.location, Abstract.Val.t) call -> spec ->
- Abstract.Dom.t -> Abstract.Dom.t list or_bottom
+ Abstract.Dom.t -> (Partition.key*Abstract.Dom.t) list
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 1ce8dd5d91ed1f126de402825f9d2298151ea620..261bfb1116eee5def3195c54a383529c0c533e3b 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -32,19 +32,19 @@ module type S = sig
val assume: state -> stmt -> exp -> bool -> state or_bottom
val call:
stmt -> lval option -> exp -> exp list -> state ->
- state list or_bottom * Eval.cacheable
+ (Partition.key * state) list * Eval.cacheable
val check_unspecified_sequence:
stmt ->
state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
unit or_bottom
val enter_scope: kernel_function -> varinfo list -> state -> state
type call_result = {
- states: state list or_bottom;
+ states: (Partition.key * state) list;
cacheable: Eval.cacheable;
builtin: bool;
}
val compute_call_ref:
- (stmt -> (loc, value) call -> recursion option ->state -> call_result) ref
+ (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
end
(* Reference filled in by the callwise-inout callback *)
@@ -296,14 +296,15 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ------------------------------------------------------------------------ *)
type call_result = {
- states: state list or_bottom;
+ states: (Partition.key * state) list;
cacheable: cacheable;
builtin: bool;
}
(* Forward reference to [Eval_funs.compute_call] *)
let compute_call_ref :
- (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
+ (stmt -> (loc, value) call -> recursion option -> state ->
+ call_result) ref
= ref (fun _ -> assert false)
(* Returns the result of a call, and a boolean that indicates whether a
@@ -324,7 +325,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Domain.Store.register_initial_state (Value_util.call_stack ()) state;
!compute_call_ref stmt call recursion state
| `Bottom ->
- { states = `Bottom; cacheable = Cacheable; builtin=false }
+ { states = []; cacheable = Cacheable; builtin=false }
in
cleanup ();
res
@@ -460,8 +461,6 @@ module Make (Abstract: Abstractions.Eva) = struct
let pre = state in
(* Process the call according to the domain decision. *)
let call_result = process_call stmt call recursion valuation state in
- call_result.cacheable,
- call_result.states >>- fun result ->
let leaving_vars = leaving_vars kf_callee in
(* Do not try to reduce concrete arguments if a builtin was used. *)
let gather_reduced_arguments =
@@ -488,11 +487,11 @@ module Make (Abstract: Abstractions.Eva) = struct
in
let states =
List.fold_left
- (fun acc return -> Bottom.add_to_list (process return) acc)
- [] result
+ (fun acc (k,x) -> Bottom.add_to_list (process x >>-: fun y -> k,y) acc)
+ [] call_result.states
in
InOutCallback.clear ();
- Bottom.bot_of_list states
+ call_result.cacheable, states
(* ------------------- Evaluation of the arguments ------------------------ *)
@@ -747,39 +746,40 @@ module Make (Abstract: Abstractions.Eva) = struct
Alarmset.emit ki_call alarms;
let cacheable = ref Cacheable in
let eval =
- functions >>- fun functions ->
+ functions >>-: fun functions ->
let current_kf = Value_util.current_kf () in
let process_one_function kf valuation =
(* The special Frama_C_ functions to print states are handled here. *)
if apply_special_directives ~subdivnb kf args state
then
let () = apply_cvalue_callback kf ki_call state in
- `Value ([state])
+ [(Partition.Key.empty, state)]
else
(* Create the call. *)
let eval, alarms = make_call ~subdivnb kf args valuation state in
Alarmset.emit ki_call alarms;
- eval >>- fun (call, recursion, valuation) ->
- (* Register the call. *)
- Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
- (* Do the call. *)
- let c, states =
- do_one_call valuation stmt lval_option call recursion state
+ let states =
+ eval >>-: fun (call, recursion, valuation) ->
+ (* Register the call. *)
+ Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
+ (* Do the call. *)
+ let c, states =
+ do_one_call valuation stmt lval_option call recursion state
+ in
+ (* If needed, propagate that callers cannot be cached. *)
+ if c = NoCacheCallers then
+ cacheable := NoCacheCallers;
+ states
in
- (* If needed, propagate that callers cannot be cached. *)
- if c = NoCacheCallers then
- cacheable := NoCacheCallers;
- states
+ Bottom.list_of_bot states
in
(* Process each possible function apart, and append the result list. *)
let process acc (kf, valuation) =
- let res = process_one_function kf valuation in
- (Bottom.list_of_bot res) @ acc
+ process_one_function kf valuation @ acc
in
- let states_list = List.fold_left process [] functions in
- Bottom.bot_of_list states_list
+ List.fold_left process [] functions
in
- eval, !cacheable
+ Bottom.list_of_bot eval, !cacheable
(* ------------------------------------------------------------------------ *)
(* Unspecified Sequence *)
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index 87c505e24111ca06f51ce4a9cb5ee3fe9178c788..414b093dbf482237bc4ce17da97da025ac7b1edd 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -37,7 +37,7 @@ module type S = sig
val call:
stmt -> lval option -> exp -> exp list -> state ->
- state list or_bottom * Eval.cacheable
+ (Partition.key * state) list * Eval.cacheable
val check_unspecified_sequence:
Cil_types.stmt ->
@@ -49,7 +49,7 @@ module type S = sig
val enter_scope: kernel_function -> varinfo list -> state -> state
type call_result = {
- states: state list or_bottom;
+ states: (Partition.key * state) list;
cacheable: Eval.cacheable;
builtin: bool;
}
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 1867b8a07201ab6228366f4fb1cff4ce9c212815..d055a778be839921a4cc8f6d1cddb54a2482aaff 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -34,6 +34,37 @@ let new_monitor ~split_limit = {
split_values = Datatype.Integer.Set.empty;
}
+module SplitMonitor = Datatype.Make_with_collections (
+ struct
+ include Datatype.Serializable_undefined
+ module Values = Datatype.Integer.Set
+
+ type t = split_monitor
+
+ let name = "Partition.SplitMonitor"
+
+ let reprs = [ new_monitor ~split_limit:0 ]
+
+ let structural_descr =
+ Structural_descr.t_record
+ [| Datatype.Int.packed_descr; Values.packed_descr |]
+
+ let compare m1 m2 =
+ let c = Int.compare m1.split_limit m2.split_limit in
+ if c <> 0 then c else Values.compare m1.split_values m2.split_values
+
+ let equal = Datatype.from_compare
+
+ let pretty fmt m =
+ Format.fprintf fmt "%d/%d" (Values.cardinal m.split_values) m.split_limit
+
+ let hash m =
+ hash (Datatype.Int.hash m.split_limit, Values.hash m.split_values)
+
+ let copy m =
+ { m with split_values = m.split_values }
+ end)
+
(* --- Stamp rationing --- *)
(* Stamps used to label states according to slevel.
@@ -57,24 +88,44 @@ type split_term = Eva_annotations.split_term =
| Expression of Cil_types.exp
| Predicate of Cil_types.predicate
-module SplitTerm = struct
- type t = split_term
- let compare x y =
- match x, y with
- | Expression e1, Expression e2 -> Cil_datatype.ExpStructEq.compare e1 e2
- | Predicate p1, Predicate p2 -> Logic_utils.compare_predicate p1 p2
- | Expression _, Predicate _ -> 1
- | Predicate _, Expression _ -> -1
-
- let pretty fmt = function
- | Expression e -> Printer.pp_exp fmt e
- | Predicate p -> Printer.pp_predicate fmt p
-end
+module SplitTerm = Datatype.Make_with_collections (struct
+ include Datatype.Serializable_undefined
+
+ module Expressions = Cil_datatype.ExpStructEq
+ module Predicates = Cil_datatype.PredicateStructEq
+
+ type t = split_term
-module SplitMap = Map.Make (SplitTerm)
-module IntPair = Datatype.Pair (Datatype.Int) (Datatype.Int)
-module LoopList = Datatype.List (IntPair)
-module BranchList = Datatype.List (Datatype.Int)
+ let name = "Partition.SplitTerm"
+
+ let reprs =
+ Stdlib.List.map (fun e -> Expression e) Expressions.reprs @
+ Stdlib.List.map (fun p -> Predicate p) Predicates.reprs
+
+ let structural_descr =
+ Structural_descr.t_sum [|
+ [| Expressions.packed_descr |] ;
+ [| Predicates.packed_descr |] |]
+
+ let compare x y =
+ match x, y with
+ | Expression e1, Expression e2 -> Expressions.compare e1 e2
+ | Predicate p1, Predicate p2 -> Logic_utils.compare_predicate p1 p2
+ | Expression _, Predicate _ -> 1
+ | Predicate _, Expression _ -> -1
+
+ let equal = Datatype.from_compare
+
+ let pretty fmt = function
+ | Expression e -> Printer.pp_exp fmt e
+ | Predicate p -> Printer.pp_predicate fmt p
+
+ let hash = function
+ | Expression e -> FCHashtbl.hash (1,Expressions.hash e)
+ | Predicate p -> FCHashtbl.hash (2,Predicates.hash p)
+ end)
+
+module SplitMap = SplitTerm.Map
type branch = int
@@ -108,12 +159,25 @@ type key = {
dynamic_splits : split_monitor SplitMap.t; (* term -> monitor *)
}
+type call_return_policy = {
+ callee_splits: bool;
+ callee_history: bool;
+ caller_history: bool;
+ history_size: int;
+}
+
module Key =
struct
- type t = key
+
+ module IntPair = Datatype.Pair (Datatype.Int) (Datatype.Int)
+ module Stamp = Datatype.Option (IntPair)
+ module BranchList = Datatype.List (Datatype.Int)
+ module LoopList = Datatype.List (IntPair)
+ module Splits = SplitMap.Make (Datatype.Integer)
+ module DSplits = SplitMap.Make (SplitMonitor)
(* Initial key, before any partitioning *)
- let zero = {
+ let empty = {
ration_stamp = None;
branches = [];
loops = [];
@@ -121,43 +185,101 @@ struct
dynamic_splits = SplitMap.empty;
}
- let compare k1 k2 =
- let (<?>) c (cmp,x,y) =
- if c = 0 then cmp x y else c
- in
- Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp
- <?> (LoopList.compare, k1.loops, k2.loops)
- <?> (SplitMap.compare Integer.compare, k1.splits, k2.splits)
- <?> (SplitMap.compare (fun _ _ -> 0), k1.dynamic_splits, k2.dynamic_splits)
- <?> (BranchList.compare, k1.branches, k2.branches)
-
- let pretty fmt key =
- begin match key.ration_stamp with
- | Some (n,_) -> Format.fprintf fmt "#%d" n
- | None -> ()
- end;
- Pretty_utils.pp_list ~pre:"[@[" ~sep:" ;@ " ~suf:"@]]"
- Format.pp_print_int
- fmt
- key.branches;
- Pretty_utils.pp_list ~pre:"(@[" ~sep:" ;@ " ~suf:"@])"
- (fun fmt (i,_j) -> Format.pp_print_int fmt i)
- fmt
- key.loops;
- Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
- (fun fmt (t, i) -> Format.fprintf fmt "%a:%a"
- SplitTerm.pretty t
- (Integer.pretty ~hexa:false) i)
- fmt
- (SplitMap.bindings key.splits)
+ include Datatype.Make_with_collections (struct
+ include Datatype.Serializable_undefined
+
+ type t = key
+
+ let name = "Partition.Key"
+
+ let reprs = [ empty ]
+
+ let structural_descr =
+ Structural_descr.t_record [|
+ Stamp.packed_descr;
+ BranchList.packed_descr;
+ LoopList.packed_descr;
+ Splits.packed_descr;
+ DSplits.packed_descr;
+ |]
+
+ let compare k1 k2 =
+ let (<?>) c (cmp,x,y) =
+ if c = 0 then cmp x y else c
+ in
+ Stdlib.Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp
+ <?> (LoopList.compare, k1.loops, k2.loops)
+ <?> (Splits.compare, k1.splits, k2.splits)
+ (* Ignore monitors in comparison *)
+ <?> (SplitMap.compare (fun _ _ -> 0), k1.dynamic_splits, k2.dynamic_splits)
+ <?> (BranchList.compare, k1.branches, k2.branches)
+
+ let equal = Datatype.from_compare
+
+ let hash k =
+ Stdlib.Hashtbl.hash (
+ Stamp.hash k.ration_stamp,
+ BranchList.hash k.branches,
+ LoopList.hash k.loops,
+ Splits.hash k.splits,
+ DSplits.hash k.dynamic_splits) (* Monitors probably shouldn't be hashed *)
+
+ let pretty fmt key =
+ begin match key.ration_stamp with
+ | Some (n,_) -> Format.fprintf fmt "#%d" n
+ | None -> ()
+ end;
+ Pretty_utils.pp_list ~pre:"[@[" ~sep:" ;@ " ~suf:"@]]"
+ Format.pp_print_int
+ fmt
+ key.branches;
+ Pretty_utils.pp_list ~pre:"(@[" ~sep:" ;@ " ~suf:"@])"
+ (fun fmt (i,_j) -> Format.pp_print_int fmt i)
+ fmt
+ key.loops;
+ Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
+ (fun fmt (t, i) -> Format.fprintf fmt "%a:%a"
+ SplitTerm.pretty t
+ Datatype.Integer.pretty i)
+ fmt
+ (SplitMap.bindings key.splits)
+ end)
let exceed_rationing key = key.ration_stamp = None
+
+ let combine ~policy ~caller ~callee =
+ let keep_second _ v1 v2 =
+ match v1, v2 with
+ | None, None -> None
+ | Some x, None | (Some _ | None), Some x -> Some x
+ in
+ (* There is no need to preserve the uniqueness of ration stamps here, as
+ keys will always be given new stamps before the merge of identical keys.
+ This invariant depends on the sequence of operations performed by
+ the iterator and the trace_partitioning. *)
+ {
+ ration_stamp = None;
+ branches =
+ Extlib.list_first_n policy.history_size (
+ (if policy.callee_history then callee.branches else []) @
+ (if policy.caller_history then caller.branches else [])
+ );
+ loops = caller.loops;
+ splits =
+ if policy.callee_splits
+ then SplitMap.merge keep_second caller.splits callee.splits
+ else caller.splits;
+ dynamic_splits =
+ if policy.callee_splits
+ then SplitMap.merge keep_second caller.dynamic_splits callee.dynamic_splits
+ else caller.dynamic_splits;
+ }
end
(* --- Partitions --- *)
-module KMap = Map.Make (Key)
+module KMap = Key.Map
type 'a partition = 'a KMap.t
@@ -171,8 +293,8 @@ let map = KMap.map
let filter = KMap.filter
let merge = KMap.merge
-let to_list (p : 'a partition) : 'a list =
- KMap.fold (fun _k x l -> x :: l) p []
+let to_list (p : 'a partition) : (key * 'a) list =
+ KMap.fold (fun k x l -> (k, x) :: l) p []
(* --- Partitioning actions --- *)
@@ -207,7 +329,7 @@ struct
let empty = []
let initial (p : 'a list) : t =
- List.map (fun state -> Key.zero, state) p
+ List.map (fun state -> Key.empty, state) p
let to_list (f : t) : state list =
List.map snd f
@@ -511,20 +633,20 @@ struct
in
map_keys transfer p
- let transfer_states (f : state -> state list) (p : t) : t =
+ let transfer (f : (key * state) -> (key * state) list) (p : t) : t =
let n = ref 0 in
- let transfer acc (k,x) =
- let add =
+ let transfer acc key_state =
+ let add l (k, y) =
match k.ration_stamp with
(* No ration stamp, just add the state to the list *)
- | None -> fun l y -> (k,y) :: l
+ | None -> (k, y) :: l
(* There is a ration stamp, set the second part of the stamp to a unique transfer number *)
- | Some (s,_) -> fun l y ->
+ | Some (s,_) ->
let k' = { k with ration_stamp = Some (s, !n) } in
incr n;
- (k',y) :: l
+ (k', y) :: l
in
- List.fold_left add acc (f x)
+ List.fold_left add acc (f key_state)
in
List.fold_left transfer [] p
diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli
index fe3dc9f303f8332f8009fdf419dc10f6676509c1..042c0e4ae6e04332c242b493c2f91f3d390ec1d8 100644
--- a/src/plugins/value/partitioning/partition.mli
+++ b/src/plugins/value/partitioning/partition.mli
@@ -41,11 +41,19 @@
(** Partitioning keys attached to states. *)
type key
+type call_return_policy = {
+ callee_splits: bool;
+ callee_history: bool;
+ caller_history: bool;
+ history_size: int;
+}
+
module Key : sig
- val zero : key (** Initial key: no partitioning. *)
- val compare : key -> key -> int
- val pretty : Format.formatter -> key -> unit
- val exceed_rationing: key -> bool
+ include Datatype.S_with_collections with type t = key
+ val empty : t (** Initial key: no partitioning. *)
+ val exceed_rationing: t -> bool
+ val combine : policy:call_return_policy -> caller:t -> callee:t -> t
+ (** Recombinaison of keys after a call *)
end
(** Collection of states, each identified by a unique key. *)
@@ -54,7 +62,7 @@ type 'state partition
val empty : 'a partition
val is_empty : 'a partition -> bool
val size : 'a partition -> int
-val to_list : 'a partition -> 'a list
+val to_list : 'a partition -> (key*'a) list
val find : key -> 'a partition -> 'a
val replace : key -> 'a -> 'a partition -> 'a partition
val merge : (key -> 'a option -> 'b option -> 'c option) -> 'a partition ->
@@ -182,8 +190,8 @@ sig
val union : t -> t -> t
+ val transfer : ((key * state) -> (key * state) list) -> t -> t
val transfer_keys : t -> action -> t
- val transfer_states : (state -> state list) -> t -> t
val iter : (state -> unit) -> t -> unit
val filter_map: (key -> state -> state option) -> t -> t
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 4ddcf1835217ca9caa6cdfdd8bd8c3f28c1979ce..77aecd2890d236914afb00f77473f73f280a2f4e 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -139,4 +139,12 @@ struct
acc (* Impossible to convert term to lval *)
in
List.fold_left map_annot [] (get_flow_annot stmt)
+
+ let call_return_policy =
+ Partition.{
+ callee_splits = Value_parameters.InterproceduralSplits.get ();
+ callee_history = Value_parameters.InterproceduralHistory.get ();
+ caller_history = true;
+ history_size = history_size;
+ }
end
diff --git a/src/plugins/value/partitioning/partitioning_parameters.mli b/src/plugins/value/partitioning/partitioning_parameters.mli
index 891a2b72b6f988cd8a56f2495f90d55f87a71be1..636eabc5bcf6a76ace74f4b637c1cb8c9d51851a 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.mli
+++ b/src/plugins/value/partitioning/partitioning_parameters.mli
@@ -31,4 +31,5 @@ module Make (Kf : sig val kf: kernel_function end) : sig
val history_size : int
val universal_splits : Partition.action list
val flow_actions : stmt -> Partition.action list
+ val call_return_policy : Partition.call_return_policy
end
diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
index 9ba46bb5eefd06b26813c24013ac7fa535c1911b..61f2b7a458ffc32bdefebcfae7d7048304662d08 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -112,13 +112,13 @@ struct
(* Accessors *)
- let expanded (s : store) : state list =
+ let expanded (s : store) : (key * state) list =
Partition.to_list s.store_partition
let smashed (s : store) : state or_bottom =
match expanded s with
| [] -> `Bottom
- | v1 :: l -> `Value (List.fold_left Domain.join v1 l)
+ | (_k, v1) :: l -> `Value (List.fold_left Domain.join v1 (List.map snd l))
let contents (flow : flow) : state list =
Flow.to_list flow
@@ -175,6 +175,10 @@ struct
then apply (Restrict (return_exp, i))
else apply (Ration empty_rationing)
+ let call_return ~caller result =
+ let combine = Partition.Key.combine ~policy:call_return_policy in
+ List.map (fun (k, s) -> combine ~caller ~callee:k, s) result
+
(* Reset state (for hierchical convergence) *)
let reset_store (s : store) : unit =
@@ -210,7 +214,7 @@ struct
in
into.tank_states <- Partition.merge join into.tank_states new_states
- let transfer = Flow.transfer_states
+ let transfer = Flow.transfer
let output_slevel : int -> unit =
let slevel_display_step = Value_parameters.ShowSlevel.get () in
@@ -239,6 +243,7 @@ struct
in
(* Get every source flow *)
let sources_states =
+ (* Is there more than one non-empty incomming flow ? *)
match sources with
| [(_,flow)] -> [flow]
| sources ->
diff --git a/src/plugins/value/partitioning/trace_partitioning.mli b/src/plugins/value/partitioning/trace_partitioning.mli
index 0fbd96f2888d225aa4c01880e71f5b51c9ecfcef..dbdd548600b7ae0c8926bbfb29adc164f79ea709 100644
--- a/src/plugins/value/partitioning/trace_partitioning.mli
+++ b/src/plugins/value/partitioning/trace_partitioning.mli
@@ -50,7 +50,7 @@ sig
(* --- Accessors --- *)
- val expanded : store -> state list
+ val expanded : store -> (Partition.key * state) list
val smashed : store -> state or_bottom
val contents : flow -> state list
val is_empty_store : store -> bool
@@ -81,6 +81,12 @@ sig
val next_loop_iteration : flow -> Cil_types.stmt -> flow
val split_return : flow -> Cil_types.exp option -> flow
+ (** After the analysis of a function call, recombines callee partitioning keys
+ with the caller key. *)
+ val call_return:
+ caller:Partition.key ->
+ (Partition.key * state) list -> (Partition.key * state) list
+
(* --- Operators --- *)
(** Remove all states from the tank, leaving it empty as if it was just
@@ -91,7 +97,8 @@ sig
val fill : into:tank -> flow -> unit
(** Apply a transfer function to all the states of a propagation. *)
- val transfer : (state -> state list) -> flow -> flow
+ val transfer : ((Partition.key * state) -> (Partition.key * state) list) ->
+ flow -> flow
(** Join all incoming propagations into the given store. This function returns
a set of states which still need to be propagated past the store.
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index c1a44a5949f45fbb30df7eb57e360f70bc44e22d..11f8cce3e58081ea89ad878f2ad8534a50e6507e 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -791,6 +791,24 @@ module SplitLimit =
let () = add_precision_dep SplitLimit.parameter
let () = SplitLimit.set_range 0 max_int
+let () = Parameter_customize.set_group precision_tuning
+module InterproceduralSplits =
+ False
+ (struct
+ let option_name = "-eva-interprocedural-splits"
+ let help = "Keep partitioning splits through function returns"
+ end)
+let () = add_precision_dep InterproceduralSplits.parameter
+
+let () = Parameter_customize.set_group precision_tuning
+module InterproceduralHistory =
+ False
+ (struct
+ let option_name = "-eva-interprocedural-history"
+ let help = "Keep partitioning history through function returns"
+ end)
+let () = add_precision_dep InterproceduralHistory.parameter
+
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.argument_may_be_fundecl ()
module SplitReturnFunction =
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 0442dbcc0bb22414545f59df80dc386b49b15061..a05cde2a46d6bbdf015865524e5dda608eb4d91d 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -79,6 +79,8 @@ module DefaultLoopUnroll : Parameter_sig.Int
module HistoryPartitioning : Parameter_sig.Int
module ValuePartitioning : Parameter_sig.String_set
module SplitLimit : Parameter_sig.Int
+module InterproceduralSplits : Parameter_sig.Bool
+module InterproceduralHistory : Parameter_sig.Bool
module ArrayPrecisionLevel: Parameter_sig.Int
diff --git a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
index 3964a37c4107508e018d69cb6119d25a96bbcbe6..d28bedfb6dede9344daeab4b60386b4636bcb9e2 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:814:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:819:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:824:
+[variadic] FRAMAC_SHARE/libc/unistd.h:810:
Declaration of variadic function execlp.
[variadic] tests/erroneous/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 d3df0e6caaecd4de576cc56e389dabf8762146eb..85b39e35a56ab3ba5e2efcf128af74add1b33744 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:814:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:819:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:824:
+[variadic] FRAMAC_SHARE/libc/unistd.h:810:
Declaration of variadic function execlp.
[variadic] tests/known/exec.c:9: Translating call to execle to a call to execve.
[variadic] tests/known/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 a8e29aef564f9e3150640adc472080a1bb437a93..f04568a4d68f71534e09b863b40a96c050d3b06a 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:814:
+[variadic] FRAMAC_SHARE/libc/unistd.h:800:
Declaration of variadic function execl.
-[variadic] FRAMAC_SHARE/libc/unistd.h:819:
+[variadic] FRAMAC_SHARE/libc/unistd.h:805:
Declaration of variadic function execle.
-[variadic] FRAMAC_SHARE/libc/unistd.h:824:
+[variadic] FRAMAC_SHARE/libc/unistd.h:810:
Declaration of variadic function execlp.
[variadic] tests/known/exec_failed_requirement.c:7:
Translating call to execl to a call to execv.
diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.c
index b52d6c74e87425c96857b0e0bedbcc77f6085f7e..ff8453e32a8f53fa964378522ca13e4b7f822604 100644
--- a/tests/fc_script/make-wrapper.c
+++ b/tests/fc_script/make-wrapper.c
@@ -1,7 +1,7 @@
/* run.config
NOFRAMAC: testing frama-c-script
- COMMENT: we must filter 'make:' output lines, since they differ when run by the CI (e.g. mention to jobserver)
- EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && FRAMAC=../../bin/frama-c ../../bin/frama-c-script make-wrapper --make-dir . -f make-for-make-wrapper.mk | sed -e "s:$PWD:PWD:g" | grep -v "^make.*" | grep -v "recipe for target.*failed" > result/make-wrapper.res 2> result/make-wrapper.err && rm -rf make-for-make-wrapper.parse make-for-make-wrapper.eva
+ COMMENT: we must filter 'make:'/'gmake:' output lines, since they differ when run by the CI (e.g. mention to jobserver)
+ EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && FRAMAC=../../bin/frama-c ../../bin/frama-c-script make-wrapper --make-dir . -f make-for-make-wrapper.mk | sed -E -e "s:$PWD:PWD:g;/^(real|user|sys)/d;" | grep -E -v "^g?make.*" | grep -v "recipe for target.*failed" | grep -v '^$' > result/make-wrapper.res 2> result/make-wrapper.err && rm -rf make-for-make-wrapper.parse make-for-make-wrapper.eva
*/
int defined(int a);
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
index 8370fe5e49498ce18397bc847647adac6ce49eaf..30db8dfd928cbfe5194bba8de7cbadd796f82029 100644
--- a/tests/fc_script/oracle/make-wrapper.res
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -1,11 +1,7 @@
-
Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -cpp-extra-args= make-wrapper.c make-wrapper2.c
-
[kernel] Parsing make-wrapper.c (with preprocessing)
[kernel] Parsing make-wrapper2.c (with preprocessing)
-
Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort
-
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -28,19 +24,14 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war
[eva] Clean up and save partial results.
[kernel] Frama-C aborted: invalid user input.
[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'.
-
***** make-wrapper recommendations *****
-
*** recommendation #1 ***
-
1. Found recursive call at:
stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:14 <-
large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:18 <-
rec :: make-wrapper.c:23 <-
main
-
Consider patching, stubbing or adding an ACSL specification to the recursive call, then re-run the analysis.
-
*** recommendation #2 ***
2. Found function with missing spec: large_name_to_force_line_break_in_stack_msg
Looking for files defining it...
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index 3fab55c7989fe06a0dd332dafeb7f3bb9c6c47d8..fabf605d2b8d14f9aa8503e6553d945e16256a37 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -81,6 +81,49 @@ struct
table
end
+let ident_to_be_ignored id headers =
+ Extlib.string_prefix "__" id ||
+ Extlib.string_prefix "Frama_C" id ||
+ List.filter (fun h -> not (Extlib.string_prefix "__fc" h)) headers = []
+
+let check_ident c11 posix glibc nonstandard c11_headers id headers =
+ if ident_to_be_ignored id headers then (* nothing to check *) ()
+ else begin
+ if Hashtbl.mem c11 id then begin
+ (* Check that the header is the expected one.
+ Note that some symbols may appear in more than one header,
+ possibly due to collisions
+ e.g. 'flock' as type and function). *)
+ let h = Hashtbl.find c11 id in
+ if not (StringSet.mem h c11_headers) then
+ Kernel.warning "<%a>:%s : C11 says %s"
+ (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
+ id h
+ end
+ else if Hashtbl.mem posix id then begin
+ (* check that the header is the expected one *)
+ let (h, _) = Hashtbl.find posix id in
+ (* arpa/inet.h and netinet/in.h are special cases: due to mutual
+ inclusion, there are always issues with their symbols;
+ also, timezone is a special case, since it is a type in
+ sys/time.h, but a variable in time.h in POSIX. However, its
+ declaration as extern is erased by rmtmps, since it is
+ unused. *)
+ if not (List.mem h headers) &&
+ not (List.mem "arpa/inet.h" headers && h = "netinet/in.h" ||
+ List.mem "netinet/in.h" headers && h = "arpa/inet.h") &&
+ id <> "timezone"
+ then
+ Kernel.warning "<%a>:%s : POSIX says %s"
+ (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
+ id h
+ end
+ else if not (StringSet.(mem id glibc || mem id nonstandard)) then
+ Kernel.warning "<%a>:%s : unknown identifier"
+ (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
+ id
+ end
+
let () =
Db.Main.extend (fun () ->
if not !run_once then begin
@@ -94,49 +137,6 @@ let () =
and glibc_idents = Json.(to_set (parse dir "glibc_functions.json"))
and posix_idents = Json.(to_table HeadersAndExtensions (parse dir "posix_identifiers.json"))
and nonstandard_idents = Json.(keys (parse dir "nonstandard_identifiers.json")) in
- Hashtbl.iter (fun id headers ->
- if not (Extlib.string_prefix "__" id) &&
- not (Extlib.string_prefix "Frama_C" id) &&
- List.filter (fun h -> not (Extlib.string_prefix "__fc" h))
- headers <> []
- then
- let id_in_c11 = Hashtbl.mem c11_idents id in
- let id_in_posix = Hashtbl.mem posix_idents id in
- let id_in_glibc = StringSet.mem id glibc_idents in
- let id_in_nonstd = StringSet.mem id nonstandard_idents in
- let header_in_c11 h = StringSet.mem h c11_headers in
- if id_in_c11 then begin
- (* Check that the header is the expected one.
- Note that some symbols may appear in more than one header,
- possibly due to collisions
- (e.g. 'flock' as type and function). *)
- let h = Hashtbl.find c11_idents id in
- if not (header_in_c11 h) then
- Kernel.warning "<%a>:%s : C11 says %s"
- (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
- id h
- end
- else if id_in_posix then begin
- (* check the header is the expected one *)
- let (h, _) = Hashtbl.find posix_idents id in
- (* arpa/inet.h and netinet/in.h are special cases: due to mutual
- inclusion, there are always issues with their symbols;
- also, timezone is a special case, since it is a type in
- sys/time.h, but a variable in time.h in POSIX. However, its
- declaration as extern is erased by rmtmps, since it is
- unused. *)
- if not (List.mem h headers) &&
- not (List.mem "arpa/inet.h" headers && h = "netinet/in.h" ||
- List.mem "netinet/in.h" headers && h = "arpa/inet.h") &&
- id <> "timezone"
- then
- Kernel.warning "<%a>:%s : POSIX says %s"
- (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
- id h
- end
- else if not (id_in_glibc || id_in_nonstd) then
- Kernel.warning "<%a>:%s : unknown identifier"
- (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) headers
- id
- ) fc_stdlib_idents;
+ let check_ident_fun = check_ident c11_idents posix_idents glibc_idents nonstandard_idents c11_headers in
+ Hashtbl.iter check_ident_fun fc_stdlib_idents
end)
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 1345145e950c37a80e559c9426ab5a2ce0dc968e..53b38f02cd517ecf8d921d0aefa51f5aa9693d40 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -44,6 +44,7 @@
#include "__fc_define_dev_t.h"
#include "__fc_define_eof.h"
#include "__fc_define_fd_set_t.h"
+#include "__fc_define_fds.h"
#include "__fc_define_file.h"
#include "__fc_define_fpos_t.h"
#include "__fc_define_fs_cnt.h"
@@ -67,9 +68,10 @@
#include "__fc_define_ssize_t.h"
#include "__fc_define_stat.h"
#include "__fc_define_suseconds_t.h"
-#include "__fc_define_timespec.h"
#include "__fc_define_time_t.h"
#include "__fc_define_timer_t.h"
+#include "__fc_define_timespec.h"
+#include "__fc_define_timeval.h"
#include "__fc_define_uid_and_gid.h"
#include "__fc_define_useconds_t.h"
#include "__fc_define_wchar_t.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 881040218e6562ae1c75d17f17b57abbc7866064..c300bb3596b525db3b01f89b6ba8215600e143c2 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/fc_libc.c:164: assertion got status valid.
-[eva] tests/libc/fc_libc.c:165: assertion got status valid.
[eva] tests/libc/fc_libc.c:166: assertion got status valid.
[eva] tests/libc/fc_libc.c:167: assertion got status valid.
+[eva] tests/libc/fc_libc.c:168: assertion got status valid.
+[eva] tests/libc/fc_libc.c:169: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -47,7 +47,7 @@
wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
wmemset (0 call);
- Specified-only functions (426)
+ Specified-only functions (427)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -175,20 +175,20 @@
wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
- wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ wmemcmp (0 call); wmemmove (0 call); write (0 call); writev (0 call);
Undefined and unspecified functions (1)
=======================================
__builtin_abort (1 call);
- 'Extern' global variables (21)
+ 'Extern' global variables (22)
==============================
- __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
- __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_heap_status;
- __fc_hostname; __fc_locale; __fc_locale_names; __fc_mblen_state;
- __fc_mbtowc_state; __fc_random_counter; __fc_socket_counter;
- __fc_stack_status; __fc_tz; __fc_wctomb_state; optarg; opterr; optopt;
- tzname
+ __fc_basename; __fc_dirname; __fc_fds; __fc_getpwuid_pw_dir;
+ __fc_getpwuid_pw_name; __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell;
+ __fc_heap_status; __fc_hostname; __fc_locale; __fc_locale_names;
+ __fc_mblen_state; __fc_mbtowc_state; __fc_random_counter;
+ __fc_socket_counter; __fc_stack_status; __fc_tz; __fc_wctomb_state; optarg;
+ opterr; optopt; tzname
Potential entry points (1)
==========================
@@ -204,7 +204,7 @@
Goto = 113
Assignment = 625
Exit point = 100
- Function = 527
+ Function = 528
Function call = 144
Pointer dereferencing = 254
Cyclomatic complexity = 371
@@ -214,6 +214,7 @@
#include "__fc_builtin.c"
#include "__fc_builtin.h"
#include "__fc_define_fd_set_t.h"
+#include "__fc_define_timeval.h"
#include "__fc_gcc_builtins.h"
#include "__fc_integer.h"
#include "__fc_select.h"
@@ -264,6 +265,7 @@
#include "stropts.h"
#include "sys/file.h"
#include "sys/resource.h"
+#include "sys/select.h"
#include "sys/sendfile.h"
#include "sys/socket.h"
#include "sys/stat.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index c794e4be1b1caaec773f9e4c3f342430a01ce82f..38af9dde42f8d8384e4405f44b8a48c050d6ff67 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -270,6 +270,10 @@ typedef struct __fc_FILE FILE;
typedef unsigned int id_t;
typedef int suseconds_t;
typedef int clockid_t;
+struct timespec {
+ long tv_sec ;
+ long tv_nsec ;
+};
typedef unsigned int clock_t;
struct tm {
int tm_sec ;
@@ -282,10 +286,6 @@ struct tm {
int tm_yday ;
int tm_isdst ;
};
-struct timespec {
- long tv_sec ;
- long tv_nsec ;
-};
struct dirent {
ino_t d_ino ;
off_t d_off ;
@@ -304,6 +304,10 @@ struct __fc_fd_set {
long __fc_fd_set[(unsigned int)1024 / ((unsigned int)8 * sizeof(long))] ;
};
typedef struct __fc_fd_set fd_set;
+struct timeval {
+ time_t tv_sec ;
+ suseconds_t tv_usec ;
+};
struct flock {
short l_type ;
short l_whence ;
@@ -311,18 +315,6 @@ struct flock {
off_t l_len ;
pid_t l_pid ;
};
-struct timeval {
- time_t tv_sec ;
- suseconds_t tv_usec ;
-};
-struct timezone {
- int tz_minuteswest ;
- int tz_dsttime ;
-};
-struct itimerval {
- struct timeval it_interval ;
- struct timeval it_value ;
-};
typedef void * iconv_t;
struct pollfd {
int fd ;
@@ -350,6 +342,14 @@ struct __fc_code {
int c_val ;
};
typedef struct __fc_code CODE;
+struct timezone {
+ int tz_minuteswest ;
+ int tz_dsttime ;
+};
+struct itimerval {
+ struct timeval it_interval ;
+ struct timeval it_value ;
+};
typedef unsigned long rlim_t;
struct rlimit {
rlim_t rlim_cur ;
@@ -2875,7 +2875,8 @@ int fesetenv(fenv_t const *envp)
return __retres;
}
-/*@ ghost int __fc_fds[1024]; */
+extern int volatile __fc_fds[1024];
+
/*@ requires valid_string_path: valid_read_string(path);
requires valid_amode: (amode & ~((4 | 2) | 1)) ≡ 0 ∨ amode ≡ 0;
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
@@ -4518,11 +4519,70 @@ extern int kill(pid_t pid, int sig);
*/
extern int killpg(pid_t pgrp, int sig);
-/*@ requires valid_read_iov: \valid_read(iov + (0 .. iovcnt - 1));
- assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..));
+/*@ requires valid_fd: 0 ≤ fd < 1024;
+ requires
+ initialization: initialized_inputs:
+ ∀ ℤ i;
+ 0 ≤ i < iovcnt ⇒
+ \initialized(&(iov + i)->iov_base) ∧
+ \initialized(&(iov + i)->iov_len);
+ requires
+ valid_iov:
+ ∀ ℤ i;
+ 0 ≤ i < iovcnt ⇒
+ \valid((char *)(&(iov + i)->iov_base) +
+ (0 .. (iov + i)->iov_len - 1));
+ requires bounded_iovcnt: 0 ≤ iovcnt ≤ 1024;
+ ensures
+ result_error_or_read_bytes:
+ \result ≡ -1 ∨
+ (0 ≤ \result ≤
+ \sum(0, \old(iovcnt) - 1, \lambda ℤ k; (\old(iov) + k)->iov_len));
+ assigns {*((char *)(iov + i)->iov_base + j) |
+ ℤ i, ℤ j; 0 ≤ i < iovcnt ∧ 0 ≤ j < (iov + i)->iov_len},
+ \result;
+ assigns
+ {*((char *)(iov + i)->iov_base + j) |
+ ℤ i, ℤ j; 0 ≤ i < iovcnt ∧ 0 ≤ j < (iov + i)->iov_len}
+ \from (indirect: fd), (indirect: iovcnt), (indirect: __fc_fds[fd]);
+ assigns \result
+ \from (indirect: fd), (indirect: __fc_fds[fd]),
+ (indirect: *(iov + (0 ..))), (indirect: iovcnt);
*/
extern ssize_t readv(int fd, struct iovec const *iov, int iovcnt);
+/*@ requires valid_fd: 0 ≤ fd < 1024;
+ requires
+ initialization: initialized_inputs:
+ ∀ ℤ i;
+ 0 ≤ i < iovcnt ⇒
+ \initialized(&(iov + i)->iov_base) ∧
+ \initialized(&(iov + i)->iov_len);
+ requires valid_read_iov: \valid_read(iov + (0 .. iovcnt - 1));
+ requires
+ valid_read_iov_bases:
+ ∀ ℤ i;
+ 0 ≤ i < iovcnt ⇒
+ \valid_read((char *)(iov + i)->iov_base +
+ (0 .. (iov + i)->iov_len - 1));
+ requires bounded_iovcnt: 0 ≤ iovcnt ≤ 1024;
+ requires
+ bounded_lengths:
+ \sum(0, iovcnt - 1, \lambda ℤ k; (iov + k)->iov_len) ≤ 2147483647;
+ ensures
+ result_error_or_written_bytes:
+ \result ≡ -1 ∨
+ (0 ≤ \result ≤
+ \sum(0, \old(iovcnt) - 1, \lambda ℤ k; (\old(iov) + k)->iov_len));
+ assigns \result, __fc_fds[fd];
+ assigns \result
+ \from (indirect: fd), (indirect: __fc_fds[fd]),
+ (indirect: *(iov + (0 ..))), (indirect: iovcnt);
+ assigns __fc_fds[fd]
+ \from (indirect: *(iov + (0 ..))), (indirect: iovcnt);
+ */
+extern ssize_t writev(int fd, struct iovec const *iov, int iovcnt);
+
/*@ ghost struct __fc_sockfds_type __fc_sockfds[1024]; */
/*@ ghost extern int __fc_socket_counter; */
@@ -7777,34 +7837,6 @@ extern DIR *opendir(char const *path);
*/
extern struct dirent *readdir(DIR *dirp);
-/*@ requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset;
- assigns *fdset \from *fdset, (indirect: fd);
- */
-extern void FD_CLR(int fd, fd_set *fdset);
-
-/*@ requires valid_fdset: \valid_read(fdset);
- requires initialization: \initialized(fdset);
- assigns \result;
- assigns \result \from (indirect: *fdset), (indirect: fd);
- */
-extern int FD_ISSET(int fd, fd_set const *fdset);
-
-/*@ requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset;
- assigns *fdset \from *fdset, (indirect: fd);
- */
-extern void FD_SET(int fd, fd_set *fdset);
-
-/*@ requires valid_fdset: \valid(fdset);
- ensures initialization: \initialized(\old(fdset));
- assigns *fdset;
- assigns *fdset \from \nothing;
- */
-extern void FD_ZERO(fd_set *fdset);
-
/*@ requires valid_res: \valid(res);
ensures initialization: res: \initialized(\old(res));
ensures res_wrapped: *\old(res) ≡ (int)(\old(a) + \old(b));
@@ -8220,192 +8252,6 @@ extern int __va_openat_void(int dirfd, char const *filename, int flags);
extern int __va_openat_mode_t(int dirfd, char const *filename, int flags,
mode_t mode);
-/*@ ghost extern int __fc_tz; */
-
-/*@ requires valid_path: valid_read_string(path);
- requires
- valid_times_or_null: \valid_read(times + (0 .. 1)) ∨ times ≡ \null;
- assigns \result;
- assigns \result
- \from (indirect: *(path + (0 .. strlen{Old}(path)))),
- (indirect: times), (indirect: *(times + (0 .. 1)));
- */
-extern int utimes(char const *path, struct timeval const times[2]);
-
-/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
- assigns tv->tv_sec \from __fc_time;
- assigns tv->tv_usec \from __fc_time;
- assigns *((struct timezone *)tz) \from __fc_tz;
- assigns \result
- \from (indirect: tv), (indirect: tz), *tv, *((struct timezone *)tz),
- __fc_tz;
-
- behavior tv_and_tz_null:
- assumes null_tv_tz: tv ≡ \null ∧ tz ≡ \null;
- assigns \result;
- assigns \result \from (indirect: __fc_tz);
-
- behavior tv_not_null:
- assumes non_null_tv_null_tz: tv ≢ \null ∧ tz ≡ \null;
- ensures
- initialization: tv_sec: tv_usec:
- \initialized(&\old(tv)->tv_sec) ∧
- \initialized(&\old(tv)->tv_usec);
- ensures tv_usec_bounded: 0 ≤ \old(tv)->tv_usec ≤ 999999;
- assigns tv->tv_sec, tv->tv_usec, \result;
- assigns tv->tv_sec \from (indirect: __fc_time);
- assigns tv->tv_usec \from (indirect: __fc_time);
- assigns \result \from (indirect: *tv), (indirect: __fc_tz);
-
- behavior tz_not_null:
- assumes null_tv_non_null_tz: tv ≡ \null ∧ tz ≢ \null;
- ensures initialization: tz: \initialized((struct timezone *)\old(tz));
- assigns *((struct timezone *)tz), \result;
- assigns *((struct timezone *)tz) \from __fc_tz;
- assigns \result
- \from (indirect: *((struct timezone *)tz)), (indirect: __fc_tz);
-
- behavior tv_and_tz_not_null:
- assumes non_null_tv_tz: tv ≢ \null ∧ tz ≢ \null;
- ensures
- initialization: tv_sec: tv_usec:
- \initialized(&\old(tv)->tv_sec) ∧
- \initialized(&\old(tv)->tv_usec);
- ensures initialization: tz: \initialized((struct timezone *)\old(tz));
- assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
- assigns tv->tv_sec \from (indirect: __fc_time);
- assigns tv->tv_usec \from (indirect: __fc_time);
- assigns *((struct timezone *)tz) \from __fc_tz;
- assigns \result
- \from (indirect: *tv), (indirect: *((struct timezone *)tz)),
- (indirect: __fc_tz);
-
- complete behaviors tv_and_tz_not_null,
- tz_not_null,
- tv_not_null,
- tv_and_tz_null;
- disjoint behaviors tv_and_tz_not_null,
- tz_not_null,
- tv_not_null,
- tv_and_tz_null;
- */
-extern int gettimeofday(struct timeval * restrict tv, void * restrict tz);
-
-/*@ requires valid_tv_or_null: \valid_read(tv) ∨ tv ≡ \null;
- requires valid_tz_or_null: \valid_read(tz) ∨ tz ≡ \null;
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns __fc_time, __fc_tz, \result;
- assigns __fc_time
- \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
- assigns __fc_tz
- \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
- assigns \result \from (indirect: *tv), (indirect: *tz);
- */
-extern int settimeofday(struct timeval const *tv, struct timezone const *tz);
-
-/*@ ghost struct itimerval volatile __fc_itimer_real; */
-/*@ ghost struct itimerval volatile __fc_itimer_virtual; */
-/*@ ghost struct itimerval volatile __fc_itimer_prof; */
-/*@ requires valid_curr_value: \valid(curr_value);
- ensures initialization: curr_value: \initialized(\old(curr_value));
- assigns \result, *curr_value;
- assigns \result \from (indirect: which);
- assigns *curr_value
- \from __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
-
- behavior real:
- assumes itimer_real: which ≡ 0;
- ensures result_ok: \result ≡ 0;
- assigns \result, *curr_value;
- assigns \result \from \nothing;
- assigns *curr_value \from __fc_itimer_real;
-
- behavior virtual:
- assumes itimer_virtual: which ≡ 1;
- ensures result_ok: \result ≡ 0;
- assigns \result, *curr_value;
- assigns \result \from \nothing;
- assigns *curr_value \from __fc_itimer_virtual;
-
- behavior prof:
- assumes itimer_prof: which ≡ 2;
- ensures result_ok: \result ≡ 0;
- assigns \result, *curr_value;
- assigns \result \from \nothing;
- assigns *curr_value \from __fc_itimer_prof;
-
- behavior invalid:
- assumes invalid_which: which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2;
- ensures result_error: \result ≡ -1;
- assigns \result;
- assigns \result \from \nothing;
-
- complete behaviors invalid, prof, virtual, real;
- disjoint behaviors invalid, prof, virtual, real;
- */
-extern int getitimer(int which, struct itimerval *curr_value);
-
-/*@ requires valid_new_value: \valid_read(new_value);
- requires
- old_value_null_or_valid: old_value ≡ \null ∨ \valid(old_value);
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns *old_value, \result;
- assigns *old_value
- \from (indirect: which), (indirect: old_value), (indirect: new_value),
- __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
- assigns \result
- \from (indirect: which), (indirect: new_value), (indirect: *new_value);
-
- behavior real:
- assumes
- itimer_real_and_valid:
- which ≡ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
- 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
- ensures result_ok: \result ≡ 0;
- ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, *old_value, __fc_itimer_real;
- assigns \result \from \nothing;
- assigns *old_value \from __fc_itimer_real;
- assigns __fc_itimer_real \from *new_value;
-
- behavior virtual:
- assumes
- itimer_virtual_and_valid:
- which ≡ 1 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
- 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
- ensures result_ok: \result ≡ 0;
- ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, *old_value;
- assigns \result \from \nothing;
- assigns *old_value \from __fc_itimer_virtual;
-
- behavior prof:
- assumes
- itimer_prof_and_valid:
- which ≡ 2 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
- 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
- ensures result_ok: \result ≡ 0;
- ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, *old_value;
- assigns \result \from \nothing;
- assigns *old_value \from __fc_itimer_prof;
-
- behavior invalid:
- assumes
- invalid_itimer_or_new_value:
- (which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2) ∨
- ¬(0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
- 0 ≤ new_value->it_interval.tv_usec ≤ 999999);
- ensures result_error: \result ≡ -1;
- assigns \result;
- assigns \result \from \nothing;
-
- disjoint behaviors invalid, prof, virtual, real;
- */
-extern int setitimer(int which, struct itimerval const * restrict new_value,
- struct itimerval * restrict old_value);
-
/*@ ghost int volatile __fc_fds_state; */
/*@ requires nfds: nfds ≥ 0;
requires readfs: readfds ≡ \null ∨ \valid(readfds);
@@ -8861,6 +8707,220 @@ extern void syslog(int __x0, char const *__x1, void * const *__va_params);
/*@ assigns \nothing; */
extern void vsyslog(int __x0, char const *__x1, va_list __x2);
+/*@ ghost extern int __fc_tz; */
+
+/*@ requires valid_path: valid_read_string(path);
+ requires
+ valid_times_or_null: \valid_read(times + (0 .. 1)) ∨ times ≡ \null;
+ assigns \result;
+ assigns \result
+ \from (indirect: *(path + (0 .. strlen{Old}(path)))),
+ (indirect: times), (indirect: *(times + (0 .. 1)));
+ */
+extern int utimes(char const *path, struct timeval const times[2]);
+
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
+ assigns tv->tv_sec \from __fc_time;
+ assigns tv->tv_usec \from __fc_time;
+ assigns *((struct timezone *)tz) \from __fc_tz;
+ assigns \result
+ \from (indirect: tv), (indirect: tz), *tv, *((struct timezone *)tz),
+ __fc_tz;
+
+ behavior tv_and_tz_null:
+ assumes null_tv_tz: tv ≡ \null ∧ tz ≡ \null;
+ assigns \result;
+ assigns \result \from (indirect: __fc_tz);
+
+ behavior tv_not_null:
+ assumes non_null_tv_null_tz: tv ≢ \null ∧ tz ≡ \null;
+ ensures
+ initialization: tv_sec: tv_usec:
+ \initialized(&\old(tv)->tv_sec) ∧
+ \initialized(&\old(tv)->tv_usec);
+ ensures tv_usec_bounded: 0 ≤ \old(tv)->tv_usec ≤ 999999;
+ assigns tv->tv_sec, tv->tv_usec, \result;
+ assigns tv->tv_sec \from (indirect: __fc_time);
+ assigns tv->tv_usec \from (indirect: __fc_time);
+ assigns \result \from (indirect: *tv), (indirect: __fc_tz);
+
+ behavior tz_not_null:
+ assumes null_tv_non_null_tz: tv ≡ \null ∧ tz ≢ \null;
+ ensures initialization: tz: \initialized((struct timezone *)\old(tz));
+ assigns *((struct timezone *)tz), \result;
+ assigns *((struct timezone *)tz) \from __fc_tz;
+ assigns \result
+ \from (indirect: *((struct timezone *)tz)), (indirect: __fc_tz);
+
+ behavior tv_and_tz_not_null:
+ assumes non_null_tv_tz: tv ≢ \null ∧ tz ≢ \null;
+ ensures
+ initialization: tv_sec: tv_usec:
+ \initialized(&\old(tv)->tv_sec) ∧
+ \initialized(&\old(tv)->tv_usec);
+ ensures initialization: tz: \initialized((struct timezone *)\old(tz));
+ assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result;
+ assigns tv->tv_sec \from (indirect: __fc_time);
+ assigns tv->tv_usec \from (indirect: __fc_time);
+ assigns *((struct timezone *)tz) \from __fc_tz;
+ assigns \result
+ \from (indirect: *tv), (indirect: *((struct timezone *)tz)),
+ (indirect: __fc_tz);
+
+ complete behaviors tv_and_tz_not_null,
+ tz_not_null,
+ tv_not_null,
+ tv_and_tz_null;
+ disjoint behaviors tv_and_tz_not_null,
+ tz_not_null,
+ tv_not_null,
+ tv_and_tz_null;
+ */
+extern int gettimeofday(struct timeval * restrict tv, void * restrict tz);
+
+/*@ requires valid_tv_or_null: \valid_read(tv) ∨ tv ≡ \null;
+ requires valid_tz_or_null: \valid_read(tz) ∨ tz ≡ \null;
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns __fc_time, __fc_tz, \result;
+ assigns __fc_time
+ \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
+ assigns __fc_tz
+ \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
+ assigns \result \from (indirect: *tv), (indirect: *tz);
+ */
+extern int settimeofday(struct timeval const *tv, struct timezone const *tz);
+
+/*@ ghost struct itimerval volatile __fc_itimer_real; */
+/*@ ghost struct itimerval volatile __fc_itimer_virtual; */
+/*@ ghost struct itimerval volatile __fc_itimer_prof; */
+/*@ requires valid_curr_value: \valid(curr_value);
+ ensures initialization: curr_value: \initialized(\old(curr_value));
+ assigns \result, *curr_value;
+ assigns \result \from (indirect: which);
+ assigns *curr_value
+ \from __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
+
+ behavior real:
+ assumes itimer_real: which ≡ 0;
+ ensures result_ok: \result ≡ 0;
+ assigns \result, *curr_value;
+ assigns \result \from \nothing;
+ assigns *curr_value \from __fc_itimer_real;
+
+ behavior virtual:
+ assumes itimer_virtual: which ≡ 1;
+ ensures result_ok: \result ≡ 0;
+ assigns \result, *curr_value;
+ assigns \result \from \nothing;
+ assigns *curr_value \from __fc_itimer_virtual;
+
+ behavior prof:
+ assumes itimer_prof: which ≡ 2;
+ ensures result_ok: \result ≡ 0;
+ assigns \result, *curr_value;
+ assigns \result \from \nothing;
+ assigns *curr_value \from __fc_itimer_prof;
+
+ behavior invalid:
+ assumes invalid_which: which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2;
+ ensures result_error: \result ≡ -1;
+ assigns \result;
+ assigns \result \from \nothing;
+
+ complete behaviors invalid, prof, virtual, real;
+ disjoint behaviors invalid, prof, virtual, real;
+ */
+extern int getitimer(int which, struct itimerval *curr_value);
+
+/*@ requires valid_new_value: \valid_read(new_value);
+ requires
+ old_value_null_or_valid: old_value ≡ \null ∨ \valid(old_value);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns *old_value, \result;
+ assigns *old_value
+ \from (indirect: which), (indirect: old_value), (indirect: new_value),
+ __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
+ assigns \result
+ \from (indirect: which), (indirect: new_value), (indirect: *new_value);
+
+ behavior real:
+ assumes
+ itimer_real_and_valid:
+ which ≡ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
+ 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
+ ensures result_ok: \result ≡ 0;
+ ensures initialization: old_value: \initialized(\old(old_value));
+ assigns \result, *old_value, __fc_itimer_real;
+ assigns \result \from \nothing;
+ assigns *old_value \from __fc_itimer_real;
+ assigns __fc_itimer_real \from *new_value;
+
+ behavior virtual:
+ assumes
+ itimer_virtual_and_valid:
+ which ≡ 1 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
+ 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
+ ensures result_ok: \result ≡ 0;
+ ensures initialization: old_value: \initialized(\old(old_value));
+ assigns \result, *old_value;
+ assigns \result \from \nothing;
+ assigns *old_value \from __fc_itimer_virtual;
+
+ behavior prof:
+ assumes
+ itimer_prof_and_valid:
+ which ≡ 2 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
+ 0 ≤ new_value->it_interval.tv_usec ≤ 999999;
+ ensures result_ok: \result ≡ 0;
+ ensures initialization: old_value: \initialized(\old(old_value));
+ assigns \result, *old_value;
+ assigns \result \from \nothing;
+ assigns *old_value \from __fc_itimer_prof;
+
+ behavior invalid:
+ assumes
+ invalid_itimer_or_new_value:
+ (which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2) ∨
+ ¬(0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧
+ 0 ≤ new_value->it_interval.tv_usec ≤ 999999);
+ ensures result_error: \result ≡ -1;
+ assigns \result;
+ assigns \result \from \nothing;
+
+ disjoint behaviors invalid, prof, virtual, real;
+ */
+extern int setitimer(int which, struct itimerval const * restrict new_value,
+ struct itimerval * restrict old_value);
+
+/*@ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset;
+ assigns *fdset \from *fdset, (indirect: fd);
+ */
+extern void FD_CLR(int fd, fd_set *fdset);
+
+/*@ requires valid_fdset: \valid_read(fdset);
+ requires initialization: \initialized(fdset);
+ assigns \result;
+ assigns \result \from (indirect: *fdset), (indirect: fd);
+ */
+extern int FD_ISSET(int fd, fd_set const *fdset);
+
+/*@ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset;
+ assigns *fdset \from *fdset, (indirect: fd);
+ */
+extern void FD_SET(int fd, fd_set *fdset);
+
+/*@ requires valid_fdset: \valid(fdset);
+ ensures initialization: \initialized(\old(fdset));
+ assigns *fdset;
+ assigns *fdset \from \nothing;
+ */
+extern void FD_ZERO(fd_set *fdset);
+
/*@ assigns \result;
assigns \result \from which, who; */
extern int getpriority(int which, id_t who);
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 815b277af9e8e3fecf6f395a1b1b023ea8dd3ffa..eca9057a10e161facaeb91f1b8b069d8788ad038 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -6,6 +6,7 @@
[kernel] Parsing share/libc/__fc_define_dev_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_eof.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fd_set_t.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_define_fds.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_file.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fpos_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fs_cnt.h (with preprocessing)
@@ -32,6 +33,7 @@
[kernel] Parsing share/libc/__fc_define_time_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_timer_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_timespec.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_define_timeval.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_uid_and_gid.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_useconds_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_wchar_t.h (with preprocessing)
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 75b421147917c7fdf6b9f9bcbd1001f867f21829..884473c2427f4106a9d6c5fded60ee06f15b1c86 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -317,8 +317,8 @@
[eva:final-states] Values at end of function main:
__fc_errno ∈ [--..--]
__fc_heap_status ∈ [--..--]
+ __fc_fds[0..1023] ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
- __fc_fds[0..1023] ∈ {0}
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
__fc_ghbn.host.h_name ∈ {{ NULL ; &__fc_ghbn.hostbuf[0] }}
diff --git a/tests/libc/oracle/socket.0.res.oracle b/tests/libc/oracle/socket.0.res.oracle
index c0f9285b9913c93af17f9c46cecdd5f9e2b994d1..276fcf21362da709bfb1e3539c7ad646d8272d88 100644
--- a/tests/libc/oracle/socket.0.res.oracle
+++ b/tests/libc/oracle/socket.0.res.oracle
@@ -68,24 +68,20 @@
[eva] Done for function test_read
[eva] computing for function test_readv <- main.
Called from tests/libc/socket.c:127.
-[eva] computing for function init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:68.
-[eva] computing for function bzero <- init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:43.
-[eva] Done for function bzero
-[eva] computing for function write <- init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:44.
-[eva] Done for function write
-[eva] Recording results for init_reception
-[eva] Done for function init_reception
+[eva] tests/libc/socket.c:68: Reusing old results for call to init_reception
[eva] computing for function readv <- test_readv <- main.
Called from tests/libc/socket.c:69.
[eva] using specification for function readv
[eva] tests/libc/socket.c:69:
- function readv: precondition 'valid_read_iov' got status valid.
-[eva] share/libc/sys/uio.h:37: Warning:
- no \from part
- for clause 'assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..));'
+ function readv: precondition 'valid_fd' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'valid_iov' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'bounded_iovcnt' got status valid.
+[eva] share/libc/sys/uio.h:52:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
[eva] Done for function readv
[eva:alarm] tests/libc/socket.c:72: Warning:
accessing uninitialized left-value.
@@ -240,8 +236,8 @@
[2].iov_len ∈ {3}
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_recvmsg:
- __fc_sockfds[0..1023] ∈ [--..--]
__fc_fds[0..1023] ∈ [--..--]
+ __fc_sockfds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
rcv_buffer_scattered1[0] ∈ [--..--]
[1] ∈ [--..--] or UNINITIALIZED
@@ -265,9 +261,9 @@
.msg_flags ∈ [--..--] or UNINITIALIZED
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_server_echo:
+ __fc_fds[0..1023] ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
- __fc_fds[0..1023] ∈ [--..--]
fd ∈ [-1..1023]
addr ∈ [--..--] or UNINITIALIZED
addrlen ∈ {8}
@@ -276,9 +272,9 @@
r ∈ [-1..64]
__retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
- __fc_fds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
socket_fd[0..1] ∈ [0..1023]
r ∈ {0; 1; 5; 20; 100; 200; 300; 400}
diff --git a/tests/libc/oracle/socket.1.res.oracle b/tests/libc/oracle/socket.1.res.oracle
index a60c6913b0fb68fee18a85d1c2bc363f9fadb3a7..82d1a5a2090728ffd2cadaba116d11e3f9084d6a 100644
--- a/tests/libc/oracle/socket.1.res.oracle
+++ b/tests/libc/oracle/socket.1.res.oracle
@@ -68,24 +68,20 @@
[eva] Done for function test_read
[eva] computing for function test_readv <- main.
Called from tests/libc/socket.c:127.
-[eva] computing for function init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:68.
-[eva] computing for function bzero <- init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:43.
-[eva] Done for function bzero
-[eva] computing for function write <- init_reception <- test_readv <- main.
- Called from tests/libc/socket.c:44.
-[eva] Done for function write
-[eva] Recording results for init_reception
-[eva] Done for function init_reception
+[eva] tests/libc/socket.c:68: Reusing old results for call to init_reception
[eva] computing for function readv <- test_readv <- main.
Called from tests/libc/socket.c:69.
[eva] using specification for function readv
[eva] tests/libc/socket.c:69:
- function readv: precondition 'valid_read_iov' got status valid.
-[eva] share/libc/sys/uio.h:37: Warning:
- no \from part
- for clause 'assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..));'
+ function readv: precondition 'valid_fd' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'valid_iov' got status valid.
+[eva] tests/libc/socket.c:69:
+ function readv: precondition 'bounded_iovcnt' got status valid.
+[eva] share/libc/sys/uio.h:52:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
[eva] Done for function readv
[eva:alarm] tests/libc/socket.c:72: Warning:
accessing uninitialized left-value.
@@ -240,8 +236,8 @@
[2].iov_len ∈ {3}
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_recvmsg:
- __fc_sockfds[0..1023] ∈ [--..--]
__fc_fds[0..1023] ∈ [--..--]
+ __fc_sockfds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
rcv_buffer_scattered1[0] ∈ [--..--]
[1] ∈ [--..--] or UNINITIALIZED
@@ -267,9 +263,9 @@
.msg_flags ∈ [--..--] or UNINITIALIZED
S___fc_stdout[0..1] ∈ [--..--]
[eva:final-states] Values at end of function test_server_echo:
+ __fc_fds[0..1023] ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
- __fc_fds[0..1023] ∈ [--..--]
fd ∈ [-1..1023]
addr ∈ [--..--] or UNINITIALIZED
addrlen ∈ {8}
@@ -278,9 +274,9 @@
r ∈ [-1..64]
__retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
__fc_sockfds[0..1023] ∈ [--..--]
__fc_socket_counter ∈ [--..--]
- __fc_fds[0..1023] ∈ [--..--]
rcv_buffer[0..9] ∈ {0}
socket_fd[0..1] ∈ [0..1023]
r ∈ {0; 1; 5; 20; 100; 200; 300; 400}
diff --git a/tests/libc/oracle/sys_uio_h.res.oracle b/tests/libc/oracle/sys_uio_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..feee0f8a0d4570603b66fd56bf5d8a7389ebe5d3
--- /dev/null
+++ b/tests/libc/oracle/sys_uio_h.res.oracle
@@ -0,0 +1,112 @@
+[kernel] Parsing tests/libc/sys_uio_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+[eva] computing for function __va_open_mode_t <- main.
+ Called from tests/libc/sys_uio_h.c:17.
+[eva] using specification for function __va_open_mode_t
+[eva] tests/libc/sys_uio_h.c:17:
+ function __va_open_mode_t: precondition 'valid_filename' got status valid.
+[eva] Done for function __va_open_mode_t
+[eva] tests/libc/sys_uio_h.c:19: assertion got status valid.
+[eva] tests/libc/sys_uio_h.c:20: assertion got status valid.
+[eva] tests/libc/sys_uio_h.c:21: assertion got status valid.
+[eva] computing for function writev <- main.
+ Called from tests/libc/sys_uio_h.c:22.
+[eva] using specification for function writev
+[eva] tests/libc/sys_uio_h.c:22:
+ function writev: precondition 'valid_fd' got status valid.
+[eva] tests/libc/sys_uio_h.c:22:
+ function writev: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/sys_uio_h.c:22:
+ function writev: precondition 'valid_read_iov' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:22: Warning:
+ function writev: precondition 'valid_read_iov_bases' got status unknown.
+[eva] tests/libc/sys_uio_h.c:22:
+ function writev: precondition 'bounded_iovcnt' got status valid.
+[eva] share/libc/sys/uio.h:67:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
+[eva:alarm] tests/libc/sys_uio_h.c:22: Warning:
+ function writev: precondition 'bounded_lengths' got status unknown.
+[eva] share/libc/sys/uio.h:72:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
+[eva] Done for function writev
+[eva] computing for function close <- main.
+ Called from tests/libc/sys_uio_h.c:23.
+[eva] using specification for function close
+[eva] tests/libc/sys_uio_h.c:23:
+ function close: precondition 'valid_fd' got status valid.
+[eva] Done for function close
+[eva] computing for function __va_open_void <- main.
+ Called from tests/libc/sys_uio_h.c:24.
+[eva] using specification for function __va_open_void
+[eva] tests/libc/sys_uio_h.c:24:
+ function __va_open_void: precondition 'valid_filename' got status valid.
+[eva] tests/libc/sys_uio_h.c:24:
+ function __va_open_void: precondition 'flag_not_CREAT' got status valid.
+[eva] Done for function __va_open_void
+[eva] computing for function readv <- main.
+ Called from tests/libc/sys_uio_h.c:25.
+[eva] using specification for function readv
+[eva:alarm] tests/libc/sys_uio_h.c:25: Warning:
+ function readv: precondition 'valid_fd' got status unknown.
+[eva] tests/libc/sys_uio_h.c:25:
+ function readv: precondition 'initialization,initialized_inputs' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:25: Warning:
+ function readv: precondition 'valid_iov' got status unknown.
+[eva] tests/libc/sys_uio_h.c:25:
+ function readv: precondition 'bounded_iovcnt' got status valid.
+[eva] share/libc/sys/uio.h:52:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
+[eva] Done for function readv
+[eva] computing for function close <- main.
+ Called from tests/libc/sys_uio_h.c:26.
+[eva] tests/libc/sys_uio_h.c:26:
+ function close: precondition 'valid_fd' got status valid.
+[eva] Done for function close
+[eva] computing for function __va_open_mode_t <- main.
+ Called from tests/libc/sys_uio_h.c:37.
+[eva] tests/libc/sys_uio_h.c:37:
+ function __va_open_mode_t: precondition 'valid_filename' got status valid.
+[eva] Done for function __va_open_mode_t
+[eva] computing for function writev <- main.
+ Called from tests/libc/sys_uio_h.c:39.
+[eva] tests/libc/sys_uio_h.c:39:
+ function writev: precondition 'valid_fd' got status valid.
+[eva] tests/libc/sys_uio_h.c:39:
+ function writev: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/sys_uio_h.c:39:
+ function writev: precondition 'valid_read_iov' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:39: Warning:
+ function writev: precondition 'valid_read_iov_bases' got status unknown.
+[eva] tests/libc/sys_uio_h.c:39:
+ function writev: precondition 'bounded_iovcnt' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:39: Warning:
+ function writev: precondition 'bounded_lengths' got status unknown.
+[eva] Done for function writev
+[eva:alarm] tests/libc/sys_uio_h.c:40: Warning:
+ assertion 'unreachable' got status invalid (stopping propagation).
+[eva:alarm] tests/libc/sys_uio_h.c:43: Warning:
+ signed overflow. assert w + r ≤ 2147483647;
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
+ str ∈ {{ "A small string" }}
+ empty_buf ∈ {0}
+ buf[0..9] ∈ [--..--]
+ buf2[0..13] ∈ [--..--] or UNINITIALIZED
+ v[0].iov_base ∈ {{ "A small string" }}
+ [0].iov_len ∈ {15}
+ [1] ∈ {0}
+ [2].iov_base ∈ {{ (void *)&buf }}
+ [2].iov_len ∈ {10}
+ [3].iov_base ∈ {{ (void *)&buf2 }}
+ [3].iov_len ∈ {14}
+ fd ∈ [-1..1023]
+ w ∈ [-1..2147483647]
+ r ∈ [-1..2147483647]
+ __retres ∈ [-2..2147483647]
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 55e6a1c528de73a57f89e7f4b640206bc2f38233..5173981ab82804e60d054d1f19aea51cd3f81bc2 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -570,9 +570,8 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
- __fc_fds[0] ∈ {0}
- [1..1023] ∈ [--..--]
r ∈ {-1; 0}
hostname[0..255] ∈ [--..--] or UNINITIALIZED
fd ∈ [-1..1023]
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 1ce6be573a566003223a378d330cfdb7e4c1744b..fa6d33a9d1b05edf653138dc9d4527f5421f3532 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -570,9 +570,8 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_fds[0..1023] ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
- __fc_fds[0] ∈ {0}
- [1..1023] ∈ [--..--]
r ∈ {-1; 0}
hostname[0..255] ∈ [--..--] or UNINITIALIZED
fd ∈ [-1..1023]
diff --git a/tests/libc/sys_uio_h.c b/tests/libc/sys_uio_h.c
new file mode 100644
index 0000000000000000000000000000000000000000..2bde83999ac582c7c96456c572735e9c3ceef108
--- /dev/null
+++ b/tests/libc/sys_uio_h.c
@@ -0,0 +1,44 @@
+#include <sys/uio.h>
+#include <unistd.h>
+#include <fcntl.h>
+volatile int nondet;
+int main() {
+ char *str = "A small string";
+ char *empty_buf = 0;
+ char buf[10] = "\n\n\nbuffer";
+ char buf2[14];
+ struct iovec v[4] =
+ {
+ {str, 15},
+ {empty_buf, 0},
+ {buf, 10},
+ {buf2, 14},
+ };
+ int fd = open("/tmp/uio.txt", O_WRONLY | O_CREAT, 0660);
+ if (fd < 0) return 1;
+ //@ assert \valid_read(((char*)v[0].iov_base) + (0 .. v[0].iov_len-1));
+ //@ assert \valid_read(((char*)v[1].iov_base) + (0 .. v[1].iov_len-1));
+ //@ assert \valid_read(((char*)v[2].iov_base) + (0 .. v[2].iov_len-1));
+ ssize_t w = writev(fd, v, 3);
+ close(fd);
+ fd = open("/tmp/uio.txt", O_RDONLY);
+ ssize_t r = readv(fd, v+2, 2);
+ close(fd);
+
+ if (nondet) {
+ char buf3[10] = "\n\n\nbuffer";
+ char buf4[14];
+ struct iovec v2[4] =
+ {
+ {str, 15},
+ {empty_buf, 0},
+ {buf3, 11}, // invalid length
+ };
+ int fd2 = open("/tmp/uio2.txt", O_WRONLY | O_CREAT, 0660);
+ if (fd2 < 0) return 1;
+ ssize_t w = writev(fd2, v2, 3); // must fail
+ //@ assert unreachable: \false;
+ }
+
+ return w + r;
+}
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index a57305d1570190ba61230b014b4c0bec1da423ae..189a5298dc644b531bbc585f569754593b007010 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -44,10 +44,11 @@
=======================================
- 'Extern' global variables (11)
+ 'Extern' global variables (12)
==============================
- Frama_C_entropy_source; __fc_errno; __fc_heap_status; __fc_hostname;
- __fc_stdin; __fc_stdout; __fc_ttyname; optarg; opterr; optind; optopt
+ Frama_C_entropy_source; __fc_errno; __fc_fds; __fc_heap_status;
+ __fc_hostname; __fc_stdin; __fc_stdout; __fc_ttyname; optarg; opterr;
+ optind; optopt
Potential entry points (2)
==========================
diff --git a/tests/metrics/oracle/libc.json b/tests/metrics/oracle/libc.json
index afe73bccdad6b27be86cc5b509fb01fda44e6ce4..de14067e7a65d53a82dd943adb71c6cb31536f68 100644
--- a/tests/metrics/oracle/libc.json
+++ b/tests/metrics/oracle/libc.json
@@ -136,7 +136,7 @@
],
"undefined-functions": [],
"extern-global-vars": [
- "Frama_C_entropy_source", "__fc_errno", "__fc_heap_status",
+ "Frama_C_entropy_source", "__fc_errno", "__fc_fds", "__fc_heap_status",
"__fc_hostname", "__fc_stdin", "__fc_stdout", "__fc_ttyname", "optarg",
"opterr", "optind", "optopt"
],
diff --git a/tests/misc/oracle/interpreted_automata_dataflow_backward.dot b/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
index 47e6019ac1093ecdc6ea36d337a1a351c2cb8f0d..90f737cafe26b8a2a85f1a103dadd5cf611984da 100644
--- a/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
+++ b/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
@@ -4,77 +4,73 @@ digraph G {
cp1 [label=<x>, ];
cp2 [label=< >, ];
cp3 [label=<x>, ];
- cp4 [label=< >, ];
+ cp4 [label=<x, y>, ];
cp5 [label=<x, y>, ];
cp6 [label=<x, y>, ];
- cp7 [label=<x, y>, ];
- cp8 [label=<x>, ];
- cp9 [label=<x, a>, ];
- cp10 [label=<x>, ];
- cp11 [label=<x, a>, ];
- cp12 [label=<x>, ];
+ cp7 [label=<x>, ];
+ cp8 [label=<x, a>, ];
+ cp9 [label=<x>, ];
+ cp10 [label=<x, a>, ];
+ cp11 [label=<x>, ];
+ cp12 [label=<x, a, i>, ];
cp13 [label=<x, a, i>, ];
- cp14 [label=<x, a, i>, ];
- cp15 [label=<x, a, i>, shape=invtriangle, ];
+ cp14 [label=<x, a, i>, shape=invtriangle, ];
+ cp15 [label=<x, a, i>, ];
cp16 [label=<x, a, i>, ];
cp17 [label=<x, a, i>, ];
- cp18 [label=<x, a, i>, ];
+ cp18 [label=<x>, ];
cp19 [label=<x>, ];
- cp20 [label=<x>, ];
+ cp20 [label=<x, a, i>, ];
cp21 [label=<x, a, i>, ];
cp22 [label=<x, a, i>, ];
cp23 [label=<x, a, i>, ];
cp24 [label=<x, a, i>, ];
- cp25 [label=<x, a, i>, ];
- cp26 [label=<x, a, i>, ];
+ cp25 [label=< >, ];
+ cp26 [label=< >, ];
cp27 [label=< >, ];
cp28 [label=< >, ];
cp29 [label=< >, ];
cp30 [label=< >, ];
- cp31 [label=< >, ];
- cp32 [label=< >, ];
+ cp31 [label=<x>, ];
+ cp32 [label=<x>, ];
cp33 [label=<x>, ];
- cp34 [label=<x>, ];
- cp35 [label=<x>, ];
- subgraph cluster_1 { cp26;cp25;cp24;cp23;cp22;cp18;cp17;cp16;cp15;cp14;
+ subgraph cluster_1 { cp24;cp23;cp22;cp21;cp20;cp17;cp16;cp15;cp14;cp13;
};
cp1 -> cp3 [label=<Enter y, z, w, a>, ];
- cp3 -> cp5 [label=<int y = 3;>, ];
- cp4 -> cp2 [label=<Exit y, z, w, a>, ];
- cp5 -> cp6 [label=<y *= 2;>, ];
- cp6 -> cp7 [label=<int z = y + 1;>, ];
- cp7 -> cp8 [label=<int w = y + x;>, ];
- cp8 -> cp9 [label=<int a = 1;>, ];
- cp9 -> cp11 [label=<Enter i>, ];
- cp10 -> cp28 [label=<x != 3>, ];
- cp10 -> cp29 [label=<!(x != 3)>, ];
- cp11 -> cp13 [label=<int i = 0;>, ];
- cp12 -> cp10 [label=<Exit i>, ];
- cp13 -> cp14 [label=< >, ];
- cp14 -> cp15 [constraint=false, label=<Enter >, ];
- cp15 -> cp18 [label=<i < 10>, ];
- cp15 -> cp19 [label=<!(i < 10)>, ];
- cp16 -> cp14 [label=<Exit >, ];
- cp17 -> cp23 [label=<Enter b, c>, ];
- cp18 -> cp17 [label=< >, ];
- cp19 -> cp20 [label=<Enter >, ];
- cp20 -> cp33 [label=< >, ];
- cp21 -> cp17 [label=<Exit >, ];
- cp22 -> cp16 [label=<i ++;>, ];
- cp23 -> cp25 [label=<int b = 3;>, ];
- cp24 -> cp22 [label=<Exit b, c>, ];
- cp25 -> cp26 [label=<int c = i + 1;>, ];
- cp26 -> cp24 [label=<a ++;>, ];
- cp27 -> cp32 [label=<return>, ];
- cp28 -> cp30 [label=<Enter >, ];
- cp29 -> cp27 [label=< >, ];
- cp30 -> cp31 [label=<x = 3;>, ];
- cp31 -> cp27 [label=<Exit >, ];
- cp32 -> cp2 [label=<Exit y, z, w, a>, ];
- cp33 -> cp34 [label=<Exit i>, ];
- cp34 -> cp35 [label=<Exit >, ];
- cp35 -> cp10 [label=<Exit >, ];
+ cp3 -> cp4 [label=<int y = 3;>, ];
+ cp4 -> cp5 [label=<y *= 2;>, ];
+ cp5 -> cp6 [label=<int z = y + 1;>, ];
+ cp6 -> cp7 [label=<int w = y + x;>, ];
+ cp7 -> cp8 [label=<int a = 1;>, ];
+ cp8 -> cp10 [label=<Enter i>, ];
+ cp9 -> cp26 [label=<x != 3>, ];
+ cp9 -> cp27 [label=<!(x != 3)>, ];
+ cp10 -> cp12 [label=<int i = 0;>, ];
+ cp11 -> cp9 [label=<Exit i>, ];
+ cp12 -> cp13 [label=< >, ];
+ cp13 -> cp14 [constraint=false, label=<Enter >, ];
+ cp14 -> cp17 [label=<i < 10>, ];
+ cp14 -> cp18 [label=<!(i < 10)>, ];
+ cp15 -> cp13 [label=<Exit >, ];
+ cp16 -> cp21 [label=<Enter b, c>, ];
+ cp17 -> cp16 [label=< >, ];
+ cp18 -> cp19 [label=<Enter >, ];
+ cp19 -> cp31 [label=< >, ];
+ cp20 -> cp15 [label=<i ++;>, ];
+ cp21 -> cp23 [label=<int b = 3;>, ];
+ cp22 -> cp20 [label=<Exit b, c>, ];
+ cp23 -> cp24 [label=<int c = i + 1;>, ];
+ cp24 -> cp22 [label=<a ++;>, ];
+ cp25 -> cp30 [label=<return>, ];
+ cp26 -> cp28 [label=<Enter >, ];
+ cp27 -> cp25 [label=< >, ];
+ cp28 -> cp29 [label=<x = 3;>, ];
+ cp29 -> cp25 [label=<Exit >, ];
+ cp30 -> cp2 [label=<Exit y, z, w, a>, ];
+ cp31 -> cp32 [label=<Exit i>, ];
+ cp32 -> cp33 [label=<Exit >, ];
+ cp33 -> cp9 [label=<Exit >, ];
}
\ No newline at end of file
diff --git a/tests/misc/oracle/interpreted_automata_dataflow_forward.dot b/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
index 65c37595f4a46b8fde1a551920de17f3ecb8e92a..715c5beae70f84dfde5c5e293af5ab22b7f2c25f 100644
--- a/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
+++ b/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
@@ -4,77 +4,73 @@ digraph G {
cp1 [label=< >, ];
cp2 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp3 [label=< >, ];
- cp4 [label=<⊥>, style="dashed", ];
- cp5 [label=<y: 3>, ];
- cp6 [label=<y: 6>, ];
+ cp4 [label=<y: 3>, ];
+ cp5 [label=<y: 6>, ];
+ cp6 [label=<y: 6<br />z: 7>, ];
cp7 [label=<y: 6<br />z: 7>, ];
- cp8 [label=<y: 6<br />z: 7>, ];
- cp9 [label=<y: 6<br />z: 7<br />a: 1>, ];
- cp10 [label=<y: 6<br />z: 7>, ];
- cp11 [label=<y: 6<br />z: 7<br />a: 1>, ];
- cp12 [label=<⊥>, style="dashed", ];
- cp13 [label=<y: 6<br />z: 7<br />a: 1<br />i: 0>, ];
- cp14 [label=<y: 6<br />z: 7>, shape=invtriangle, ];
- cp15 [label=<y: 6<br />z: 7>, ];
- cp16 [label=<y: 6<br />z: 7<br />b: 3>, ];
+ cp8 [label=<y: 6<br />z: 7<br />a: 1>, ];
+ cp9 [label=<y: 6<br />z: 7>, ];
+ cp10 [label=<y: 6<br />z: 7<br />a: 1>, ];
+ cp11 [label=<⊥>, style="dashed", ];
+ cp12 [label=<y: 6<br />z: 7<br />a: 1<br />i: 0>, ];
+ cp13 [label=<y: 6<br />z: 7>, shape=invtriangle, ];
+ cp14 [label=<y: 6<br />z: 7>, ];
+ cp15 [label=<y: 6<br />z: 7<br />b: 3>, ];
+ cp16 [label=<y: 6<br />z: 7>, ];
cp17 [label=<y: 6<br />z: 7>, ];
cp18 [label=<y: 6<br />z: 7>, ];
cp19 [label=<y: 6<br />z: 7>, ];
- cp20 [label=<y: 6<br />z: 7>, ];
- cp21 [label=<⊥>, style="dashed", ];
+ cp20 [label=<y: 6<br />z: 7<br />b: 3>, ];
+ cp21 [label=<y: 6<br />z: 7>, ];
cp22 [label=<y: 6<br />z: 7<br />b: 3>, ];
- cp23 [label=<y: 6<br />z: 7>, ];
+ cp23 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp24 [label=<y: 6<br />z: 7<br />b: 3>, ];
- cp25 [label=<y: 6<br />z: 7<br />b: 3>, ];
- cp26 [label=<y: 6<br />z: 7<br />b: 3>, ];
+ cp25 [label=<x: 3<br />y: 6<br />z: 7>, ];
+ cp26 [label=<y: 6<br />z: 7>, ];
cp27 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp28 [label=<y: 6<br />z: 7>, ];
cp29 [label=<x: 3<br />y: 6<br />z: 7>, ];
- cp30 [label=<y: 6<br />z: 7>, ];
- cp31 [label=<x: 3<br />y: 6<br />z: 7>, ];
- cp32 [label=<x: 3<br />y: 6<br />z: 7>, ];
+ cp30 [label=<x: 3<br />y: 6<br />z: 7>, ];
+ cp31 [label=<y: 6<br />z: 7>, ];
+ cp32 [label=<y: 6<br />z: 7>, ];
cp33 [label=<y: 6<br />z: 7>, ];
- cp34 [label=<y: 6<br />z: 7>, ];
- cp35 [label=<y: 6<br />z: 7>, ];
- subgraph cluster_1 { cp26;cp25;cp24;cp23;cp22;cp18;cp17;cp16;cp15;cp14;
+ subgraph cluster_1 { cp24;cp23;cp22;cp21;cp20;cp17;cp16;cp15;cp14;cp13;
};
cp1 -> cp3 [label=<Enter y, z, w, a>, ];
- cp3 -> cp5 [label=<int y = 3;>, ];
- cp4 -> cp2 [label=<Exit y, z, w, a>, style="dashed", ];
- cp5 -> cp6 [label=<y *= 2;>, ];
- cp6 -> cp7 [label=<int z = y + 1;>, ];
- cp7 -> cp8 [label=<int w = y + x;>, ];
- cp8 -> cp9 [label=<int a = 1;>, ];
- cp9 -> cp11 [label=<Enter i>, ];
- cp10 -> cp28 [label=<x != 3>, ];
- cp10 -> cp29 [label=<!(x != 3)>, ];
- cp11 -> cp13 [label=<int i = 0;>, ];
- cp12 -> cp10 [label=<Exit i>, style="dashed", ];
- cp13 -> cp14 [label=< >, ];
- cp14 -> cp15 [label=<Enter >, ];
- cp15 -> cp18 [label=<i < 10>, ];
- cp15 -> cp19 [label=<!(i < 10)>, ];
- cp16 -> cp14 [constraint=false, label=<Exit >, ];
- cp17 -> cp23 [label=<Enter b, c>, ];
- cp18 -> cp17 [label=< >, ];
- cp19 -> cp20 [label=<Enter >, ];
- cp20 -> cp33 [label=< >, ];
- cp21 -> cp17 [label=<Exit >, style="dashed", ];
- cp22 -> cp16 [label=<i ++;>, ];
- cp23 -> cp25 [label=<int b = 3;>, ];
- cp24 -> cp22 [label=<Exit b, c>, ];
- cp25 -> cp26 [label=<int c = i + 1;>, ];
- cp26 -> cp24 [label=<a ++;>, ];
- cp27 -> cp32 [label=<return>, ];
- cp28 -> cp30 [label=<Enter >, ];
- cp29 -> cp27 [label=< >, ];
- cp30 -> cp31 [label=<x = 3;>, ];
- cp31 -> cp27 [label=<Exit >, ];
- cp32 -> cp2 [label=<Exit y, z, w, a>, ];
- cp33 -> cp34 [label=<Exit i>, ];
- cp34 -> cp35 [label=<Exit >, ];
- cp35 -> cp10 [label=<Exit >, ];
+ cp3 -> cp4 [label=<int y = 3;>, ];
+ cp4 -> cp5 [label=<y *= 2;>, ];
+ cp5 -> cp6 [label=<int z = y + 1;>, ];
+ cp6 -> cp7 [label=<int w = y + x;>, ];
+ cp7 -> cp8 [label=<int a = 1;>, ];
+ cp8 -> cp10 [label=<Enter i>, ];
+ cp9 -> cp26 [label=<x != 3>, ];
+ cp9 -> cp27 [label=<!(x != 3)>, ];
+ cp10 -> cp12 [label=<int i = 0;>, ];
+ cp11 -> cp9 [label=<Exit i>, style="dashed", ];
+ cp12 -> cp13 [label=< >, ];
+ cp13 -> cp14 [label=<Enter >, ];
+ cp14 -> cp17 [label=<i < 10>, ];
+ cp14 -> cp18 [label=<!(i < 10)>, ];
+ cp15 -> cp13 [constraint=false, label=<Exit >, ];
+ cp16 -> cp21 [label=<Enter b, c>, ];
+ cp17 -> cp16 [label=< >, ];
+ cp18 -> cp19 [label=<Enter >, ];
+ cp19 -> cp31 [label=< >, ];
+ cp20 -> cp15 [label=<i ++;>, ];
+ cp21 -> cp23 [label=<int b = 3;>, ];
+ cp22 -> cp20 [label=<Exit b, c>, ];
+ cp23 -> cp24 [label=<int c = i + 1;>, ];
+ cp24 -> cp22 [label=<a ++;>, ];
+ cp25 -> cp30 [label=<return>, ];
+ cp26 -> cp28 [label=<Enter >, ];
+ cp27 -> cp25 [label=< >, ];
+ cp28 -> cp29 [label=<x = 3;>, ];
+ cp29 -> cp25 [label=<Exit >, ];
+ cp30 -> cp2 [label=<Exit y, z, w, a>, ];
+ cp31 -> cp32 [label=<Exit i>, ];
+ cp32 -> cp33 [label=<Exit >, ];
+ cp33 -> cp9 [label=<Exit >, ];
}
\ No newline at end of file
diff --git a/tests/value/oracle/partitioning-interproc.0.res.oracle b/tests/value/oracle/partitioning-interproc.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4481fdb71c75b560b40d5f611f615da44aa446a3
--- /dev/null
+++ b/tests/value/oracle/partitioning-interproc.0.res.oracle
@@ -0,0 +1,62 @@
+[kernel] Parsing tests/value/partitioning-interproc.c (with preprocessing)
+[eva] Analyzing a complete application starting at cassign_test
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function cassign <- cassign_test.
+ Called from tests/value/partitioning-interproc.c:24.
+[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
+ Called from tests/value/partitioning-interproc.c:11.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for cassign
+[eva] Done for function cassign
+[eva] tests/value/partitioning-interproc.c:26: Frama_C_show_each: {1}
+[eva] tests/value/partitioning-interproc.c:30:
+ Reusing old results for call to cassign
+[eva] computing for function cassign <- cassign_test.
+ Called from tests/value/partitioning-interproc.c:30.
+[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
+ Called from tests/value/partitioning-interproc.c:11.
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for cassign
+[eva] Done for function cassign
+[eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
+[eva] Recording results for cassign_test
+[eva] done for function cassign_test
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function cassign:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ {0} or UNINITIALIZED
+ __retres ∈ {0; 1}
+[eva:final-states] Values at end of function cassign_test:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ {0} or UNINITIALIZED
+ y ∈ {1} or UNINITIALIZED
+[from] Computing for function cassign
+[from] Computing for function Frama_C_nondet <-cassign
+[from] Done for function Frama_C_nondet
+[from] Done for function cassign
+[from] Computing for function cassign_test
+[from] Done for function cassign_test
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_nondet:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; a; b
+[from] Function cassign:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ x FROM Frama_C_entropy_source; p (and SELF)
+ \result FROM Frama_C_entropy_source
+[from] Function cassign_test:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function cassign:
+ Frama_C_entropy_source; tmp; x; __retres
+[inout] Inputs for function cassign:
+ Frama_C_entropy_source
+[inout] Out (internal) for function cassign_test:
+ Frama_C_entropy_source; x; y; tmp; tmp_0
+[inout] Inputs for function cassign_test:
+ Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-interproc.1.res.oracle b/tests/value/oracle/partitioning-interproc.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dfd3684a60556eb5eb3f3103610e38cf700f7c6a
--- /dev/null
+++ b/tests/value/oracle/partitioning-interproc.1.res.oracle
@@ -0,0 +1,36 @@
+[kernel] Parsing tests/value/partitioning-interproc.c (with preprocessing)
+[eva] Analyzing a complete application starting at fabs_test
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function fabs <- fabs_test.
+ Called from tests/value/partitioning-interproc.c:50.
+[eva] Recording results for fabs
+[eva] Done for function fabs
+[eva] Recording results for fabs_test
+[eva] done for function fabs_test
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function fabs:
+ __retres ∈ [-0. .. 1.79769313486e+308]
+[eva:final-states] Values at end of function fabs_test:
+ x ∈ [-1. .. 1.]
+[from] Computing for function fabs
+[from] Done for function fabs
+[from] Computing for function fabs_test
+[from] Done for function fabs_test
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function fabs:
+ \result FROM x
+[from] Function fabs_test:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function fabs:
+ __retres
+[inout] Inputs for function fabs:
+ \nothing
+[inout] Out (internal) for function fabs_test:
+ x; tmp
+[inout] Inputs for function fabs_test:
+ \nothing
diff --git a/tests/value/oracle/partitioning-interproc.2.res.oracle b/tests/value/oracle/partitioning-interproc.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..25cdbcbd6200484db29211b2522b308cd086c023
--- /dev/null
+++ b/tests/value/oracle/partitioning-interproc.2.res.oracle
@@ -0,0 +1,36 @@
+[kernel] Parsing tests/value/partitioning-interproc.c (with preprocessing)
+[eva] Analyzing a complete application starting at fabs_splits_test
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function fabs_splits <- fabs_splits_test.
+ Called from tests/value/partitioning-interproc.c:71.
+[eva] Recording results for fabs_splits
+[eva] Done for function fabs_splits
+[eva] Recording results for fabs_splits_test
+[eva] done for function fabs_splits_test
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function fabs_splits:
+ __retres ∈ [0. .. 1.79769313486e+308]
+[eva:final-states] Values at end of function fabs_splits_test:
+ x ∈ [-1. .. 1.]
+[from] Computing for function fabs_splits
+[from] Done for function fabs_splits
+[from] Computing for function fabs_splits_test
+[from] Done for function fabs_splits_test
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function fabs_splits:
+ \result FROM x
+[from] Function fabs_splits_test:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function fabs_splits:
+ __retres
+[inout] Inputs for function fabs_splits:
+ \nothing
+[inout] Out (internal) for function fabs_splits_test:
+ x; tmp
+[inout] Inputs for function fabs_splits_test:
+ \nothing
diff --git a/tests/value/oracle/partitioning-interproc.res.oracle b/tests/value/oracle/partitioning-interproc.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b7f81ec5b367882ea010952fffc47aeae9e2d5c2
--- /dev/null
+++ b/tests/value/oracle/partitioning-interproc.res.oracle
@@ -0,0 +1,62 @@
+[kernel] Parsing tests/value/partitioning-interproc.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function conditional_assign <- main.
+ Called from tests/value/partitioning-interproc.c:23.
+[eva] computing for function Frama_C_nondet <- conditional_assign <- main.
+ Called from tests/value/partitioning-interproc.c:10.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for conditional_assign
+[eva] Done for function conditional_assign
+[eva] tests/value/partitioning-interproc.c:25: Frama_C_show_each: {1}
+[eva] tests/value/partitioning-interproc.c:29:
+ Reusing old results for call to conditional_assign
+[eva] computing for function conditional_assign <- main.
+ Called from tests/value/partitioning-interproc.c:29.
+[eva] computing for function Frama_C_nondet <- conditional_assign <- main.
+ Called from tests/value/partitioning-interproc.c:10.
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for conditional_assign
+[eva] Done for function conditional_assign
+[eva] tests/value/partitioning-interproc.c:31: Frama_C_show_each: {1}
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function conditional_assign:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ {0} or UNINITIALIZED
+ __retres ∈ {0; 1}
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ {0} or UNINITIALIZED
+ y ∈ {1} or UNINITIALIZED
+[from] Computing for function conditional_assign
+[from] Computing for function Frama_C_nondet <-conditional_assign
+[from] Done for function Frama_C_nondet
+[from] Done for function conditional_assign
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_nondet:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; a; b
+[from] Function conditional_assign:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ x FROM Frama_C_entropy_source; p (and SELF)
+ \result FROM Frama_C_entropy_source
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function conditional_assign:
+ Frama_C_entropy_source; tmp; x; __retres
+[inout] Inputs for function conditional_assign:
+ Frama_C_entropy_source
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; x; y; tmp; tmp_0
+[inout] Inputs for function main:
+ Frama_C_entropy_source
diff --git a/tests/value/oracle_apron/partitioning-interproc.0.res.oracle b/tests/value/oracle_apron/partitioning-interproc.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e64c57f27312171ca2f44caf1d8123951bdc7206
--- /dev/null
+++ b/tests/value/oracle_apron/partitioning-interproc.0.res.oracle
@@ -0,0 +1,11 @@
+16,17c16,22
+< [eva] tests/value/partitioning-interproc.c:30:
+< Reusing old results for call to cassign
+---
+> [eva] computing for function cassign <- cassign_test.
+> Called from tests/value/partitioning-interproc.c:30.
+> [eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
+> Called from tests/value/partitioning-interproc.c:11.
+> [eva] Done for function Frama_C_nondet
+> [eva] Recording results for cassign
+> [eva] Done for function cassign
diff --git a/tests/value/partitioning-interproc.c b/tests/value/partitioning-interproc.c
new file mode 100644
index 0000000000000000000000000000000000000000..e4094424342e522149e90672f435887c25cfd652
--- /dev/null
+++ b/tests/value/partitioning-interproc.c
@@ -0,0 +1,74 @@
+/* run.config*
+
+ STDOPT: #"-main cassign_test -eva-partition-history 1 -eva-interprocedural-history"
+ STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-domains equality -eva-interprocedural-history"
+ STDOPT: #"-main fabs_splits_test -eva-partition-history 1 -eva-domains equality -eva-interprocedural-splits"
+ */
+#include "__fc_builtin.h"
+
+int cassign(int *p)
+{
+ if (Frama_C_nondet(0,1))
+ {
+ *p = 0;
+ return 1;
+ }
+
+ return 0;
+}
+
+void cassign_test(void) {
+ int x, y;
+
+ // First call
+ if (cassign(&x)) {
+ y = x + 1;
+ Frama_C_show_each(y);
+ }
+
+ // Second call with some MemExec hit
+ if (cassign(&x)) {
+ y = x + 1;
+ Frama_C_show_each(y);
+ }
+}
+
+
+double fabs(double x)
+{
+ if (x == 0.0) {
+ return 0.0;
+ } else if (x > 0.0) {
+ return x;
+ } else {
+ return -x;
+ }
+}
+
+void fabs_test(double x)
+{
+ if (fabs(x) > 1.0) {
+ x = x < 0 ? -1.0 : 1.0;
+ }
+}
+
+
+double fabs_splits(double x)
+{
+ //@ split x > 0.0;
+ //@ split x < 0.0;
+ if (x == 0.0) {
+ return 0.0;
+ } else if (x > 0.0) {
+ return x;
+ } else {
+ return -x;
+ }
+}
+
+void fabs_splits_test(double x)
+{
+ if (fabs_splits(x) > 1.0) {
+ x = x < 0 ? -1.0 : 1.0;
+ }
+}