From 5071ca131059fd536d53164913822926ef1231f7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Wed, 3 Oct 2018 15:06:15 +0200
Subject: [PATCH] Added placeholders for ghosts
---
src/kernel_internals/typing/cabs2cil.ml | 14 +++++++-------
src/kernel_services/ast_printing/cil_printer.ml | 8 ++++++++
src/kernel_services/ast_printing/cprint.ml | 12 ++++++------
3 files changed, 21 insertions(+), 13 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index cc275cde63e..bbb74a087c0 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4783,7 +4783,7 @@ and doAttr ghost (a: A.attribute) : attribute list =
end
| A.CONSTANT (A.CONST_FLOAT str) ->
ACons ("__fc_float", [AStr str])
- | A.CALL({expr_node = A.VARIABLE n}, args,ghost) -> begin
+ | A.CALL({expr_node = A.VARIABLE n}, args, ghost) -> begin
let n' = if strip then stripUnderscore n else n in
let ae' = List.map ae (args@ghost) in
ACons(n', ae')
@@ -5026,7 +5026,7 @@ and doType (ghost:bool) isFuncArg
function argument";
doDeclType (TArray(bt, lo, empty_size_cache (), al')) acc d
- | A.PROTO (d, args, _,isva) ->
+ | A.PROTO (d, args, _, isva) ->
(* Start a scope for the parameter names *)
enterScope ();
(* Intercept the old-style use of varargs.h. On GCC this means that
@@ -5180,7 +5180,7 @@ and isVariableSizedArray ghost (dt: A.decl_type)
| PTR (al, dt) -> PTR (al, findArray dt)
| JUSTBASE -> JUSTBASE
| PARENTYPE (prea, dt, posta) -> PARENTYPE (prea, findArray dt, posta)
- | PROTO (dt, f,g, a) -> PROTO (findArray dt, f,g, a)
+ | PROTO (dt, f, g, a) -> PROTO (findArray dt, f, g, a)
in
let dt' = findArray dt in
match !res with
@@ -6362,9 +6362,9 @@ and doExp local_env
intType
end
- | A.CALL(f, args,args_ghost) ->
- Format.printf "Length param %i@." (List.length args);
- Format.printf "Length param %i@." (List.length args_ghost);
+ | A.CALL(f, args,_args_ghost) ->
+(* Format.printf "Length param %i@." (List.length args);
+ Format.printf "Length param %i@." (List.length args_ghost);*)
let (rf,sf, f', ft') =
match (stripParen f).expr_node with
(* Treat the VARIABLE case separate because we might be calling a
@@ -8994,7 +8994,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
f' :: fl'
end
in
- let fmlocs = (match dt with PROTO(_, fml,_, _) -> fml | _ -> []) in
+ let fmlocs = (match dt with PROTO(_, fml, _, _) -> fml | _ -> []) in
let formals = doFormals (argsToList formals_t) fmlocs in
(* in case of formals referred to in types of others, doType has
put dummy varinfos. We need to fix them now that we have proper
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index adc133983a5..6479d91058c 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -873,6 +873,10 @@ class cil_printer () = object (self)
| _ -> fprintf fmt "(%a)" self#exp e);
(* Now the arguments *)
Pretty_utils.pp_flowlist ~left:"(" ~sep:"," ~right:")" self#exp fmt args;
+ (* Now the ghost arguments *)
+ Format.fprintf fmt "%t ghost " (fun fmt -> self#pp_open_annotation fmt);
+ Pretty_utils.pp_flowlist ~left:"(" ~sep:"," ~right:")" self#exp fmt [] ;
+ Format.fprintf fmt "@ %t" (fun fmt -> self#pp_close_annotation fmt);
(* Now the terminator *)
fprintf fmt "%s" instr_terminator
in
@@ -1891,6 +1895,10 @@ class cil_printer () = object (self)
| Some args ->
Pretty_utils.pp_list ~sep:",@ " pp_args fmt args;
if isvararg then fprintf fmt "@ , ...")
+ ;
+ Format.fprintf fmt "%t ghost (" (fun fmt -> self#pp_open_annotation fmt);
+ Pretty_utils.pp_list ~sep:",@ " pp_args fmt [] ;
+ Format.fprintf fmt ")@ %t" (fun fmt -> self#pp_close_annotation fmt);
in
let pp_params fmt = match fundecl with
| None ->
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 03e842b3193..36b2a4797aa 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -251,9 +251,9 @@ and print_decl (n: string) fmt = function
| ARRAY (d, al, e) ->
fprintf fmt "%a[@[%a%a@]]"
(print_decl n) d print_attributes al print_expression e
- | PROTO(d, args, isva) ->
- fprintf fmt "@[%a@;(%a)@]"
- (print_decl n) d print_params (args,isva)
+ | PROTO(d, args, ghost_args, isva) ->
+ fprintf fmt "@[%a@;(%a) /*@@@ ghost (%a) */ @]"
+ (print_decl n) d print_params (args,isva) print_params (ghost_args, false)
and print_fields fmt (flds : field_group list) =
pp_list ~sep:"@ " print_field_group fmt flds
@@ -369,9 +369,9 @@ and print_expression_level (lvl: int) fmt (exp : expression) =
[arg; { expr_node = TYPE_SIZEOF (bt, dt) } ], _) ->
fprintf fmt "__builtin_va_arg(@[%a,@ %a@])"
(print_expression_level 0) arg print_onlytype (bt, dt)
- | CALL (exp, args) ->
- fprintf fmt "%a(@[@;%a@])"
- print_expression exp print_comma_exps args
+ | CALL (exp, args, ghost_args) ->
+ fprintf fmt "%a(@[@;%a@]) /*@@@ ghost (@[@;%a@]) */"
+ print_expression exp print_comma_exps args print_comma_exps ghost_args
| CONSTANT (CONST_INT i) -> pp_print_string fmt i
| CONSTANT (CONST_FLOAT f) -> pp_print_string fmt f
| CONSTANT (CONST_CHAR c) -> fprintf fmt "'%s'" (escape_wstring c)
--
GitLab