diff --git a/ptests/check_oracles.sh b/ptests/check_oracles.sh
index 5deedcb293b311150dfb2996532d1e68212c5832..a7bb568c1f52e01a6a31cc2a0478c30abdb3a003 100755
--- a/ptests/check_oracles.sh
+++ b/ptests/check_oracles.sh
@@ -55,7 +55,7 @@ do
# only report oracles in tested directories (DEFAULT_SUITES)
for dir in $(grep DEFAULT_SUITES "tests/ptests_config" | sed 's/DEFAULT_SUITES=//'); do
- find "tests/$dir" -name "*.oracle" | sed "s|^|${plugin_test_dir%tests}|" >> $actual_oracles
+ find "tests/$dir" -name "*.oracle" | sed "s|^|${plugin_test_dir%tests}|" | sed 's|"|\\"|g' >> $actual_oracles
done
)
done
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle
deleted file mode 100644
index c9a461392e7cb29343481e9e0560a5021bf0beb2..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle
+++ /dev/null
@@ -1,254 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function comprehension_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 85) in 'comprehension_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 86) in 'comprehension_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 84) in 'comprehension_alias':
-Effect at line 88
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function field_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 54) in 'field_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 55) in 'field_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 53) in 'field_alias':
-Effect at line 57
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function field_range_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 66) in 'field_range_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 67) in 'field_range_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 65) in 'field_range_alias':
-Effect at line 69
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function formal_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 25) in 'formal_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 26) in 'formal_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 24) in 'formal_alias':
-Effect at line 28
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function formal_alias_array
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 40) in 'formal_alias_array':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 41) in 'formal_alias_array':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 42) in 'formal_alias_array':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (1/2):
-Effect at line 44
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (2/2):
-Effect at line 45
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function formal_no_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 33) in 'formal_no_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 32) in 'formal_no_alias':
-Effect at line 35
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function global_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 10) in 'global_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 11) in 'global_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 9) in 'global_alias':
-Effect at line 13
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function global_no_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 18) in 'global_no_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 17) in 'global_no_alias':
-Effect at line 20
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function set_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 74) in 'set_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 75) in 'set_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 73) in 'set_alias':
-Effect at line 77
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function union_alias
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 95) in 'union_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 96) in 'union_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 94) in 'union_alias':
-Effect at line 98
-Prove: true.
-
-------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_alias':
- /*@
- behavior typed:
- requires \separated(g_alias,\union(&g_alias,global+(..)));
- */
- void global_alias(void);
-[wp] Warning: Memory model hypotheses for function 'global_no_alias':
- /*@ behavior typed: requires \separated(g_alias,&g_alias); */
- void global_no_alias(void);
-[wp] Warning: Memory model hypotheses for function 'formal_alias':
- /*@
- behavior typed:
- requires \separated(global+(..),f_alias);
- requires \separated(f_alias,global+(..));
- */
- void formal_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
- /*@
- behavior typed:
- requires \separated(global+(..),alias_array+(..));
- requires \separated(&(*alias_array)[0 .. 1],global+(..));
- */
- void formal_alias_array(int (*alias_array)[2]);
-[wp] Warning: Memory model hypotheses for function 'field_alias':
- /*@
- behavior typed:
- requires \separated(global+(..),x);
- requires \separated(&x->x,global+(..));
- */
- void field_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'field_range_alias':
- /*@
- behavior typed:
- requires \separated(global+(..),x+(..));
- requires \separated(&(x + (0 .. 3))->x,global+(..));
- */
- void field_range_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'set_alias':
- /*@
- behavior typed:
- requires \separated(\union(global+(..),&g_alias),f_alias);
- requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
- */
- void set_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
- /*@
- behavior typed:
- requires \separated({alias | int *alias; alias ≡ \at(g_alias,Pre)},
- \union(&g_alias,global+(..)));
- */
- void comprehension_alias(void);
-[wp] Warning: Memory model hypotheses for function 'union_alias':
- /*@
- behavior typed:
- requires \separated(\union(global+(..),&g_alias),f_alias);
- requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
- */
- void union_alias(int *f_alias);
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.h b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/bitmask0x8000.h
rename to src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unsigned.err.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unsigned.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unsigned.res.oracle
deleted file mode 100644
index e7238623044f48af8abeae9895e9a68e455001b3..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/unsigned.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] 1 goal scheduled
-[wp] [Tactical] Goal typed_lemma_U32 : Valid
-[wp] Proved goals: 1 / 1
- Qed: 0
- Script: 1
-------------------------------------------------------------
- Global
-------------------------------------------------------------
-
-Lemma U32:
-Prove: (is_uint32 x_0) -> ((land 4294967295 x_0)=x_0)
-Prover Tactical returns Valid
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
index ac78ca7305f4763d5fd6c105d3e9e4075a6736ac..c1f541d00af218c3a2c837305606b0681f1e9f7d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
@@ -3,6 +3,6 @@
"target": "not (bit_test off_0 15)",
"pattern": "!bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "qed", "verdict": "valid" } ],
- "Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0203,
- "steps": 21 } ] } } ]
+ "Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0263,
+ "steps": 32 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
index 33e7209ad3158d6d4f71329229b8baae165cd394..95cf3e5f2953bc7ed7b6c9ad5939b20299677781 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
@@ -2,7 +2,7 @@
"select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "(bit_test off_0 15)",
"pattern": "bit_test$off15" },
- "children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0214,
- "steps": 20 } ],
+ "children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0129,
+ "steps": 32 } ],
"Bit #15 (sup)": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
index 1fdbf73385990607f817cc728ca4b1de46c36995..5c4ea8084169bec24a7caa4d469727168e29a2e0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/bitmask0x8000.h (with preprocessing)
+[kernel] Parsing tests/wp_plugin/bitmask0x8000.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Script] Goal typed_lemma_res_n : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
deleted file mode 100644
index b908bc8578a9a582d5db8cd077546571368e4e06..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-# frama-c -wp -wp-no-let -wp-timeout 45 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-[wp] 7 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_band_bool_false_ensures : Unsuccess
-[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_bor_bool_false_ensures : Unsuccess
-[wp] [Alt-Ergo 2.0.0] Goal typed_bor_bool_true_ensures : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_bxor_bool_false_ensures : Unsuccess
-[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_job_ensures : Unsuccess
-[wp] Proved goals: 3 / 7
- Qed: 2
- Alt-Ergo 2.0.0: 1 (unsuccess: 4)
-[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.0.report.json'
-[wp] Report out: 'tests/wp_plugin/result_qualif/bool.0.report.json'
--------------------------------------------------------------
-Functions WP Alt-Ergo Total Success
-job - - 1 0.0%
-bor_bool - 1 (4..16) 2 50.0%
-band_bool 1 - 2 50.0%
-bxor_bool 1 - 2 50.0%
--------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle
deleted file mode 100644
index 1524fcd67af880eeea3ae07ea547aae8eb0d7ea1..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle
+++ /dev/null
@@ -1,10 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] 1 goal scheduled
-[wp] [Script] Goal typed_lemma_Simple : Unsuccess
-[wp] Proved goals: 0 / 1
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic Inductive - - 1 0.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
deleted file mode 100644
index e6c28bf655407f69bf063936bf2860a26d7c671d..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
+++ /dev/null
@@ -1,22 +0,0 @@
-# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-[wp] 8 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_init_ensures : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_invariant_Partial_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_invariant_Range_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
-[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_init_assigns : Valid
-[wp] Proved goals: 8 / 8
- Qed: 4
- Alt-Ergo 2.0.0: 4
-[wp] Report 'tests/wp_typed/user_init.i.0.report.json'
--------------------------------------------------------------
-Functions WP Alt-Ergo Total Success
-init 4 4 (48..60) 8 100%
--------------------------------------------------------------
diff --git a/tests/metrics/oracle/libc.3.res.oracle b/tests/metrics/oracle/libc.3.res.oracle
deleted file mode 100644
index eeb5977dbc5fef0789c0e314ec2e68f5834bd8d2..0000000000000000000000000000000000000000
--- a/tests/metrics/oracle/libc.3.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/metrics/libc.c (with preprocessing)
diff --git a/tests/misc/oracle/log-file.0.res.oracle b/tests/misc/oracle/log-file.0.res.oracle
deleted file mode 100644
index 83288a2ea513c05a7125a26eea8b5a4cee999871..0000000000000000000000000000000000000000
--- a/tests/misc/oracle/log-file.0.res.oracle
+++ /dev/null
@@ -1,44 +0,0 @@
-[kernel] Parsing tests/misc/log-file.i (no preprocessing)
-[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] computing for function f <- main.
- Called from tests/misc/log-file.i:20.
-[kernel:annot:missing-spec] tests/misc/log-file.i:20: Warning:
- Neither code nor specification for function f, generating default assigns from the prototype
-[eva] using specification for function f
-[eva] Done for function f
-[eva] computing for function g <- main.
- Called from tests/misc/log-file.i:21.
-[eva] using specification for function g
-[eva] tests/misc/log-file.i:17: Warning:
- no 'assigns \result \from ...' clause specified for function g
-[eva] Done for function g
-[eva] tests/misc/log-file.i:22: starting to merge loop iterations
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
- r ∈ [--..--]
- __retres ∈ {0}
-[from] Computing for function main
-[from] Computing for function f <-main
-[from] Done for function f
-[from] Computing for function g <-main
-[from] Done for function g
-[from] Done for function main
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- \result FROM \nothing
-[from] Function g:
- \result FROM ANYTHING(origin:Unknown)
-[from] Function main:
- \result FROM \nothing
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main:
- r; i; __retres
-[inout] Inputs for function main:
- \nothing
diff --git a/tests/misc/oracle/log-file.1.res.oracle b/tests/misc/oracle/log-file.1.res.oracle
deleted file mode 100644
index c5369cc7504986a9cb0dda96a852e4dd05417423..0000000000000000000000000000000000000000
--- a/tests/misc/oracle/log-file.1.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-[kernel] Parsing tests/misc/log-file.i (no preprocessing)
-[kernel:foo-category] result with dkey
-[kernel] result
-[kernel:foo-category] feedback with dkey
-[kernel] feedback
-[kernel:foo-category] debug (level 0) with dkey
-[kernel] debug (level 0)
-[kernel] Warning: warning
diff --git a/tests/misc/oracle/my_visitor.res.oracle b/tests/misc/oracle/my_visitor.res.oracle
deleted file mode 100644
index 04b0d97491307081cc55be88c27f3d3b47e00392..0000000000000000000000000000000000000000
--- a/tests/misc/oracle/my_visitor.res.oracle
+++ /dev/null
@@ -1,23 +0,0 @@
-[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
-[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
-[kernel] Warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
-[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
-[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
-[kernel] Warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
-/* Generated by Frama-C */
-int f(void)
-{
- int __retres;
- /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
- int y = 0;
- y ++;
- /*@ assert y ≡ 1; */
- /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
- ;
- __retres = 0;
- /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
- return __retres;
-}
-
-