diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
index c69d39414c1922c5e4d3bcdb9c8ff9d1f05e98e5..a569876861fcafa65028face7c822c4245bb6337 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
@@ -4,6 +4,8 @@
[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:543: Warning:
Neither code nor explicit terminates for function exit,
generating default clauses. See -generated-spec-* options for more info
+[wp] [Valid] Goal inconditional_exit_assigns_normal (Cfg) (Unreachable)
+[wp] [Valid] Goal inconditional_exit_ensures (Cfg) (Unreachable)
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function inconditional_exit
@@ -14,22 +16,7 @@ Prove: true.
------------------------------------------------------------
-Goal Post-condition (file issue-684-exit.c, line 4) in 'inconditional_exit':
-Prove: true.
-
-------------------------------------------------------------
-
Goal Exit-condition (file issue-684-exit.c, line 3) in 'inconditional_exit':
Prove: true.
------------------------------------------------------------
-
-Goal Assigns nothing in 'inconditional_exit':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns nothing in 'inconditional_exit':
-Prove: true.
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
index f78ed5d813b1ab1745fbb6f7e8a2eccd974536a0..4a867b0febd745bbf10801c5b394ac013d89f035 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
@@ -4,16 +4,16 @@
[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:543: Warning:
Neither code nor explicit terminates for function exit,
generating default clauses. See -generated-spec-* options for more info
+[wp] [Valid] Goal inconditional_exit_assigns_normal (Cfg) (Unreachable)
+[wp] [Valid] Goal inconditional_exit_ensures (Cfg) (Unreachable)
[wp] Warning: Missing RTE guards
-[wp] 5 goals scheduled
+[wp] 2 goals scheduled
[wp] [Valid] typed_inconditional_exit_terminates (Qed)
-[wp] [Valid] typed_inconditional_exit_ensures (Qed)
[wp] [Valid] typed_inconditional_exit_exits (Qed)
-[wp] [Valid] typed_inconditional_exit_assigns_exit (Qed)
-[wp] [Valid] typed_inconditional_exit_assigns_normal (Qed)
-[wp] Proved goals: 5 / 5
- Qed: 5
+[wp] Proved goals: 4 / 4
+ Unreachable: 2
+ Qed: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- inconditional_exit 5 - 5 100%
+ inconditional_exit 2 - 2 100%
------------------------------------------------------------
diff --git a/tests/libc/oracle/argz_c.res.oracle b/tests/libc/oracle/argz_c.res.oracle
index 5e0b1929b42c7aa9d766a2fbcef20238c149fbcb..21fe8e24b8a38363435af2d16775a8a65e0eb262 100644
--- a/tests/libc/oracle/argz_c.res.oracle
+++ b/tests/libc/oracle/argz_c.res.oracle
@@ -87,10 +87,6 @@
[eva] Done for function stpcpy
[eva] Recording results for argz_create
[eva] Done for function argz_create
-[eva] computing for function exit <- main.
- Called from argz_c.c:21.
-[eva] using specification for function exit
-[eva] Done for function exit
[eva] argz_c.c:22: assertion got status valid.
[eva] argz_c.c:23: Call to builtin free
[eva] argz_c.c:23: function free: precondition 'freeable' got status valid.
@@ -104,9 +100,6 @@
allocating variable __malloc_argz_create_sep_l208
[eva] Recording results for argz_create_sep
[eva] Done for function argz_create_sep
-[eva] computing for function exit <- main.
- Called from argz_c.c:26.
-[eva] Done for function exit
[eva] computing for function __FC_assert <- main.
Called from argz_c.c:27.
[eva] using specification for function __FC_assert
@@ -152,9 +145,6 @@
[eva] Done for function argz_append
[eva] Recording results for argz_add
[eva] Done for function argz_add
-[eva] computing for function exit <- main.
- Called from argz_c.c:31.
-[eva] Done for function exit
[eva] computing for function __FC_assert <- main.
Called from argz_c.c:32.
[eva] argz_c.c:32:
@@ -172,9 +162,6 @@
allocating variable __realloc_argz_add_sep_l299
[eva] Recording results for argz_add_sep
[eva] Done for function argz_add_sep
-[eva] computing for function exit <- main.
- Called from argz_c.c:34.
-[eva] Done for function exit
[eva] computing for function __FC_assert <- main.
Called from argz_c.c:35.
[eva] argz_c.c:35:
@@ -203,9 +190,6 @@
[eva] FRAMAC_SHARE/libc/argz.c:279: Call to builtin memcpy
[eva] Recording results for argz_append
[eva] Done for function argz_append
-[eva] computing for function exit <- main.
- Called from argz_c.c:39.
-[eva] Done for function exit
[eva] computing for function __FC_assert <- main.
Called from argz_c.c:40.
[eva] argz_c.c:40:
@@ -224,9 +208,6 @@
[eva] Done for function argz_append
[eva] Recording results for argz_add
[eva] Done for function argz_add
-[eva] computing for function exit <- main.
- Called from argz_c.c:42.
-[eva] Done for function exit
[eva] computing for function __FC_assert <- main.
Called from argz_c.c:43.
[eva] argz_c.c:43:
@@ -499,9 +480,6 @@
[eva] FRAMAC_SHARE/libc/argz.c:126: Call to builtin free
[eva] Recording results for argz_replace
[eva] Done for function argz_replace
-[eva] computing for function exit <- main.
- Called from argz_c.c:46.
-[eva] Done for function exit
[eva] computing for function __FC_assert <- main.
Called from argz_c.c:47.
[eva] argz_c.c:47:
@@ -601,9 +579,6 @@
function memmove: precondition 'valid_src' got status valid.
[eva] Recording results for argz_insert
[eva] Done for function argz_insert
-[eva] computing for function exit <- main.
- Called from argz_c.c:65.
-[eva] Done for function exit
[eva] computing for function __FC_assert <- main.
Called from argz_c.c:66.
[eva] argz_c.c:66:
@@ -628,6 +603,31 @@
[eva] Done for function argz_insert
[eva] computing for function exit <- main.
Called from argz_c.c:68.
+[eva] using specification for function exit
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from argz_c.c:65.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from argz_c.c:46.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from argz_c.c:42.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from argz_c.c:39.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from argz_c.c:34.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from argz_c.c:31.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from argz_c.c:26.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from argz_c.c:21.
[eva] Done for function exit
[eva] computing for function __FC_assert <- main.
Called from argz_c.c:69.
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 376bef4479ffc054eed551a7d9ed04e68ccf1524..1893865c64c11adc5ee8f5cddf57a0522ade6a2f 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -161,10 +161,6 @@
[eva] netdb_c.c:36:
function fprintf_va_1: precondition valid_read_string(format) got status valid.
[eva] Done for function fprintf_va_1
-[eva] computing for function exit <- main.
- Called from netdb_c.c:37.
-[eva] using specification for function exit
-[eva] Done for function exit
[eva] computing for function socket <- main.
Called from netdb_c.c:46.
[eva] using specification for function socket
@@ -189,6 +185,10 @@
[eva] Done for function fprintf_va_2
[eva] computing for function exit <- main.
Called from netdb_c.c:58.
+[eva] using specification for function exit
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from netdb_c.c:37.
[eva] Done for function exit
[eva] computing for function freeaddrinfo <- main.
Called from netdb_c.c:61.
diff --git a/tests/libc/oracle/search_h.res.oracle b/tests/libc/oracle/search_h.res.oracle
index 1737610be446fafaaf03fb7a1da4ca61e9d3426c..bb8778da14a3fe599f634d8e2e037ff49d23d30e 100644
--- a/tests/libc/oracle/search_h.res.oracle
+++ b/tests/libc/oracle/search_h.res.oracle
@@ -44,6 +44,8 @@
[eva:invalid-assigns] search_h.c:34:
Completely invalid destination for assigns clause *compar. Ignoring.
[eva] Done for function tsearch
+[eva:alarm] search_h.c:40: Warning:
+ out of bounds read. assert \valid_read((struct element **)node);
[eva] computing for function fprintf_va_1 <- main.
Called from search_h.c:36.
[eva] using specification for function fprintf_va_1
@@ -53,8 +55,6 @@
Called from search_h.c:38.
[eva] using specification for function exit
[eva] Done for function exit
-[eva:alarm] search_h.c:40: Warning:
- out of bounds read. assert \valid_read((struct element **)node);
[kernel:annot:missing-spec] search_h.c:46: Warning:
Neither code nor specification for function twalk,
generating default assigns. See -generated-spec-* options for more info
diff --git a/tests/libc/oracle/socket_h.res.oracle b/tests/libc/oracle/socket_h.res.oracle
index f122611b2afb78badbf78ebbc3f05e36b703268f..d19a86d1f49df0b6281ef306b0e3f9ace0bc4edf 100644
--- a/tests/libc/oracle/socket_h.res.oracle
+++ b/tests/libc/oracle/socket_h.res.oracle
@@ -8,10 +8,6 @@
Called from socket_h.c:7.
[eva] using specification for function socket
[eva] Done for function socket
-[eva] computing for function exit <- main.
- Called from socket_h.c:8.
-[eva] using specification for function exit
-[eva] Done for function exit
[eva] computing for function inet_addr <- main.
Called from socket_h.c:11.
[eva] using specification for function inet_addr
@@ -32,6 +28,10 @@
[eva] Done for function connect
[eva] computing for function exit <- main.
Called from socket_h.c:14.
+[eva] using specification for function exit
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from socket_h.c:8.
[eva] Done for function exit
[eva] computing for function getsockopt <- main.
Called from socket_h.c:18.
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index 45ebf20af8220b7e3871dddd1592c92f74c840d9..c5b9d81f0e7c1dde82f9da28885f425a9f42d3fe 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -18,16 +18,6 @@
Called from spawn_h.c:43.
[eva] using specification for function posix_spawn_file_actions_init
[eva] Done for function posix_spawn_file_actions_init
-[eva] computing for function perror <- main.
- Called from spawn_h.c:45.
-[eva] using specification for function perror
-[eva] spawn_h.c:45:
- function perror: precondition 'valid_string_s' got status valid.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:45.
-[eva] using specification for function exit
-[eva] Done for function exit
[kernel:annot:missing-spec] spawn_h.c:47: Warning:
Neither code nor specification for function posix_spawn_file_actions_addclose,
generating default assigns. See -generated-spec-* options for more info
@@ -35,14 +25,6 @@
Called from spawn_h.c:47.
[eva] using specification for function posix_spawn_file_actions_addclose
[eva] Done for function posix_spawn_file_actions_addclose
-[eva] computing for function perror <- main.
- Called from spawn_h.c:50.
-[eva] spawn_h.c:50:
- function perror: precondition 'valid_string_s' got status valid.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:50.
-[eva] Done for function exit
[kernel:annot:missing-spec] spawn_h.c:60: Warning:
Neither code nor specification for function posix_spawnattr_init,
generating default assigns. See -generated-spec-* options for more info
@@ -50,14 +32,6 @@
Called from spawn_h.c:60.
[eva] using specification for function posix_spawnattr_init
[eva] Done for function posix_spawnattr_init
-[eva] computing for function perror <- main.
- Called from spawn_h.c:62.
-[eva] spawn_h.c:62:
- function perror: precondition 'valid_string_s' got status valid.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:62.
-[eva] Done for function exit
[kernel:annot:missing-spec] spawn_h.c:63: Warning:
Neither code nor specification for function posix_spawnattr_setflags,
generating default assigns. See -generated-spec-* options for more info
@@ -65,14 +39,6 @@
Called from spawn_h.c:63.
[eva] using specification for function posix_spawnattr_setflags
[eva] Done for function posix_spawnattr_setflags
-[eva] computing for function perror <- main.
- Called from spawn_h.c:65.
-[eva] spawn_h.c:65:
- function perror: precondition 'valid_string_s' got status valid.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:65.
-[eva] Done for function exit
[eva] computing for function sigfillset <- main.
Called from spawn_h.c:67.
[eva] using specification for function sigfillset
@@ -86,14 +52,6 @@
Called from spawn_h.c:68.
[eva] using specification for function posix_spawnattr_setsigmask
[eva] Done for function posix_spawnattr_setsigmask
-[eva] computing for function perror <- main.
- Called from spawn_h.c:70.
-[eva] spawn_h.c:70:
- function perror: precondition 'valid_string_s' got status valid.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:70.
-[eva] Done for function exit
[eva] spawn_h.c:36: starting to merge loop iterations
[eva] computing for function getopt <- main.
Called from spawn_h.c:36.
@@ -101,39 +59,15 @@
[eva] computing for function posix_spawn_file_actions_init <- main.
Called from spawn_h.c:43.
[eva] Done for function posix_spawn_file_actions_init
-[eva] computing for function perror <- main.
- Called from spawn_h.c:45.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:45.
-[eva] Done for function exit
[eva] computing for function posix_spawn_file_actions_addclose <- main.
Called from spawn_h.c:47.
[eva] Done for function posix_spawn_file_actions_addclose
-[eva] computing for function perror <- main.
- Called from spawn_h.c:50.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:50.
-[eva] Done for function exit
[eva] computing for function posix_spawnattr_init <- main.
Called from spawn_h.c:60.
[eva] Done for function posix_spawnattr_init
-[eva] computing for function perror <- main.
- Called from spawn_h.c:62.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:62.
-[eva] Done for function exit
[eva] computing for function posix_spawnattr_setflags <- main.
Called from spawn_h.c:63.
[eva] Done for function posix_spawnattr_setflags
-[eva] computing for function perror <- main.
- Called from spawn_h.c:65.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:65.
-[eva] Done for function exit
[eva] computing for function sigfillset <- main.
Called from spawn_h.c:67.
[eva] Done for function sigfillset
@@ -141,11 +75,31 @@
Called from spawn_h.c:68.
[eva] Done for function posix_spawnattr_setsigmask
[eva] computing for function perror <- main.
- Called from spawn_h.c:70.
+ Called from spawn_h.c:45.
+[eva] using specification for function perror
+[eva] spawn_h.c:45:
+ function perror: precondition 'valid_string_s' got status valid.
[eva] Done for function perror
-[eva] computing for function exit <- main.
+[eva] computing for function perror <- main.
+ Called from spawn_h.c:50.
+[eva] spawn_h.c:50:
+ function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva] computing for function perror <- main.
+ Called from spawn_h.c:62.
+[eva] spawn_h.c:62:
+ function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva] computing for function perror <- main.
+ Called from spawn_h.c:65.
+[eva] spawn_h.c:65:
+ function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva] computing for function perror <- main.
Called from spawn_h.c:70.
-[eva] Done for function exit
+[eva] spawn_h.c:70:
+ function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
[eva:alarm] spawn_h.c:82: Warning:
out of bounds read. assert \valid_read(argv + optind);
[eva:garbled-mix:write] spawn_h.c:82:
@@ -162,9 +116,6 @@
[eva] spawn_h.c:85:
function perror: precondition 'valid_string_s' got status valid.
[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:85.
-[eva] Done for function exit
[kernel:annot:missing-spec] spawn_h.c:90: Warning:
Neither code nor specification for function posix_spawnattr_destroy,
generating default assigns. See -generated-spec-* options for more info
@@ -177,9 +128,6 @@
[eva] spawn_h.c:92:
function perror: precondition 'valid_string_s' got status valid.
[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:92.
-[eva] Done for function exit
[kernel:annot:missing-spec] spawn_h.c:96: Warning:
Neither code nor specification for function posix_spawn_file_actions_destroy,
generating default assigns. See -generated-spec-* options for more info
@@ -192,9 +140,6 @@
[eva] spawn_h.c:98:
function perror: precondition 'valid_string_s' got status valid.
[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:98.
-[eva] Done for function exit
[eva:alarm] spawn_h.c:101: Warning:
accessing uninitialized left-value. assert \initialized(&child_pid);
[eva] computing for function printf_va_1 <- main.
@@ -208,14 +153,6 @@
[eva] spawn_h.c:106:
function waitpid, behavior stat_loc_non_null: precondition 'valid_stat_loc' got status valid.
[eva] Done for function waitpid
-[eva] computing for function perror <- main.
- Called from spawn_h.c:108.
-[eva] spawn_h.c:108:
- function perror: precondition 'valid_string_s' got status valid.
-[eva] Done for function perror
-[eva] computing for function exit <- main.
- Called from spawn_h.c:108.
-[eva] Done for function exit
[eva] computing for function printf_va_2 <- main.
Called from spawn_h.c:110.
[eva] using specification for function printf_va_2
@@ -247,9 +184,42 @@
[eva] computing for function waitpid <- main.
Called from spawn_h.c:106.
[eva] Done for function waitpid
+[eva] computing for function perror <- main.
+ Called from spawn_h.c:108.
+[eva] spawn_h.c:108:
+ function perror: precondition 'valid_string_s' got status valid.
+[eva] Done for function perror
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:108.
+[eva] using specification for function exit
+[eva] Done for function exit
[eva] computing for function exit <- main.
Called from spawn_h.c:122.
[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:98.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:92.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:85.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:70.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:65.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:62.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:50.
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from spawn_h.c:45.
+[eva] Done for function exit
[eva] Recording results for main
[eva] Done for function main
[eva:garbled-mix:summary]
diff --git a/tests/libc/oracle/stdnoreturn_h.res.oracle b/tests/libc/oracle/stdnoreturn_h.res.oracle
index 2ffebd78e3f0208e367ade7e64dd7dbed4b28371..84361dfd8110ebe400ee64166cb843ebdae1822f 100644
--- a/tests/libc/oracle/stdnoreturn_h.res.oracle
+++ b/tests/libc/oracle/stdnoreturn_h.res.oracle
@@ -4,14 +4,14 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
-[eva] computing for function f <- main.
- Called from stdnoreturn_h.c:18.
-[eva] Recording results for f
-[eva] Done for function f
[eva] computing for function g <- main.
Called from stdnoreturn_h.c:19.
[eva] Recording results for g
[eva] Done for function g
+[eva] computing for function f <- main.
+ Called from stdnoreturn_h.c:18.
+[eva] Recording results for f
+[eva] Done for function f
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/sys_select.res.oracle b/tests/libc/oracle/sys_select.res.oracle
index 99b776af8457627f82eda3ca5fcd93eb5bdee8b7..17aef2c88e155c5ed0021923305a8e5d39e00f23 100644
--- a/tests/libc/oracle/sys_select.res.oracle
+++ b/tests/libc/oracle/sys_select.res.oracle
@@ -8,10 +8,6 @@
Called from sys_select.c:9.
[eva] using specification for function socket
[eva] Done for function socket
-[eva] computing for function exit <- main.
- Called from sys_select.c:10.
-[eva] using specification for function exit
-[eva] Done for function exit
[eva] sys_select.c:16: Call to builtin memset
[eva] sys_select.c:16: function memset: precondition 'valid_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:151:
@@ -34,6 +30,10 @@
[eva] Done for function bind
[eva] computing for function exit <- main.
Called from sys_select.c:21.
+[eva] using specification for function exit
+[eva] Done for function exit
+[eva] computing for function exit <- main.
+ Called from sys_select.c:10.
[eva] Done for function exit
[eva] computing for function FD_ZERO <- main.
Called from sys_select.c:22.
diff --git a/tests/misc/oracle/interpreted_automata_dataflow_backward.dot b/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
index 99f06648f6e429f3618551c663ac9fd6b3d33fcf..f51d2851fbc0cb51fbdb32e0edbc5a74d41909e9 100644
--- a/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
+++ b/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
@@ -5,72 +5,72 @@ digraph G {
cp2 [label=< >, ];
cp3 [label=< >, ];
cp4 [label=<x, a, i>, ];
- cp5 [label=<x>, ];
+ cp5 [label=<x, a>, ];
cp6 [label=<x>, ];
cp7 [label=<x>, ];
- cp8 [label=<x>, ];
+ cp8 [label=<x, a>, ];
cp9 [label=< >, ];
- cp10 [label=<x, y>, ];
- cp11 [label=< >, ];
- cp12 [label=<x, a, i>, ];
- cp13 [label=< >, ];
- cp14 [label=<x, a, i>, ];
+ cp10 [label=<x>, ];
+ cp11 [label=<x>, ];
+ cp12 [label=< >, ];
+ cp13 [label=<x, a, i>, ];
+ cp14 [label=< >, ];
cp15 [label=<x>, ];
- cp16 [label=<x, a>, ];
+ cp16 [label=< >, ];
cp17 [label=<x>, ];
- cp18 [label=< >, ];
+ cp18 [label=<x>, ];
cp19 [label=< >, ];
cp20 [label=<x, a, i>, ];
cp21 [label=<x, a, i>, ];
- cp22 [label=<x, y>, ];
- cp23 [label=<x, a, i>, ];
- cp24 [label=<x, y>, ];
- cp25 [label=<x>, ];
+ cp22 [label=<x, a, i>, ];
+ cp23 [label=<x, y>, ];
+ cp24 [label=<x, a, i>, shape=invtriangle, ];
+ cp25 [label=<x, y>, ];
cp26 [label=<x>, ];
- cp27 [label=<x, a, i>, ];
- cp28 [label=<x, a, i>, shape=invtriangle, ];
- cp29 [label=<x>, ];
+ cp27 [label=<x>, ];
+ cp28 [label=<x, a, i>, ];
+ cp29 [label=<x, a, i>, ];
cp30 [label=<x, a, i>, ];
- cp31 [label=<x, a>, ];
+ cp31 [label=<x, a, i>, ];
cp32 [label=<x>, ];
- cp33 [label=<x, a, i>, ];
+ cp33 [label=<x, y>, ];
- subgraph cluster_1 { cp33;cp30;cp28;cp27;cp23;cp21;cp20;cp12;cp4;cp1;
+ subgraph cluster_1 { cp31;cp30;cp29;cp28;cp24;cp22;cp21;cp20;cp13;cp4;
};
- cp1 -> cp28 [constraint=false, label=<Enter >, ];
- cp2 -> cp19 [label=<Exit >, ];
- cp3 -> cp9 [label=<Enter >, ];
- cp4 -> cp20 [label=<a ++;>, ];
- cp5 -> cp8 [label=<Exit i>, ];
- cp6 -> cp8 [label=<Exit >, ];
- cp7 -> cp15 [label=< >, ];
- cp8 -> cp3 [label=<x != 3>, ];
- cp8 -> cp11 [label=<!(x != 3)>, ];
- cp9 -> cp2 [label=<x = 3;>, ];
- cp10 -> cp24 [label=<y *= 2;>, ];
- cp11 -> cp19 [label=< >, ];
- cp12 -> cp21 [label=<Enter b, c>, ];
- cp14 -> cp1 [label=< >, ];
- cp15 -> cp25 [label=<Exit i>, ];
- cp16 -> cp14 [label=<int i = 0;>, ];
- cp17 -> cp29 [label=<Enter y, z, w, a>, ];
- cp18 -> cp13 [label=<Exit y, z, w, a>, ];
- cp19 -> cp18 [label=<return>, ];
- cp20 -> cp33 [label=<Exit b, c>, ];
- cp21 -> cp30 [label=<int b = 3;>, ];
- cp22 -> cp32 [label=<int w = y + x;>, ];
- cp23 -> cp1 [label=<Exit >, ];
- cp24 -> cp22 [label=<int z = y + 1;>, ];
- cp25 -> cp6 [label=<Exit >, ];
- cp26 -> cp7 [label=<Enter >, ];
- cp27 -> cp12 [label=< >, ];
- cp28 -> cp27 [label=<i < 10>, ];
- cp28 -> cp26 [label=<!(i < 10)>, ];
- cp29 -> cp10 [label=<int y = 3;>, ];
- cp30 -> cp4 [label=<int c = i + 1;>, ];
- cp31 -> cp16 [label=<Enter i>, ];
- cp32 -> cp31 [label=<int a = 1;>, ];
- cp33 -> cp23 [label=<i ++;>, ];
+ cp1 -> cp30 [label=< >, ];
+ cp2 -> cp19 [label=<x = 3;>, ];
+ cp3 -> cp16 [label=<return>, ];
+ cp4 -> cp20 [label=<int c = i + 1;>, ];
+ cp5 -> cp1 [label=<int i = 0;>, ];
+ cp6 -> cp10 [label=<Exit >, ];
+ cp7 -> cp26 [label=<Enter >, ];
+ cp8 -> cp5 [label=<Enter i>, ];
+ cp9 -> cp3 [label=< >, ];
+ cp10 -> cp17 [label=<Exit >, ];
+ cp11 -> cp25 [label=<int y = 3;>, ];
+ cp12 -> cp2 [label=<Enter >, ];
+ cp13 -> cp30 [label=<Exit >, ];
+ cp15 -> cp17 [label=<Exit i>, ];
+ cp16 -> cp14 [label=<Exit y, z, w, a>, ];
+ cp17 -> cp12 [label=<x != 3>, ];
+ cp17 -> cp9 [label=<!(x != 3)>, ];
+ cp18 -> cp11 [label=<Enter y, z, w, a>, ];
+ cp19 -> cp3 [label=<Exit >, ];
+ cp20 -> cp31 [label=<a ++;>, ];
+ cp21 -> cp4 [label=<int b = 3;>, ];
+ cp22 -> cp13 [label=<i ++;>, ];
+ cp23 -> cp33 [label=<int z = y + 1;>, ];
+ cp24 -> cp28 [label=<i < 10>, ];
+ cp24 -> cp7 [label=<!(i < 10)>, ];
+ cp25 -> cp23 [label=<y *= 2;>, ];
+ cp26 -> cp27 [label=< >, ];
+ cp27 -> cp6 [label=<Exit i>, ];
+ cp28 -> cp29 [label=< >, ];
+ cp29 -> cp21 [label=<Enter b, c>, ];
+ cp30 -> cp24 [constraint=false, label=<Enter >, ];
+ cp31 -> cp22 [label=<Exit b, c>, ];
+ cp32 -> cp8 [label=<int a = 1;>, ];
+ cp33 -> cp32 [label=<int w = y + x;>, ];
}
diff --git a/tests/misc/oracle/interpreted_automata_dataflow_forward.dot b/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
index 57834ef539166eac084da62b4a8825b7b2e741d7..5bd76740068fd18bfee8b58df814c6e95ef6d59c 100644
--- a/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
+++ b/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
@@ -1,76 +1,76 @@
digraph G {
fontname="fixed";
node [shape=circle, ];
- cp1 [label=<y: 6<br />z: 7>, shape=invtriangle, ];
- cp2 [label=<x: 3<br />y: 6<br />z: 7>, ];
- cp3 [label=<y: 6<br />z: 7>, ];
+ cp1 [label=<y: 6<br />z: 7<br />a: 1<br />i: 0>, ];
+ cp2 [label=<y: 6<br />z: 7>, ];
+ cp3 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp4 [label=<y: 6<br />z: 7<br />b: 3>, ];
- cp5 [label=<⊥>, style="dashed", ];
+ cp5 [label=<y: 6<br />z: 7<br />a: 1>, ];
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>, ];
- cp10 [label=<y: 3>, ];
- cp11 [label=<x: 3<br />y: 6<br />z: 7>, ];
+ cp8 [label=<y: 6<br />z: 7<br />a: 1>, ];
+ cp9 [label=<x: 3<br />y: 6<br />z: 7>, ];
+ cp10 [label=<y: 6<br />z: 7>, ];
+ cp11 [label=< >, ];
cp12 [label=<y: 6<br />z: 7>, ];
- cp13 [label=<x: 3<br />y: 6<br />z: 7>, ];
- cp14 [label=<y: 6<br />z: 7<br />a: 1<br />i: 0>, ];
- cp15 [label=<y: 6<br />z: 7>, ];
- cp16 [label=<y: 6<br />z: 7<br />a: 1>, ];
- cp17 [label=< >, ];
- cp18 [label=<x: 3<br />y: 6<br />z: 7>, ];
+ cp13 [label=<y: 6<br />z: 7<br />b: 3>, ];
+ cp14 [label=<x: 3<br />y: 6<br />z: 7>, ];
+ cp15 [label=<⊥>, style="dashed", ];
+ cp16 [label=<x: 3<br />y: 6<br />z: 7>, ];
+ cp17 [label=<y: 6<br />z: 7>, ];
+ cp18 [label=< >, ];
cp19 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp20 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp21 [label=<y: 6<br />z: 7>, ];
- cp22 [label=<y: 6<br />z: 7>, ];
- cp23 [label=<y: 6<br />z: 7<br />b: 3>, ];
- cp24 [label=<y: 6>, ];
- cp25 [label=<y: 6<br />z: 7>, ];
+ cp22 [label=<y: 6<br />z: 7<br />b: 3>, ];
+ cp23 [label=<y: 6>, ];
+ cp24 [label=<y: 6<br />z: 7>, ];
+ cp25 [label=<y: 3>, ];
cp26 [label=<y: 6<br />z: 7>, ];
cp27 [label=<y: 6<br />z: 7>, ];
cp28 [label=<y: 6<br />z: 7>, ];
- cp29 [label=< >, ];
- cp30 [label=<y: 6<br />z: 7<br />b: 3>, ];
- cp31 [label=<y: 6<br />z: 7<br />a: 1>, ];
+ cp29 [label=<y: 6<br />z: 7>, ];
+ cp30 [label=<y: 6<br />z: 7>, shape=invtriangle, ];
+ cp31 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp32 [label=<y: 6<br />z: 7>, ];
- cp33 [label=<y: 6<br />z: 7<br />b: 3>, ];
+ cp33 [label=<y: 6<br />z: 7>, ];
- subgraph cluster_1 { cp33;cp30;cp28;cp27;cp23;cp21;cp20;cp12;cp4;cp1;
+ subgraph cluster_1 { cp31;cp30;cp29;cp28;cp24;cp22;cp21;cp20;cp13;cp4;
};
- cp1 -> cp28 [label=<Enter >, ];
- cp2 -> cp19 [label=<Exit >, ];
- cp3 -> cp9 [label=<Enter >, ];
- cp4 -> cp20 [label=<a ++;>, ];
- cp5 -> cp8 [label=<Exit i>, style="dashed", ];
- cp6 -> cp8 [label=<Exit >, ];
- cp7 -> cp15 [label=< >, ];
- cp8 -> cp3 [label=<x != 3>, ];
- cp8 -> cp11 [label=<!(x != 3)>, ];
- cp9 -> cp2 [label=<x = 3;>, ];
- cp10 -> cp24 [label=<y *= 2;>, ];
- cp11 -> cp19 [label=< >, ];
- cp12 -> cp21 [label=<Enter b, c>, ];
- cp14 -> cp1 [label=< >, ];
- cp15 -> cp25 [label=<Exit i>, ];
- cp16 -> cp14 [label=<int i = 0;>, ];
- cp17 -> cp29 [label=<Enter y, z, w, a>, ];
- cp18 -> cp13 [label=<Exit y, z, w, a>, ];
- cp19 -> cp18 [label=<return>, ];
- cp20 -> cp33 [label=<Exit b, c>, ];
- cp21 -> cp30 [label=<int b = 3;>, ];
- cp22 -> cp32 [label=<int w = y + x;>, ];
- cp23 -> cp1 [constraint=false, label=<Exit >, ];
- cp24 -> cp22 [label=<int z = y + 1;>, ];
- cp25 -> cp6 [label=<Exit >, ];
- cp26 -> cp7 [label=<Enter >, ];
- cp27 -> cp12 [label=< >, ];
- cp28 -> cp27 [label=<i < 10>, ];
- cp28 -> cp26 [label=<!(i < 10)>, ];
- cp29 -> cp10 [label=<int y = 3;>, ];
- cp30 -> cp4 [label=<int c = i + 1;>, ];
- cp31 -> cp16 [label=<Enter i>, ];
- cp32 -> cp31 [label=<int a = 1;>, ];
- cp33 -> cp23 [label=<i ++;>, ];
+ cp1 -> cp30 [label=< >, ];
+ cp2 -> cp19 [label=<x = 3;>, ];
+ cp3 -> cp16 [label=<return>, ];
+ cp4 -> cp20 [label=<int c = i + 1;>, ];
+ cp5 -> cp1 [label=<int i = 0;>, ];
+ cp6 -> cp10 [label=<Exit >, ];
+ cp7 -> cp26 [label=<Enter >, ];
+ cp8 -> cp5 [label=<Enter i>, ];
+ cp9 -> cp3 [label=< >, ];
+ cp10 -> cp17 [label=<Exit >, ];
+ cp11 -> cp25 [label=<int y = 3;>, ];
+ cp12 -> cp2 [label=<Enter >, ];
+ cp13 -> cp30 [constraint=false, label=<Exit >, ];
+ cp15 -> cp17 [label=<Exit i>, style="dashed", ];
+ cp16 -> cp14 [label=<Exit y, z, w, a>, ];
+ cp17 -> cp12 [label=<x != 3>, ];
+ cp17 -> cp9 [label=<!(x != 3)>, ];
+ cp18 -> cp11 [label=<Enter y, z, w, a>, ];
+ cp19 -> cp3 [label=<Exit >, ];
+ cp20 -> cp31 [label=<a ++;>, ];
+ cp21 -> cp4 [label=<int b = 3;>, ];
+ cp22 -> cp13 [label=<i ++;>, ];
+ cp23 -> cp33 [label=<int z = y + 1;>, ];
+ cp24 -> cp28 [label=<i < 10>, ];
+ cp24 -> cp7 [label=<!(i < 10)>, ];
+ cp25 -> cp23 [label=<y *= 2;>, ];
+ cp26 -> cp27 [label=< >, ];
+ cp27 -> cp6 [label=<Exit i>, ];
+ cp28 -> cp29 [label=< >, ];
+ cp29 -> cp21 [label=<Enter b, c>, ];
+ cp30 -> cp24 [label=<Enter >, ];
+ cp31 -> cp22 [label=<Exit b, c>, ];
+ cp32 -> cp8 [label=<int a = 1;>, ];
+ cp33 -> cp32 [label=<int w = y + x;>, ];
}
diff --git a/tests/value/oracle/noreturn.res.oracle b/tests/value/oracle/noreturn.res.oracle
index 304917afda22a9fb33e394f22e87e5f9731a32a4..9ac52f56318df28adda9ac3b68bd9675a5dd2a83 100644
--- a/tests/value/oracle/noreturn.res.oracle
+++ b/tests/value/oracle/noreturn.res.oracle
@@ -16,13 +16,20 @@
Called from noreturn.i:28.
[eva] Recording results for warn_never_ends
[eva] Done for function warn_never_ends
-[kernel:annot:missing-spec] noreturn.i:29: Warning:
- Neither code nor specification for function stop,
- generating default assigns. See -generated-spec-* options for more info
-[eva] computing for function stop <- main.
- Called from noreturn.i:29.
-[eva] using specification for function stop
-[eva] Done for function stop
+[eva] computing for function should_never_end <- main.
+ Called from noreturn.i:33.
+[eva] Recording results for should_never_end
+[eva] Done for function should_never_end
+[eva] computing for function should_never_end <- main.
+ Called from noreturn.i:32.
+[eva] Recording results for should_never_end
+[eva] noreturn.i:32: Warning:
+ function should_never_end may terminate but has the noreturn attribute
+[eva] Done for function should_never_end
+[eva] computing for function never_ends <- main.
+ Called from noreturn.i:31.
+[eva] Recording results for never_ends
+[eva] Done for function never_ends
[kernel:annot:missing-spec] noreturn.i:30: Warning:
Neither code nor specification for function haltme,
generating default assigns. See -generated-spec-* options for more info
@@ -30,20 +37,13 @@
Called from noreturn.i:30.
[eva] using specification for function haltme
[eva] Done for function haltme
-[eva] computing for function never_ends <- main.
- Called from noreturn.i:31.
-[eva] Recording results for never_ends
-[eva] Done for function never_ends
-[eva] computing for function should_never_end <- main.
- Called from noreturn.i:32.
-[eva] Recording results for should_never_end
-[eva] noreturn.i:32: Warning:
- function should_never_end may terminate but has the noreturn attribute
-[eva] Done for function should_never_end
-[eva] computing for function should_never_end <- main.
- Called from noreturn.i:33.
-[eva] Recording results for should_never_end
-[eva] Done for function should_never_end
+[kernel:annot:missing-spec] noreturn.i:29: Warning:
+ Neither code nor specification for function stop,
+ generating default assigns. See -generated-spec-* options for more info
+[eva] computing for function stop <- main.
+ Called from noreturn.i:29.
+[eva] using specification for function stop
+[eva] Done for function stop
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle_gauges/noreturn.res.oracle b/tests/value/oracle_gauges/noreturn.res.oracle
index 6847a2f3eb44f61eb5031e2ab2f61d8339975bbe..7851d62f17e233ddfd4cce1e689a538c3c8bee52 100644
--- a/tests/value/oracle_gauges/noreturn.res.oracle
+++ b/tests/value/oracle_gauges/noreturn.res.oracle
@@ -2,7 +2,7 @@
> [eva] noreturn.i:20: starting to merge loop iterations
16a18
> [eva] noreturn.i:16: starting to merge loop iterations
-34a37
-> [eva] noreturn.i:7: starting to merge loop iterations
-38a42
+20a23
> [eva] noreturn.i:13: starting to merge loop iterations
+30a34
+> [eva] noreturn.i:7: starting to merge loop iterations