From e31f765bc48e290d07e40d7bed0f0d9f671fa495 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 29 Jan 2021 15:49:24 +0100
Subject: [PATCH] [Variadic] Move Extends.Cil function to an apropriate
location
---
src/kernel_services/ast_queries/cil.ml | 2 ++
src/kernel_services/ast_queries/cil.mli | 6 ++++++
src/plugins/variadic/classify.ml | 6 +++++-
src/plugins/variadic/extends.ml | 12 ------------
src/plugins/variadic/extends.mli | 12 ------------
src/plugins/variadic/format_typer.ml | 12 ++++++------
src/plugins/variadic/standard.ml | 1 -
src/plugins/variadic/translate.ml | 2 +-
8 files changed, 20 insertions(+), 33 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 4342827a938..0edffb0dd95 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -78,6 +78,8 @@ let set_dependencies_of_ast, dependency_on_ast =
let voidType = Cil_const.voidType
let intType = TInt(IInt,[])
let uintType = TInt(IUInt,[])
+let shortType = TInt(IShort, [])
+let ushortType = TInt(IUShort, [])
let longType = TInt(ILong,[])
let longLongType = TInt(ILongLong,[])
let ulongType = TInt(IULong,[])
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 4372cfad7fe..ae92a0c24ed 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -303,6 +303,12 @@ val intType: typ
(** unsigned int *)
val uintType: typ
+(** short *)
+val shortType : typ
+
+(** unsigned short *)
+val ushortType : typ
+
(** long *)
val longType: typ
diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml
index 5a8a92ffbbf..a7fd07bd903 100644
--- a/src/plugins/variadic/classify.ml
+++ b/src/plugins/variadic/classify.ml
@@ -152,9 +152,13 @@ let classify_std env vi = match vi.vname with
(* Anything else *)
| _ -> Unknown
+let is_variadic_function vi =
+ match Cil.unrollType vi.vtype with
+ | TFun (_, _, b, _) -> b
+ | _ -> false
let classify env vi =
- if Extends.Cil.is_variadic_function vi then begin
+ if is_variadic_function vi then begin
Self.result ~level:2 ~current:true
"Declaration of variadic function %s." vi.vname;
Some {
diff --git a/src/plugins/variadic/extends.ml b/src/plugins/variadic/extends.ml
index 71aa6b65371..a01a05090b9 100644
--- a/src/plugins/variadic/extends.ml
+++ b/src/plugins/variadic/extends.ml
@@ -40,18 +40,6 @@ module Typ = struct
List.length (params typ)
end
-module Cil = struct
- include Cil
-
- let shortType = TInt(IShort, [])
- let ushortType = TInt(IUShort, [])
-
- let is_variadic_function vi =
- match Cil.unrollType vi.vtype with
- | TFun (_, _, b, _) -> b
- | _ -> false
-end
-
module List = struct
include List
diff --git a/src/plugins/variadic/extends.mli b/src/plugins/variadic/extends.mli
index d27c84466aa..2d486b59e30 100644
--- a/src/plugins/variadic/extends.mli
+++ b/src/plugins/variadic/extends.mli
@@ -31,18 +31,6 @@ module Typ : sig
val params_count : typ -> int
end
-module Cil : sig
- include module type of Cil
-
- val shortType : typ
- val ushortType : typ
-
- (** @return [true] if varinfo is a variadic function, [false] if it
- is a non-variadic function or if it is not a function. *)
- val is_variadic_function : varinfo -> bool
-end
-
-
module List : sig
include module type of List
diff --git a/src/plugins/variadic/format_typer.ml b/src/plugins/variadic/format_typer.ml
index d37c1ef0060..e7f0ff59522 100644
--- a/src/plugins/variadic/format_typer.ml
+++ b/src/plugins/variadic/format_typer.ml
@@ -47,7 +47,7 @@ let type_f_specifier ?find_typedef spec =
match spec.f_conversion_specifier, spec.f_length_modifier with
| #signed_specifier, None -> Cil.intType
| #signed_specifier, Some `hh -> Cil.scharType
- | #signed_specifier, Some `h -> Extends.Cil.shortType
+ | #signed_specifier, Some `h -> Cil.shortType
| #signed_specifier, Some `l -> Cil.longType
| #signed_specifier, Some `ll -> Cil.longLongType
| #signed_specifier, Some `j -> get_typedef ?find_typedef "intmax_t"
@@ -55,7 +55,7 @@ let type_f_specifier ?find_typedef spec =
| #signed_specifier, Some `t -> get_typedef ?find_typedef "ptrdiff_t"
| #unsigned_specifier, None -> Cil.uintType
| #unsigned_specifier, Some `hh -> Cil.ucharType
- | #unsigned_specifier, Some `h -> Extends.Cil.ushortType
+ | #unsigned_specifier, Some `h -> Cil.ushortType
| #unsigned_specifier, Some `l -> Cil.ulongType
| #unsigned_specifier, Some `ll -> Cil.ulongLongType
| #unsigned_specifier, Some `j -> get_typedef ?find_typedef "uintmax_t"
@@ -71,7 +71,7 @@ let type_f_specifier ?find_typedef spec =
| `p, None -> Cil.voidPtrType
| `n, None -> ptr Cil.intType
| `n, Some `hh -> ptr Cil.scharType
- | `n, Some `h -> ptr Extends.Cil.shortType
+ | `n, Some `h -> ptr Cil.shortType
| `n, Some `l -> ptr Cil.longType
| `n, Some `ll -> ptr Cil.longLongType
| `n, Some `j -> ptr (get_typedef ?find_typedef "intmax_t")
@@ -83,7 +83,7 @@ let type_s_specifier ?find_typedef spec =
match spec.s_conversion_specifier, spec.s_length_modifier with
| #signed_specifier, None -> ptr Cil.intType
| #signed_specifier, Some `hh -> ptr Cil.scharType
- | #signed_specifier, Some `h -> ptr Extends.Cil.shortType
+ | #signed_specifier, Some `h -> ptr Cil.shortType
| #signed_specifier, Some `l -> ptr Cil.longType
| #signed_specifier, Some `ll -> ptr Cil.longLongType
| #signed_specifier, Some `j -> ptr (get_typedef ?find_typedef "intmax_t")
@@ -91,7 +91,7 @@ let type_s_specifier ?find_typedef spec =
| #signed_specifier, Some `t -> ptr (get_typedef ?find_typedef "ptrdiff_t")
| #unsigned_specifier, None -> ptr Cil.uintType
| #unsigned_specifier, Some `hh -> ptr Cil.ucharType
- | #unsigned_specifier, Some `h -> ptr Extends.Cil.ushortType
+ | #unsigned_specifier, Some `h -> ptr Cil.ushortType
| #unsigned_specifier, Some `l -> ptr Cil.ulongType
| #unsigned_specifier, Some `ll -> ptr Cil.ulongLongType
| #unsigned_specifier, Some `j -> ptr (get_typedef ?find_typedef "uintmax_t")
@@ -105,7 +105,7 @@ let type_s_specifier ?find_typedef spec =
| `p, None -> ptr (Cil.voidPtrType)
| `n, None -> ptr Cil.intType
| `n, Some `hh -> ptr Cil.scharType
- | `n, Some `h -> ptr Extends.Cil.shortType
+ | `n, Some `h -> ptr Cil.shortType
| `n, Some `l -> ptr Cil.longType
| `n, Some `ll -> ptr Cil.longLongType
| `n, Some `j -> ptr (get_typedef ?find_typedef "intmax_t")
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index bd3a6e65699..1db894c1d19 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -23,7 +23,6 @@
open Cil_types
open Va_types
open Options
-module Cil = Extends.Cil
module List = Extends.List
module Typ = Extends.Typ
module Build = Va_build
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 3ae608c093e..2469b531c77 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -233,7 +233,7 @@ let translate_variadics (file : file) =
method! vexpr exp =
begin match exp.enode with
| AddrOf (Var vi, NoOffset)
- when Extends.Cil.is_variadic_function vi && is_framac_builtin vi ->
+ when Classify.is_variadic_function vi && is_framac_builtin vi ->
Self.not_yet_implemented
~source:(fst exp.eloc)
"The variadic plugin doesn't handle calls to a pointer to the \
--
GitLab