From 3d246b6c0ec57530240fde7a9d3c794ab49ce969 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 19 Aug 2019 17:18:29 +0200
Subject: [PATCH] [Kernel] Changes the behavior of makeFormalVar to make it
easier to use
---
src/kernel_services/ast_queries/cil.ml | 33 +++++++++++++++----------
src/kernel_services/ast_queries/cil.mli | 25 +++++++++++++++----
tests/cil/insert_formal.ml | 12 ++++++---
3 files changed, 48 insertions(+), 22 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index f7023cb80fa..bc6dfe38314 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5285,28 +5285,35 @@ let setMaxId (f: fundec) =
* this one. If where = "^" then it is inserted first. If where = "$" then
* it is inserted last. Otherwise where must be the name of a formal after
* which to insert this. By default it is inserted at the end. *)
-let makeFormalVar fdec ?(where = "$") name typ : varinfo =
- let makeit ghost name =
+let makeFormalVar fdec ?(ghost=fdec.svar.vghost) ?(where = "$") name typ : varinfo =
+ assert ((not fdec.svar.vghost) || ghost) ;
+ let makeit name =
let vi = makeLocal ~ghost ~formal:true fdec name typ in
- if ghost then vi.vattr <- addAttribute (Attr(frama_c_ghost, [])) vi.vattr ;
+ if ghost && not fdec.svar.vghost then
+ vi.vattr <- addAttribute (Attr(frama_c_ghost, [])) vi.vattr ;
vi
in
+ let error () = Kernel.fatal ~current:true
+ "makeFormalVar: cannot find insert-after formal %s" where
+ in
(* Search for the insertion place *)
let rec loopFormals acc = function
- | [] when where = "$" || where = "$g" || where = "^g" ->
- let ghost = where = "$g" || where = "^g" in
- let vi = makeit ghost name in vi, List.rev (vi::acc)
| [] ->
- Kernel.fatal ~current:true
- "makeFormalVar: cannot find insert-after formal %s" where
- | f :: rest when f.vname = where ->
- let vi = makeit f.vghost name in vi, List.rev_append acc (f :: vi :: rest)
- | f :: rest when (f.vghost && where = "^g") ->
- let vi = makeit true name in vi, List.rev_append acc (vi :: f :: rest)
+ if where = "$" || (ghost && where = "^") then
+ let vi = makeit name in vi, List.rev (vi :: acc)
+ else error ()
+ | f :: rest when not ghost && f.vghost ->
+ if where = "$" then
+ let vi = makeit name in vi, List.rev_append acc (vi :: f :: rest)
+ else error ()
+ | f :: rest when f.vname = where && f.vghost = ghost ->
+ let vi = makeit name in vi, List.rev_append acc (f :: vi :: rest)
+ | f :: rest when ghost && f.vghost && where = "^" ->
+ let vi = makeit name in vi, List.rev_append acc (vi :: f :: rest)
| f :: rest -> loopFormals (f::acc) rest
in
let vi, newformals =
- if where = "^" then let vi = makeit false name in vi, vi :: fdec.sformals
+ if where = "^" && not ghost then let vi = makeit name in vi, vi :: fdec.sformals
else
loopFormals [] fdec.sformals
in
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 71b9b2795cc..b5efeffc565 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -181,7 +181,10 @@ val selfFormalsDecl: State.t
(** state of the table associating formals to each prototype. *)
val makeFormalsVarDecl: ?ghost:bool -> (string * typ * attributes) -> varinfo
- (** creates a new varinfo for the parameter of a prototype. *)
+ (** creates a new varinfo for the parameter of a prototype.
+ By default, this formal variable is not ghost.
+ @modify 19.0-Potassium+dev adds a parameter for ghost status
+ *)
(** Update the formals of a function declaration from its identifier and its
type. For a function definition, use {!Cil.setFormals}.
@@ -581,11 +584,11 @@ val isTypeTagType: logic_type -> bool
val isVariadicListType: typ -> bool
(** Obtain the argument list ([] if None).
- @since Argon+dev Beware that it contains the ghost arguments. *)
+ @since 19.0-Potassium+dev Beware that it contains the ghost arguments. *)
val argsToList:
(string * typ * attributes) list option -> (string * typ * attributes) list
-(** @since Argon+dev
+(** @since 19.0-Potassium+dev
Obtain the argument lists (non-ghost, ghosts) ([], [] if None) *)
val argsToPairOfLists:
(string * typ * attributes) list option ->
@@ -658,7 +661,9 @@ val splitFunctionTypeVI:
The [ghost] argument defaults to [false], and corresponds to the field
[vghost] .
The first unnamed argument specifies whether the varinfo is for a global and
- the second is for formals. *)
+ the second is for formals.
+ @modify 19.0-Potassium adds an optional ghost parameter
+*)
val makeVarinfo:
?source:bool -> ?temp:bool -> ?referenced:bool -> ?ghost:bool -> bool -> bool
-> string -> typ -> varinfo
@@ -668,8 +673,18 @@ val makeVarinfo:
insert this one. If where = "^" then it is inserted first. If where = "$"
then it is inserted last. Otherwise where must be the name of a formal
after which to insert this. By default it is inserted at the end.
+
+ The [ghost] parameter indicates if the variable should be inserted in the
+ list of formals or ghost formals. By default, it takes the ghost status of
+ the function where the formal is inserted. Note that:
+
+ - specifying ghost to false if the function is ghost leads to an error
+ - when [where] is specified, its status must be the same as the formal to
+ insert (else, it cannot be found in the list of ghost or non ghost formals)
+
+ @modify 19.0-Potassium adds the optional ghost parameter
*)
-val makeFormalVar: fundec -> ?where:string -> string -> typ -> varinfo
+val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> string -> typ -> varinfo
(** Make a local variable and add it to a function's slocals and to the given
block (only if insert = true, which is the default).
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
index dd545df87cc..18e26925e70 100644
--- a/tests/cil/insert_formal.ml
+++ b/tests/cil/insert_formal.ml
@@ -6,9 +6,10 @@ class visitor = object
method! vfunc f =
let insert_circ f = Cil.makeFormalVar f ~where:"^" "x" Cil.intType in
let insert_dollar f = Cil.makeFormalVar f ~where:"$" "x" Cil.intType in
- let insert_circ_g f = Cil.makeFormalVar f ~where:"^g" "x" Cil.intType in
- let insert_dollar_g f = Cil.makeFormalVar f ~where:"$g" "x" Cil.intType in
+ let insert_circ_g f = Cil.makeFormalVar f ~ghost:true ~where:"^" "x" Cil.intType in
+ let insert_dollar_g f = Cil.makeFormalVar f ~ghost:true ~where:"$" "x" Cil.intType in
let insert_a f = Cil.makeFormalVar f ~where:"a" "x" Cil.intType in
+ let insert_a_g f = Cil.makeFormalVar f ~ghost:true ~where:"a" "x" Cil.intType in
let circ_list = [
"void_circumflex" ;
"a_circumflex" ;
@@ -31,12 +32,14 @@ class visitor = object
] in
let a_list = [
"a_a" ;
- "ghost_a_a" ;
"a_b_c_a" ;
"b_a_c_a" ;
+ "a_ghost_b_c_a" ;
+ ] in
+ let a_g_list = [
+ "ghost_a_a" ;
"all_ghost_a_b_c_a" ;
"all_ghost_b_a_c_a" ;
- "a_ghost_b_c_a" ;
"b_ghost_a_c_a"
] in
if List.mem f.svar.vname circ_list then ignore(insert_circ f) ;
@@ -44,6 +47,7 @@ class visitor = object
if List.mem f.svar.vname circ_g_list then ignore(insert_circ_g f) ;
if List.mem f.svar.vname dollar_g_list then ignore(insert_dollar_g f) ;
if List.mem f.svar.vname a_list then ignore(insert_a f) ;
+ if List.mem f.svar.vname a_g_list then ignore(insert_a_g f) ;
Cil.DoChildren
end
--
GitLab