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 21e0d8d49e93362922685b0c1538a1026d24bedf..c05fcc276682f9b154646b05cb55addc0de2b977 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; }