Update test oracles

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.
-
-------------------------------------------------------------

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%
 ------------------------------------------------------------

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.

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.

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

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.

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] 

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 ======

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.

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 &lt; 10>, ];
-  cp28 -> cp26 [label=<!(i &lt; 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 &lt; 10>, ];
+  cp24 -> cp7 [label=<!(i &lt; 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;>, ];
   
   }

tests/misc/oracle/interpreted_automata_dataflow_forward.dot

 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 &lt; 10>, ];
-  cp28 -> cp26 [label=<!(i &lt; 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 &lt; 10>, ];
+  cp24 -> cp7 [label=<!(i &lt; 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;>, ];
   
   }

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 ======

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