diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 4342827a938e1b64fc3c85c07864b9cbf2191e3c..0edffb0dd95d3c08071125f6d65856aa016648ff 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 4372cfad7fe4f305abaa5f647ef83af0f9b5aff8..ae92a0c24ed9f2fa5bb8db649f1a52031fee9632 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 5a8a92ffbbfc84175734c192efd10b91bd0502b8..a7fd07bd903055bc33815aa8928b0413ae558fff 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 71aa6b65371ee2f471ca253776de7d08da115dc9..a01a05090b9c708433809e2abf97a3636d0d9474 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 d27c84466aac76b779e1903f6b28e06e2edbbf0c..2d486b59e30b7e686e1ddab0b2eea6e1ec6dd1c2 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 d37c1ef006064bd984d5507aaec36021433b6b31..e7f0ff59522ab5a5417b451cd95cc2ed0a566ba8 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 bd3a6e656999a09ae0bf67088be27fbbe017a165..1db894c1d19b942e2cdf30e141e92f11ab772613 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 3ae608c093eb7d7dcf5ff55de45a546fc49ca19d..2469b531c7773585583ee91089b82726b98b869b 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 \