From b1ae8fd09f84149bf3affd5eb58c49064a4801ac Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Fri, 1 Feb 2019 12:56:23 +0100
Subject: [PATCH] Adds a test for argument with side-effetcs in ghost
parameters
---
.../syntax/ghost_parameters_side_effect_arg.i | 16 ++++++
...host_parameters_side_effect_arg.res.oracle | 50 +++++++++++++++++++
2 files changed, 66 insertions(+)
create mode 100644 tests/syntax/ghost_parameters_side_effect_arg.i
create mode 100644 tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
diff --git a/tests/syntax/ghost_parameters_side_effect_arg.i b/tests/syntax/ghost_parameters_side_effect_arg.i
new file mode 100644
index 00000000000..0df969f056c
--- /dev/null
+++ b/tests/syntax/ghost_parameters_side_effect_arg.i
@@ -0,0 +1,16 @@
+void function(int x) /*@ ghost(int y) */ ;
+int other(int x) /*@ ghost(int y) */ ;
+
+void caller(){
+ int x = 0 ;
+ //@ ghost int g = 0 ;
+ int t[] = { 0, 0, 0 } ;
+
+ function(x++) /*@ ghost(g++) */ ;
+ function(x = 2) /*@ ghost(g = 42) */ ;
+ function(x += 2) /*@ ghost(g += 42) */ ;
+ function(-x) /*@ ghost(-g) */ ;
+ function( (x == 0) ? x : 42 ) /*@ ghost( (g == 0) ? g : 42 ) */ ;
+ function(t[x++]) /*@ ghost(t[g++]) */ ;
+ function( other(x) /*@ ghost(g) */ ) /*@ ghost( other(x, g) ) */ ;
+}
diff --git a/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle b/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
new file mode 100644
index 00000000000..544448d8da7
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
@@ -0,0 +1,50 @@
+[kernel] Parsing tests/syntax/ghost_parameters_side_effect_arg.i (no preprocessing)
+/* Generated by Frama-C */
+void function(int x)/*@ ghost (int y) */;
+
+int other(int x)/*@ ghost (int y) */;
+
+void caller(void)
+{
+ /*@ ghost int g_tmp; */
+ int tmp;
+ /*@ ghost int g_tmp_0; */
+ int tmp_0;
+ /*@ ghost int g_tmp_1; */
+ int tmp_1;
+ /*@ ghost int g_tmp_2; */
+ int tmp_2;
+ int x = 0;
+ /*@ ghost int g = 0; */
+ int t[3] = {0, 0, 0};
+ /*@ ghost g_tmp = g; */
+ /*@ ghost g ++; */
+ /*@ ghost ; */
+ tmp = x;
+ x ++;
+ ;
+ function(tmp)/*@ ghost (g_tmp) */;
+ /*@ ghost g = 42; */
+ x = 2;
+ function(x)/*@ ghost (g) */;
+ /*@ ghost g += 42; */
+ x += 2;
+ function(x)/*@ ghost (g) */;
+ function(- x)/*@ ghost (- g) */;
+ /*@ ghost if (g == 0) g_tmp_0 = g; else g_tmp_0 = 42; */
+ if (x == 0) tmp_0 = x; else tmp_0 = 42;
+ function(tmp_0)/*@ ghost (g_tmp_0) */;
+ /*@ ghost g_tmp_1 = g; */
+ /*@ ghost g ++; */
+ /*@ ghost ; */
+ tmp_1 = x;
+ x ++;
+ ;
+ function(t[tmp_1])/*@ ghost (t[g_tmp_1]) */;
+ /*@ ghost g_tmp_2 = other(x,g); */
+ tmp_2 = other(x)/*@ ghost (g) */;
+ function(tmp_2)/*@ ghost (g_tmp_2) */;
+ return;
+}
+
+
--
GitLab