From 3179009d2ac32de8dc7323a4578b0bba19fba88d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 9 Oct 2024 18:23:35 +0200
Subject: [PATCH] [region] use memoized domain

---
 src/plugins/region/Region.ml                  |   2 +-
 src/plugins/region/analysis.ml                |  10 -
 src/plugins/region/register.ml                |  15 +-
 .../tests/wp_region/oracle/array.res.oracle   | 360 ------------------
 .../wp_region/oracle/copy_array.res.oracle    | 288 --------------
 .../oracle/heterogenous_cast.res.oracle       |  44 ---
 .../tests/wp_region/oracle/record.res.oracle  | 107 ------
 .../tests/wp_region/oracle/union.res.oracle   |  48 ---
 .../wp_region/oracle_qualif/array.res.oracle  | 360 ------------------
 .../oracle_qualif/copy_array.res.oracle       | 288 --------------
 .../heterogenous_cast.res.oracle              |  44 ---
 .../wp_region/oracle_qualif/record.res.oracle | 107 ------
 .../wp_region/oracle_qualif/union.res.oracle  |  48 ---
 13 files changed, 15 insertions(+), 1706 deletions(-)

diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index f7b06282251..7a885301254 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -26,7 +26,7 @@
 
 type map = Memory.map
 type node = Memory.node
-let map kf = (Code.domain kf).map
+let map kf = (Analysis.get kf).map
 let id n = Memory.id n
 let uid m n = Memory.id @@ Memory.node m n
 let iter = Memory.iter
diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml
index 252bb026bd0..8fd275216e3 100644
--- a/src/plugins/region/analysis.ml
+++ b/src/plugins/region/analysis.ml
@@ -56,16 +56,6 @@ let get kf =
     Options.feedback ~ontty:`Transient "Function %a…" Kernel_function.pretty kf ;
     let domain = Code.domain kf in
     STATE.add kf domain ;
-    Options.result "@[<v 2>Function %a:%t@]@."
-      Kernel_function.pretty kf
-      begin fun fmt ->
-        List.iter
-          begin fun r ->
-            Format.pp_print_newline fmt () ;
-            Memory.pp_region fmt r ;
-          end @@
-        Memory.regions domain.map
-      end ;
     domain
 
 let compute kf = ignore @@ get kf
diff --git a/src/plugins/region/register.ml b/src/plugins/region/register.ml
index 54cd5cdd62b..0d904f9fd3e 100644
--- a/src/plugins/region/register.ml
+++ b/src/plugins/region/register.ml
@@ -31,7 +31,20 @@ let main () =
     begin
       Ast.compute () ;
       R.feedback "Analyzing regions" ;
-      Globals.Functions.iter Analysis.compute ;
+      Globals.Functions.iter
+        begin fun kf ->
+          let domain = Analysis.get kf in
+          Options.result "@[<v 2>Function %a:%t@]@."
+            Kernel_function.pretty kf
+            begin fun fmt ->
+              List.iter
+                begin fun r ->
+                  Format.pp_print_newline fmt () ;
+                  Memory.pp_region fmt r ;
+                end @@
+              Memory.regions domain.map
+            end
+        end
     end
 
 let () = Boot.Main.extend main
diff --git a/src/plugins/wp/tests/wp_region/oracle/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
index 6fd76bcdc0e..1c937abfbab 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
@@ -6,366 +6,6 @@
 [wp] Warning: Missing RTE guards
 [region] array.c:23: Warning: Annotations not analyzed
 [region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function add_first4
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
index b50ed95f5a1..75bce10e980 100644
--- a/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
@@ -7,294 +7,6 @@
 [region] copy_array.c:15: Warning: Annotations not analyzed
 [region] copy_array.c:18: Warning: Annotations not analyzed
 [region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function copy
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
index f7b3f9e10a0..a6a8f41e11a 100644
--- a/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
@@ -5,50 +5,6 @@
 [wp] [Valid] Goal g_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function g
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/record.res.oracle b/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
index 7ba53f1df82..721829172e9 100644
--- a/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
@@ -5,113 +5,6 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function f
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/union.res.oracle b/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
index 87cfc66c455..7023fcc52f2 100644
--- a/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
@@ -5,54 +5,6 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function f
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
index 132cfb8a7b3..6162ad43a5a 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
@@ -6,366 +6,6 @@
 [wp] Warning: Missing RTE guards
 [region] array.c:23: Warning: Annotations not analyzed
 [region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
 [wp] 6 goals scheduled
 [wp] [Valid] region_add_first4_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_add_first4_ensures_2 (Qed)
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
index 7071946431d..87119772a2e 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
@@ -7,294 +7,6 @@
 [region] copy_array.c:15: Warning: Annotations not analyzed
 [region] copy_array.c:18: Warning: Annotations not analyzed
 [region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
 [wp] 13 goals scheduled
 [wp] [Valid] region_copy_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_copy_loop_invariant_Copy_preserved (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
index 5ef48e91de1..cc19d2134ab 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
@@ -5,50 +5,6 @@
 [wp] [Valid] Goal g_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
 [wp] 4 goals scheduled
 [wp] [Valid] region_g_assert (Alt-Ergo) (Cached)
 [wp] [Valid] region_g_assigns_part1 (Qed)
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
index cc8d40d8228..166e787cf3e 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
@@ -5,113 +5,6 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
 [wp] 4 goals scheduled
 [wp] [Valid] region_f_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_f_ensures_2 (Qed)
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
index 40300a0021d..8ac57f31244 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
@@ -5,54 +5,6 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
 [wp] 6 goals scheduled
 [wp] [Valid] region_f_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_f_assert (Alt-Ergo) (Cached)
-- 
GitLab