diff --git a/tests/pretty_printing/oracle/annotations.res.oracle b/tests/pretty_printing/oracle/annotations.res.oracle index 255b684d87d9a451d9ae7c7690b54448550fcda7..5bf1bbf12250bb5f4072936f612e0e31774e9b9b 100644 --- a/tests/pretty_printing/oracle/annotations.res.oracle +++ b/tests/pretty_printing/oracle/annotations.res.oracle @@ -110,16 +110,16 @@ void reference_function(void) } -[kernel] Parsing annotations_tmp.c (with preprocessing) +[kernel] Parsing ocode_0_annotations.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. + def'n of func function_no_ghost at annotations.i:13 (sum 9297192) conflicts with the one at ocode_0_annotations.c:12 (sum 14988159); keeping the one at ocode_0_annotations.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. + def'n of func function_with_ghost at annotations.i:43 (sum 9297192) conflicts with the one at ocode_0_annotations.c:38 (sum 14988159); keeping the one at ocode_0_annotations.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. + def'n of func ghost_function at annotations.i:80 (sum 9297192) conflicts with the one at ocode_0_annotations.c:71 (sum 14988159); keeping the one at ocode_0_annotations.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 + dropping duplicate def'n of func reference_function at annotations.i:114 in favor of that at ocode_0_annotations.c:105 /* Generated by Frama-C */ /*@ axiomatic A { predicate P(ℤ x) diff --git a/tests/pretty_printing/oracle/binary_logic_op.res.oracle b/tests/pretty_printing/oracle/binary_logic_op.res.oracle index aaaee21786ad5c914b1e434a6327626d979ee834..84f4e54ade864e4385d02939f3eec006a08823fc 100644 --- a/tests/pretty_printing/oracle/binary_logic_op.res.oracle +++ b/tests/pretty_printing/oracle/binary_logic_op.res.oracle @@ -22,7 +22,7 @@ predicate mixed(ℤ x, ℤ y, ℤ z, ℤ t) = /*@ logic ℠exp(℠n) = \pow(\e, n); */ -[kernel] Parsing binary_logic_op_tmp.c (with preprocessing) +[kernel] Parsing ocode_0_binary_logic_op.c (with preprocessing) [kernel] Parsing binary_logic_op.c (with preprocessing) /* Generated by Frama-C */ /*@ diff --git a/tests/pretty_printing/oracle/ghost_else.res.oracle b/tests/pretty_printing/oracle/ghost_else.res.oracle index ddf4b2237375be69f394ca80a89700ded8571b79..2b7895ea3ee5bc8fa7afaa299c434f5975fffcc2 100644 --- a/tests/pretty_printing/oracle/ghost_else.res.oracle +++ b/tests/pretty_printing/oracle/ghost_else.res.oracle @@ -44,18 +44,18 @@ void ghost_else_plus_else_association(int x) /*@ ghost (int y) */ } -[kernel] Parsing ghost_else_tmp.c (with preprocessing) +[kernel] Parsing ocode_0_ghost_else.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 + dropping duplicate def'n of func if_ghost_else_one_line at ghost_else.i:1 in favor of that at ocode_0_ghost_else.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 + dropping duplicate def'n of func if_ghost_else_block at ghost_else.i:7 in favor of that at ocode_0_ghost_else.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 + dropping duplicate def'n of func if_ghost_else_multi_line_block at ghost_else.i:15 in favor of that at ocode_0_ghost_else.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 + dropping duplicate def'n of func normal_if_ghost_else_intricated at ghost_else.i:25 in favor of that at ocode_0_ghost_else.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 + dropping duplicate def'n of func ghost_else_plus_else_association at ghost_else.i:32 in favor of that at ocode_0_ghost_else.c:35 /* Generated by Frama-C */ void if_ghost_else_one_line(int x) /*@ ghost (int y) */ { diff --git a/tests/pretty_printing/oracle/relations.res.oracle b/tests/pretty_printing/oracle/relations.res.oracle index 97183cc29c288e575355a748ab50718786ca6894..13fab570d66fc74b5496bf47f9bd52a97e38d4bf 100644 --- a/tests/pretty_printing/oracle/relations.res.oracle +++ b/tests/pretty_printing/oracle/relations.res.oracle @@ -5,7 +5,7 @@ /*@ predicate rel2(ℤ x, ℤ y, ℤ z, ℤ t) = x ≤ y ≡ z ∧ z ≥ t; */ -[kernel] Parsing relations_tmp.c (with preprocessing) +[kernel] Parsing ocode_0_relations.c (with preprocessing) [kernel] Parsing relations.c (with preprocessing) /* Generated by Frama-C */ /*@ predicate rel1(ℤ x, ℤ y, ℤ z, ℤ t) = x ≤ y ≤ z ∧ z ≥ t; diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config index 564c7371a459e610a391bf700b53134e40622022..c2ed0fe4352442993c379966cb56aeacb106dc58 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_NAME@_tmp.c -print -then @PTEST_NAME@_tmp.c @PTEST_FILE@ -ocode="" -print +OPT: @PTEST_FILE@ -print -journal-disable -check -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print