diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 24e66b85e25939b352aa1bd6d7f397c2d8384ab0..6e20505e30c0e5f477483bc089f25d8b3f1cd58c 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4137,8 +4137,6 @@ let rec doSpecList ghost (suggestedAnonName: string)
| Cabs.SpecCV cv -> cvattrs := cv :: !cvattrs; acc
| Cabs.SpecAttr a -> attrs := a :: !attrs; acc
| Cabs.SpecType ts -> ts :: acc
- | Cabs.SpecPattern _ ->
- Kernel.fatal ~current:true "SpecPattern in cabs2cil input"
in
(* Now scan the list and collect the type specifiers. Preserve the order *)
let tspecs = List.fold_right doSpecElem specs [] in
@@ -7306,10 +7304,6 @@ and doExp local_env
(mkCast ~newt:voidPtrType (integer ~loc addrval)) voidPtrType
end
- | Cabs.EXPR_PATTERN _ ->
- Kernel.fatal ~current:true "EXPR_PATTERN in cabs2cil input"
-
-
| Cabs.GENERIC (ce, assocs) ->
let (_, _, control_exp, control_t) = doExp local_env asconst ce AType in
match Cil.lvalue_conversion control_t with
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index 6ad87a9b83773f8886a0a4ec345e0b3d4a66057e..a2118a4874aaf4300244b5e80e151e6ba15f3542 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -34,11 +34,6 @@ let pp_storage fmt = function
| EXTERN -> fprintf fmt "EXTERN"
| REGISTER -> fprintf fmt "REGISTER"
-let pp_fun_spec fmt = function
- | INLINE -> fprintf fmt "INLINE"
- | VIRTUAL -> fprintf fmt "VIRTUAL"
- | EXPLICIT -> fprintf fmt "EXPLICIT"
-
let pp_cvspec fmt = function
| CV_CONST -> fprintf fmt "CV_CONST"
| CV_VOLATILE -> fprintf fmt "CV_VOLATILE"
@@ -102,7 +97,6 @@ and pp_spec_elem fmt = function
| SpecStorage storage -> fprintf fmt "SpecStorage %a" pp_storage storage
| SpecInline -> fprintf fmt "SpecInline"
| SpecType typeSpec -> fprintf fmt "SpecType %a" pp_typeSpecifier typeSpec
- | SpecPattern s -> fprintf fmt "SpecPattern %s" s
and pp_spec fmt spec_elems =
fprintf fmt "@[<hv 2>{" ;
@@ -362,7 +356,6 @@ and pp_exp_node fmt = function
| MEMBEROFPTR (exp, s) ->
fprintf fmt "MEMBEROFPTR(%a,%s)" pp_exp exp s
| GNU_BODY bl -> fprintf fmt "GNU_BODY %a" pp_block bl
- | EXPR_PATTERN s -> fprintf fmt "EXPR_PATTERN %s" s
| GENERIC (exp, generic_assoc_list) ->
fprintf fmt "GENERIC(%a,%a)"
pp_exp exp
diff --git a/src/kernel_services/ast_printing/cabs_debug.mli b/src/kernel_services/ast_printing/cabs_debug.mli
index 55f0740c7b1fb98497a7e4f201046bbb634ada74..fae397a8850f2ce27a1d687664d2032fe7faefe5 100644
--- a/src/kernel_services/ast_printing/cabs_debug.mli
+++ b/src/kernel_services/ast_printing/cabs_debug.mli
@@ -26,7 +26,6 @@ open Format
val pp_cabsloc : formatter -> cabsloc -> unit
val pp_storage : formatter -> storage -> unit
-val pp_fun_spec : formatter -> funspec -> unit
val pp_cvspec : formatter -> cvspec -> unit
val pp_const : formatter -> constant -> unit
val pp_labels : formatter -> string list -> unit
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 91c72cd16cd37c991f77049e2ec7af0d7014f7d6..c91565ca35f36bb5ca21c977b4a02442d3621bd9 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -166,7 +166,6 @@ let get_operator exp =
| MEMBEROF (_, _) -> ("", 15)
| MEMBEROFPTR (_, _) -> ("", 15)
| GNU_BODY _ -> ("", 17)
- | EXPR_PATTERN _ -> ("", 16) (* sm: not sure about this *)
| GENERIC _ -> ("", 16)
(*
@@ -197,7 +196,6 @@ let rec print_specifiers fmt (specs: spec_elem list) =
| SpecCV CV_GHOST -> fprintf fmt "\\ghost"
| SpecAttr al -> print_attribute fmt al
| SpecType bt -> print_type_spec fmt bt
- | SpecPattern name -> fprintf fmt "@@specifier(%s)" name
in
Pretty_utils.pp_list ~sep:"@ " print_spec_elem fmt specs
@@ -413,7 +411,6 @@ and print_expression_level (lvl: int) fmt (exp : expression) =
fprintf fmt "%a->%s"
print_expression exp fld
| GNU_BODY blk -> fprintf fmt "(@[%a@])" print_block blk
- | EXPR_PATTERN (name) -> fprintf fmt "@@expr(%s)" name
| COMMA l -> pp_list ~sep:",@ " print_expression fmt l
| GENERIC (control_exp, typ_exps) ->
fprintf fmt "_Generic(@[%a,@ %a@])" print_expression control_exp
diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml
index d5ace68bc0206150c02c11156ab214b81a741678..e0ac62c186971ec3843d4fdeadbd86d414856b33 100644
--- a/src/kernel_services/parsetree/cabs.ml
+++ b/src/kernel_services/parsetree/cabs.ml
@@ -77,9 +77,6 @@ type typeSpecifier = (* Merge all specifiers into one type *)
and storage =
| NO_STORAGE | AUTO | STATIC | EXTERN | REGISTER
-and funspec =
- | INLINE | VIRTUAL | EXPLICIT
-
and cvspec =
| CV_CONST | CV_VOLATILE | CV_RESTRICT
| CV_ATTRIBUTE_ANNOT of string | CV_GHOST
@@ -96,7 +93,6 @@ and spec_elem =
| SpecStorage of storage
| SpecInline
| SpecType of typeSpecifier
- | SpecPattern of string (* specifier pattern variable *)
(* decided to go ahead and replace 'spec_elem list' with specifier *)
and specifier = spec_elem list
@@ -311,7 +307,6 @@ and cabsexp =
| MEMBEROF of expression * string
| MEMBEROFPTR of expression * string
| GNU_BODY of block
- | EXPR_PATTERN of string (* pattern variable, and name *)
| GENERIC of (expression * (((specifier * decl_type) option * expression) list))
and constant =
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index edece4b957f1c914740a4f5cc7fbf4ec48991279..ce24e029b0f10f339494fad75afab103250e18f5 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -155,7 +155,7 @@ and childrenTypeSpecifier vis ts =
and childrenSpecElem (vis: cabsVisitor) (se: spec_elem) : spec_elem =
match se with
- SpecTypedef | SpecInline | SpecStorage _ | SpecPattern _ -> se
+ SpecTypedef | SpecInline | SpecStorage _ -> se
| SpecCV _ -> se (* cop out *)
| SpecAttr a -> begin
let al' = visitCabsAttribute vis a in
@@ -482,7 +482,6 @@ and childrenExpression vis e =
| GNU_BODY b ->
let b' = visitCabsBlock vis b in
if b' != b then { e with expr_node = GNU_BODY b' } else e
- | EXPR_PATTERN _ -> e
| GENERIC (e, generic_assocs) ->
let e' = ve e in
let exps = List.map snd generic_assocs in
diff --git a/src/plugins/metrics/metrics_cabs.ml b/src/plugins/metrics/metrics_cabs.ml
index 791a051e8399e66b7ec118552fa9be2da2d2dea2..52eef132a1d43b9112912ec27824ee3eaa64a4ff 100644
--- a/src/plugins/metrics/metrics_cabs.ml
+++ b/src/plugins/metrics/metrics_cabs.ml
@@ -168,7 +168,6 @@ class metricsCabsVisitor = object(self)
| MEMBEROF _
| MEMBEROFPTR _
| GNU_BODY _
- | EXPR_PATTERN _
| GENERIC _ -> ());
Cil.DoChildren