From 9dbd1fbf100683ed1d0d047f075cdbaaeddade7b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 1 Apr 2020 08:55:49 +0200
Subject: [PATCH] [tests] update test for #840 and set oracle
---
tests/slicing/function_lvar.i | 2 +-
tests/slicing/oracle/function_lvar.res.oracle | 57 +++++++++++++++++++
2 files changed, 58 insertions(+), 1 deletion(-)
create mode 100644 tests/slicing/oracle/function_lvar.res.oracle
diff --git a/tests/slicing/function_lvar.i b/tests/slicing/function_lvar.i
index c7d245c4528..05cc5c69a20 100644
--- a/tests/slicing/function_lvar.i
+++ b/tests/slicing/function_lvar.i
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -slice-pragma main
+OPT: -slice-pragma main -then-last -print
*/
int g(int x) { return x; }
diff --git a/tests/slicing/oracle/function_lvar.res.oracle b/tests/slicing/oracle/function_lvar.res.oracle
new file mode 100644
index 00000000000..667a53c29a9
--- /dev/null
+++ b/tests/slicing/oracle/function_lvar.res.oracle
@@ -0,0 +1,57 @@
+[kernel] Parsing tests/slicing/function_lvar.i (no preprocessing)
+[slicing] slicing requests in progress...
+[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:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 5 statements reached (out of 5): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function main
+[from] Computing for function g
+[from] Done for function g
+[pdg] done for function main
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[pdg] computing for function g
+[pdg] done for function g
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int g(int x);
+
+void g_slice_1(void)
+{
+ return;
+}
+
+void main(void)
+{
+ /*@ assert &g 鈮� &g; */ ;
+ /*@ slice pragma stmt; */
+ g_slice_1();
+ return;
+}
+
+
--
GitLab