From 8573c6ad43b66564ddc838b255310c1529e35c27 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 16 Dec 2019 18:25:39 +0100
Subject: [PATCH] [e-acsl:tests] update tests wrt kernel changes
---
.../e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
index 21e0d8d49e9..c05fcc27668 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
@@ -1,7 +1,7 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
-void function(int a, int b, int c, int d)
+void function(int a, int b) /*@ ghost (int c, int d) */
{
return;
}
@@ -14,7 +14,7 @@ int main(void)
int x = 1;
int y = 2;
int z = 3;
- function(w,x,y,z);
+ function(w,x) /*@ ghost (y,z) */;
__retres = 0;
return __retres;
}
--
GitLab