From 517e407fd6c06463b99b2db8fe48c99daf825099 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Aug 2022 10:22:21 +0200
Subject: [PATCH] promoting oracle

---
 .../local_array_non_literal_size.res.oracle   | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/tests/misc/oracle/local_array_non_literal_size.res.oracle b/tests/misc/oracle/local_array_non_literal_size.res.oracle
index e69de29bb2d..ad5c39b2fd5 100644
--- a/tests/misc/oracle/local_array_non_literal_size.res.oracle
+++ b/tests/misc/oracle/local_array_non_literal_size.res.oracle
@@ -0,0 +1,42 @@
+[kernel] Parsing local_array_non_literal_size.i (no preprocessing)
+[kernel] local_array_non_literal_size.i:12: Warning: 
+  declaration of array of 'zero-length arrays' ('int [0]`);
+  zero-length arrays are a compiler extension
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] done for function main
+[eva] Warning: The scope plugin is missing: cannot remove redundant alarms.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function one_dim:
+  normal_array[0] ∈ {0}
+              [1] ∈ {1}
+              [2] ∈ {2}
+              [3] ∈ {3}
+[eva:final-states] Values at end of function two_dim_literal:
+  normal_array[0][0] ∈ {0}
+              [0][1] ∈ {1}
+              [0][2] ∈ {2}
+              [0][3] ∈ {3}
+[eva:final-states] Values at end of function two_dim_non_literal:
+  normal_array[0][0] ∈ {0}
+              [0][1] ∈ {1}
+              [0][2] ∈ {2}
+              [0][3] ∈ {3}
+[eva:final-states] Values at end of function main:
+  __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  4 functions analyzed (out of 4): 100% coverage.
+  In these functions, 14 statements reached (out of 14): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    1 warning
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
-- 
GitLab