From 66ee58eab5e498cfc89fb5334a7d3369be77e25e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 17 Jul 2019 13:01:45 +0200
Subject: [PATCH] [Tests] Ghost parameters: side-effects on ghost call
---
src/kernel_internals/typing/cabs2cil.ml | 21 +++++++++----------
.../syntax/ghost_parameters_side_effect_arg.i | 7 ++++++-
...host_parameters_side_effect_arg.res.oracle | 10 +++++++++
3 files changed, 26 insertions(+), 12 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index d11d5f446d1..2478228b9e2 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6514,10 +6514,9 @@ and doExp local_env
| Lval (Var fv, NoOffset) -> Cil.is_special_builtin fv.vname
| _ -> false
in
+ let init_chunk = unspecified_chunk empty in
(* Do the arguments. In REVERSE order !!! Both GCC and MSVC do this *)
- let rec loopArgs
- ?(init_chunk=unspecified_chunk empty) ?(are_ghost=false)
- = function
+ let rec loopArgs ?(are_ghost=false) = function
| ([], []) ->
(match argTypes, f''.enode with
| None, Lval (Var f,NoOffset) ->
@@ -6537,13 +6536,12 @@ and doExp local_env
| _, [] ->
if not isSpecialBuiltin then
Kernel.error ~once:true ~current:true
- "Too few %s in call to %a."
- ((if are_ghost then "ghost " else "") ^ "arguments")
- Cil_printer.pp_exp f' ;
+ "Too few%s arguments in call to %a."
+ (if are_ghost then " ghost" else "") Cil_printer.pp_exp f' ;
(init_chunk, [])
| ((_, at, _) :: atypes, a :: args) ->
- let (ss, args') = loopArgs ~init_chunk ~are_ghost (atypes, args) in
+ let (ss, args') = loopArgs ~are_ghost (atypes, args) in
(* Do not cast as part of translating the argument. We let
* the castTo do this work. This was necessary for
* test/small1/union5, in which a transparent union is passed
@@ -6617,9 +6615,8 @@ and doExp local_env
if not isvar && argTypes != None && not isSpecialBuiltin then
(* Do not give a warning for functions without a prototype*)
Kernel.error ~once:true ~current:true
- "Too many %s in call to %a"
- ((if are_ghost then "ghost " else "") ^ "arguments")
- Cil_printer.pp_exp f';
+ "Too many%s arguments in call to %a"
+ (if are_ghost then " ghost" else "") Cil_printer.pp_exp f';
let rec loop = function
[] -> (init_chunk, [])
| a :: args ->
@@ -6676,7 +6673,9 @@ and doExp local_env
in
let args = if ghost then args @ ghost_args else args in
let (sghost, ghosts') = loopArgs ~are_ghost:true (ghostArgTypes, ghost_args) in
- let (sargs, args') = loopArgs ~init_chunk:sghost (argTypes, args) in
+ let (sargs, args') = loopArgs (argTypes, args) in
+
+ let sargs = sghost @@ (sargs, false) in
let (sargs, args') = (sargs, args' @ ghosts') in
(* Setup some pointer to the elements of the call. We may change
diff --git a/tests/syntax/ghost_parameters_side_effect_arg.i b/tests/syntax/ghost_parameters_side_effect_arg.i
index 0df969f056c..00d02e6665a 100644
--- a/tests/syntax/ghost_parameters_side_effect_arg.i
+++ b/tests/syntax/ghost_parameters_side_effect_arg.i
@@ -8,9 +8,14 @@ void caller(){
function(x++) /*@ ghost(g++) */ ;
function(x = 2) /*@ ghost(g = 42) */ ;
- 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) ) */ ;
+
+ /*@ ghost
+ int i = 1 ;
+ function(g++, i++) ;
+ */
}
diff --git a/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle b/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
index 544448d8da7..a049a30bcfb 100644
--- a/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
@@ -14,6 +14,8 @@ void caller(void)
int tmp_1;
/*@ ghost int g_tmp_2; */
int tmp_2;
+ /*@ ghost int g_tmp_3; */
+ /*@ ghost int g_tmp_4; */
int x = 0;
/*@ ghost int g = 0; */
int t[3] = {0, 0, 0};
@@ -44,6 +46,14 @@ void caller(void)
/*@ ghost g_tmp_2 = other(x,g); */
tmp_2 = other(x)/*@ ghost (g) */;
function(tmp_2)/*@ ghost (g_tmp_2) */;
+ /*@ ghost int i = 1; */
+ /*@ ghost g_tmp_3 = i;
+ i ++;
+ ;
+ g_tmp_4 = g;
+ g ++;
+ ; */
+ /*@ ghost function(g_tmp_4,g_tmp_3); */
return;
}
--
GitLab