From b93f5a86cc14d1d05d5b803c9cd237664a31520b Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 30 Sep 2020 15:19:27 +0200
Subject: [PATCH] init modif for tests/pretty_printing
---
.../oracle/annotations.res.oracle | 15 ++++++++++-----
.../oracle/binary_logic_op.res.oracle | 7 ++-----
.../oracle/ghost_else.res.oracle | 17 ++++++++++++-----
.../pretty_printing/oracle/relations.res.oracle | 7 ++-----
tests/pretty_printing/test_config | 2 +-
5 files changed, 27 insertions(+), 21 deletions(-)
diff --git a/tests/pretty_printing/oracle/annotations.res.oracle b/tests/pretty_printing/oracle/annotations.res.oracle
index 0e3863f75ac..255b684d87d 100644
--- a/tests/pretty_printing/oracle/annotations.res.oracle
+++ b/tests/pretty_printing/oracle/annotations.res.oracle
@@ -110,9 +110,16 @@ void reference_function(void)
}
-[kernel] Warning: Fail to open file "result/annotations.c" for code output
- System error: result/annotations.c: No such file or directory.
- Code is output on stdout instead.
+[kernel] Parsing annotations_tmp.c (with preprocessing)
+[kernel] Parsing annotations.i (no preprocessing)
+[kernel] annotations.i:13: Warning:
+ def'n of func function_no_ghost at annotations.i:13 (sum 9297192) conflicts with the one at annotations_tmp.c:12 (sum 14988159); keeping the one at annotations_tmp.c:12.
+[kernel] annotations.i:43: Warning:
+ def'n of func function_with_ghost at annotations.i:43 (sum 9297192) conflicts with the one at annotations_tmp.c:38 (sum 14988159); keeping the one at annotations_tmp.c:38.
+[kernel] annotations.i:80: Warning:
+ def'n of func ghost_function at annotations.i:80 (sum 9297192) conflicts with the one at annotations_tmp.c:71 (sum 14988159); keeping the one at annotations_tmp.c:71.
+[kernel] annotations.i:114: Warning:
+ dropping duplicate def'n of func reference_function at annotations.i:114 in favor of that at annotations_tmp.c:105
/* Generated by Frama-C */
/*@ axiomatic A {
predicate P(ℤ x)
@@ -224,5 +231,3 @@ void reference_function(void)
}
-[kernel] User Error: source file 'result/annotations.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/pretty_printing/oracle/binary_logic_op.res.oracle b/tests/pretty_printing/oracle/binary_logic_op.res.oracle
index 0b5ef363d0c..aaaee21786a 100644
--- a/tests/pretty_printing/oracle/binary_logic_op.res.oracle
+++ b/tests/pretty_printing/oracle/binary_logic_op.res.oracle
@@ -22,9 +22,8 @@ predicate mixed(ℤ x, ℤ y, ℤ z, ℤ t) =
/*@ logic â„ exp(â„ n) = \pow(\e, n);
*/
-[kernel] Warning: Fail to open file "result/binary_logic_op.c" for code output
- System error: result/binary_logic_op.c: No such file or directory.
- Code is output on stdout instead.
+[kernel] Parsing binary_logic_op_tmp.c (with preprocessing)
+[kernel] Parsing binary_logic_op.c (with preprocessing)
/* Generated by Frama-C */
/*@
predicate foo(ℤ x) =
@@ -48,5 +47,3 @@ predicate mixed(ℤ x, ℤ y, ℤ z, ℤ t) =
/*@ logic â„ exp(â„ n) = \pow(\e, n);
*/
-[kernel] User Error: source file 'result/binary_logic_op.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/pretty_printing/oracle/ghost_else.res.oracle b/tests/pretty_printing/oracle/ghost_else.res.oracle
index 6f914bc798d..ddf4b223737 100644
--- a/tests/pretty_printing/oracle/ghost_else.res.oracle
+++ b/tests/pretty_printing/oracle/ghost_else.res.oracle
@@ -44,9 +44,18 @@ void ghost_else_plus_else_association(int x) /*@ ghost (int y) */
}
-[kernel] Warning: Fail to open file "result/ghost_else.c" for code output
- System error: result/ghost_else.c: No such file or directory.
- Code is output on stdout instead.
+[kernel] Parsing ghost_else_tmp.c (with preprocessing)
+[kernel] Parsing ghost_else.i (no preprocessing)
+[kernel] ghost_else.i:1: Warning:
+ dropping duplicate def'n of func if_ghost_else_one_line at ghost_else.i:1 in favor of that at ghost_else_tmp.c:2
+[kernel] ghost_else.i:7: Warning:
+ dropping duplicate def'n of func if_ghost_else_block at ghost_else.i:7 in favor of that at ghost_else_tmp.c:9
+[kernel] ghost_else.i:15: Warning:
+ dropping duplicate def'n of func if_ghost_else_multi_line_block at ghost_else.i:15 in favor of that at ghost_else_tmp.c:16
+[kernel] ghost_else.i:25: Warning:
+ dropping duplicate def'n of func normal_if_ghost_else_intricated at ghost_else.i:25 in favor of that at ghost_else_tmp.c:27
+[kernel] ghost_else.i:32: Warning:
+ dropping duplicate def'n of func ghost_else_plus_else_association at ghost_else.i:32 in favor of that at ghost_else_tmp.c:35
/* Generated by Frama-C */
void if_ghost_else_one_line(int x) /*@ ghost (int y) */
{
@@ -92,5 +101,3 @@ void ghost_else_plus_else_association(int x) /*@ ghost (int y) */
}
-[kernel] User Error: source file 'result/ghost_else.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/pretty_printing/oracle/relations.res.oracle b/tests/pretty_printing/oracle/relations.res.oracle
index 488a65eba40..97183cc29c2 100644
--- a/tests/pretty_printing/oracle/relations.res.oracle
+++ b/tests/pretty_printing/oracle/relations.res.oracle
@@ -5,14 +5,11 @@
/*@ predicate rel2(ℤ x, ℤ y, ℤ z, ℤ t) = x ≤ y ≡ z ∧ z ≥ t;
*/
-[kernel] Warning: Fail to open file "result/relations.c" for code output
- System error: result/relations.c: No such file or directory.
- Code is output on stdout instead.
+[kernel] Parsing relations_tmp.c (with preprocessing)
+[kernel] Parsing relations.c (with preprocessing)
/* Generated by Frama-C */
/*@ predicate rel1(ℤ x, ℤ y, ℤ z, ℤ t) = x ≤ y ≤ z ∧ z ≥ t;
*/
/*@ predicate rel2(ℤ x, ℤ y, ℤ z, ℤ t) = x ≤ y ≡ z ∧ z ≥ t;
*/
-[kernel] User Error: source file 'result/relations.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config
index c43ca105429..564c7371a45 100644
--- a/tests/pretty_printing/test_config
+++ b/tests/pretty_printing/test_config
@@ -2,4 +2,4 @@ COMMENT: this directory is meant to test the parser and pretty-printer
COMMENT: the default option checks that pretty-printed code can be merged
COMMENT: with the original one
CMD: FRAMAC_PLUGIN=tests/.empty @frama-c@
-OPT: @PTEST_FILE@ -print -journal-disable -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
+OPT: @PTEST_FILE@ -print -journal-disable -check -then -ocode @PTEST_NAME@_tmp.c -print -then @PTEST_NAME@_tmp.c @PTEST_FILE@ -ocode="" -print
--
GitLab