From 14fd0be2c36cfdf30ba24f0c914a16749b1eb652 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 3 Aug 2020 18:17:22 +0200
Subject: [PATCH] update (unstable?) oracles

---
 cerberus/.frama-c/cheri_07_wide.eva/warnings.log                 | 1 -
 cerberus/.frama-c/compcertTSO-1.eva/warnings.log                 | 1 -
 cerberus/.frama-c/null_pointer_4.eva/warnings.log                | 1 -
 cerberus/.frama-c/padding_subunion_1.eva/warnings.log            | 1 -
 cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log   | 1 -
 .../pointer_arith_algebraic_properties_2_global.eva/warnings.log | 1 -
 cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log       | 1 -
 .../.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log  | 1 -
 .../provenance_basic_using_intptr_t_auto_yx.eva/warnings.log     | 1 -
 .../.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log   | 1 -
 .../.frama-c/provenance_via_io_bytewise_global.eva/warnings.log  | 1 -
 cerberus/.frama-c/trap_representation_3.eva/warnings.log         | 1 -
 .../unspecified_value_representation_bytes_1.eva/warnings.log    | 1 -
 13 files changed, 13 deletions(-)

diff --git a/cerberus/.frama-c/cheri_07_wide.eva/warnings.log b/cerberus/.frama-c/cheri_07_wide.eva/warnings.log
index 76958fa83..3cdf16b5d 100644
--- a/cerberus/.frama-c/cheri_07_wide.eva/warnings.log
+++ b/cerberus/.frama-c/cheri_07_wide.eva/warnings.log
@@ -1,3 +1,2 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 cheri_07_wide.c:10:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
 cheri_07_wide.c:12:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
diff --git a/cerberus/.frama-c/compcertTSO-1.eva/warnings.log b/cerberus/.frama-c/compcertTSO-1.eva/warnings.log
index 5880780ea..4a397709d 100644
--- a/cerberus/.frama-c/compcertTSO-1.eva/warnings.log
+++ b/cerberus/.frama-c/compcertTSO-1.eva/warnings.log
@@ -1,3 +1,2 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 compcertTSO-1.c:8:[eva:locals-escaping] warning: locals {a} escaping the scope of f through \result<f>
 compcertTSO-1.c:8:[eva:locals-escaping] warning: locals {a} escaping the scope of g through \result<g>
diff --git a/cerberus/.frama-c/null_pointer_4.eva/warnings.log b/cerberus/.frama-c/null_pointer_4.eva/warnings.log
index 14647f248..e69de29bb 100644
--- a/cerberus/.frama-c/null_pointer_4.eva/warnings.log
+++ b/cerberus/.frama-c/null_pointer_4.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/padding_subunion_1.eva/warnings.log b/cerberus/.frama-c/padding_subunion_1.eva/warnings.log
index 6dd22532c..77839f1a9 100644
--- a/cerberus/.frama-c/padding_subunion_1.eva/warnings.log
+++ b/cerberus/.frama-c/padding_subunion_1.eva/warnings.log
@@ -1,3 +1,2 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 padding_subunion_1.c:7:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
diff --git a/cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log b/cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log
index 14647f248..e69de29bb 100644
--- a/cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log
+++ b/cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/pointer_arith_algebraic_properties_2_global.eva/warnings.log b/cerberus/.frama-c/pointer_arith_algebraic_properties_2_global.eva/warnings.log
index 14647f248..e69de29bb 100644
--- a/cerberus/.frama-c/pointer_arith_algebraic_properties_2_global.eva/warnings.log
+++ b/cerberus/.frama-c/pointer_arith_algebraic_properties_2_global.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log b/cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log
index dd8bf5f19..5f466f985 100644
--- a/cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log
+++ b/cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log
@@ -1,4 +1,3 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 [eva:garbled-mix] warning: Garbled mix generated during analysis:
 {{ garbled mix of &{y} (origin: Arithmetic {pointer_offset_xor_auto.c:7}) }}
 {{ garbled mix of &{x} (origin: Arithmetic {pointer_offset_xor_auto.c:7}) }}
diff --git a/cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log b/cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log
index 0b296c6fb..83184169f 100644
--- a/cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log
+++ b/cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log
@@ -1,4 +1,3 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 provenance_basic_malloc_offset+12.c:4:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
 provenance_basic_malloc_offset+12.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
diff --git a/cerberus/.frama-c/provenance_basic_using_intptr_t_auto_yx.eva/warnings.log b/cerberus/.frama-c/provenance_basic_using_intptr_t_auto_yx.eva/warnings.log
index c4a4f6aee..af084233f 100644
--- a/cerberus/.frama-c/provenance_basic_using_intptr_t_auto_yx.eva/warnings.log
+++ b/cerberus/.frama-c/provenance_basic_using_intptr_t_auto_yx.eva/warnings.log
@@ -1,4 +1,3 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 provenance_basic_using_intptr_t_auto_yx.c:8:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_using_intptr_t_auto_yx.c:11:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
diff --git a/cerberus/.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log b/cerberus/.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log
index 14647f248..e69de29bb 100644
--- a/cerberus/.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log
+++ b/cerberus/.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/provenance_via_io_bytewise_global.eva/warnings.log b/cerberus/.frama-c/provenance_via_io_bytewise_global.eva/warnings.log
index 293d8de2d..1fcfffd06 100644
--- a/cerberus/.frama-c/provenance_via_io_bytewise_global.eva/warnings.log
+++ b/cerberus/.frama-c/provenance_via_io_bytewise_global.eva/warnings.log
@@ -1,4 +1,3 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 provenance_via_io_bytewise_global.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
 provenance_via_io_bytewise_global.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
 provenance_via_io_bytewise_global.c:14:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
diff --git a/cerberus/.frama-c/trap_representation_3.eva/warnings.log b/cerberus/.frama-c/trap_representation_3.eva/warnings.log
index 14647f248..e69de29bb 100644
--- a/cerberus/.frama-c/trap_representation_3.eva/warnings.log
+++ b/cerberus/.frama-c/trap_representation_3.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/unspecified_value_representation_bytes_1.eva/warnings.log b/cerberus/.frama-c/unspecified_value_representation_bytes_1.eva/warnings.log
index 14647f248..e69de29bb 100644
--- a/cerberus/.frama-c/unspecified_value_representation_bytes_1.eva/warnings.log
+++ b/cerberus/.frama-c/unspecified_value_representation_bytes_1.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
-- 
GitLab