From e0de5711bc0aa7c99b78fe148ec23c44ee8f57ab Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Wed, 21 Nov 2018 15:33:32 +0100
Subject: [PATCH] Makes argsToList usable again and adds a variant that
differenciates ghost/non-ghosts
---
src/kernel_internals/typing/cabs2cil.ml | 4 ++--
.../ast_printing/cil_printer.ml | 18 +++++++++---------
src/kernel_services/ast_queries/cil.ml | 5 +++++
src/kernel_services/ast_queries/cil.mli | 9 ++++++++-
4 files changed, 24 insertions(+), 12 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b5121c2d318..8f061f3f097 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5085,8 +5085,8 @@ and doType (ghost:bool) isFuncArg
let targs : varinfo list option =
match noopt_targs @ noopt_ghost_targs with
| [] -> None (* No argument list *)
- | [t] when isVoidType t.vtype ->
- Some []
+ | t :: l' when isVoidType t.vtype ->
+ Some l'
| l ->
Some l
in
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 7b2bd0d30b9..c661a2248ad 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -878,16 +878,11 @@ class cil_printer () = object (self)
let is_ghost_type (_, _, a) = Cil.hasAttribute Cil.frama_c_ghost a in
let rec split = function
- (* it means we have a va_list *)
- | [], args ->
- args, []
- (* all remaining arguments are necessarily ghosts *)
- | t :: _ , args when is_ghost_type t ->
- [], args
+ | [], args -> args, []
+ | t :: _ , args when is_ghost_type t -> [], args
| _ :: l , a :: args' ->
let (args, ghosts) = split (l, args') in
(a :: args, ghosts)
- (* it could not typecheck *)
| _ :: _ , [] -> assert false
in
let args, ghosts = if is_ghost then args, [] else split (param_ts, args) in
@@ -895,7 +890,12 @@ class cil_printer () = object (self)
(* Now the arguments *)
Pretty_utils.pp_flowlist ~left:"(" ~sep:"," ~right:")" self#exp fmt args;
(* Now the ghost arguments *)
- Pretty_utils.pp_list ~pre:"/*@@ ghost (" ~suf:") */" self#exp fmt ghosts;
+ begin match ghosts with
+ | [] -> ()
+ | _ -> Pretty_utils.pp_flowlist
+ ~left:"/*@@ ghost (" ~sep:"," ~right:") */"
+ self#exp fmt ghosts
+ end ;
(* Now the terminator *)
fprintf fmt "%s" instr_terminator
in
@@ -1922,7 +1922,7 @@ class cil_printer () = object (self)
Pretty_utils.pp_list ~sep:",@ " pp_args fmt args;
if isvararg then fprintf fmt "@ , ...")
;
- Pretty_utils.pp_list ~pre:"/*@@ ghost (" ~suf:") */"
+ Pretty_utils.pp_list ~pre:"/*@@ ghost (" ~suf:") */" ~sep:", "
pp_args fmt ghost_args
in
let pp_params fmt = match fundecl with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d9fb06581ff..264a2792759 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5798,6 +5798,11 @@ let splitFunctionTypeVI (fvi: varinfo)
TFun (rt, args, isva, a) -> rt, args, isva, a
| _ -> Kernel.abort "Function %s invoked on a non function type" fvi.vname
+let argsToPairOfLists args =
+ List.partition
+ (fun (_,_,a) -> not(hasAttribute frama_c_ghost a))
+ (argsToList args)
+
let remove_attributes_for_integral_promotion a =
dropAttributes (bitfield_attribute_name :: spare_attributes_for_c_cast) a
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 6767491fb0f..2a4dce08908 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -580,10 +580,17 @@ val isTypeTagType: logic_type -> bool
@since Nitrogen-20111001 moved from cabs2cil *)
val isVariadicListType: typ -> bool
-(** Obtain the argument list ([] if None) *)
+(** Obtain the argument list ([] if None).
+ @since Argon+dev Beware that it contains the ghost arguments. *)
val argsToList:
(string * typ * attributes) list option -> (string * typ * attributes) list
+(** @since Argon+dev
+ Obtain the argument lists (non-ghost, ghosts) ([], [] if None) *)
+val argsToPairOfLists:
+ (string * typ * attributes) list option ->
+ (string * typ * attributes) list * (string * typ * attributes) list
+
(** True if the argument is an array type *)
val isArrayType: typ -> bool
--
GitLab