diff --git a/Changelog b/Changelog
index 85dedd77b9acfa5cd96c762584d6c5689e437aed..68ec669e4d8cb47b6a27e7f1bed4c66813d86e48 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,8 @@
Open Source Release <next-release>
###############################################################################
+o! Kernel [2024-12-20] Remove Cabs.SEQUENCE statement
+
###############################################################################
Open Source Release 30.0 (Zinc)
###############################################################################
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 68fdd419ca5d5c00cecda14d658c13751e0edb5e..2624f808f3295b20ddd30c873b30b3d85b310f27 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7368,7 +7368,6 @@ and doExp local_env
let findLastComputation = function
s :: _ ->
let rec findLast st = match st.stmt_node with
- | Cabs.SEQUENCE (_, s, _) -> findLast s
| CASE (_, s, _) -> findLast s
| CASERANGE (_, _, s, _) -> findLast s
| LABEL (_, s, _) -> findLast s
@@ -9977,11 +9976,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let res = s2c (mkStmt ~ghost ~valid_sid (Block b)) in
{ res with cases = c.cases }
- | Cabs.SEQUENCE (s1, s2, _) ->
- let c1 = doStatement local_env s1 in
- let c2 = doStatement local_env s2 in
- c1 @@@ (c2, ghost)
-
| Cabs.IF(e, st, sf, _) ->
let st' = doStatement local_env st in
let sf' = doStatement local_env sf in
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index a0c46854694f05d1d36167f224f629b52a582566..a4de9e3fe929b11a6b1b445fbda432941fb36595 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -209,8 +209,6 @@ and pp_raw_stmt fmt = function
| BLOCK (bl, loc1, loc2) ->
fprintf fmt "@[<hov 2>BLOCK loc1(%a), loc2(%a) {%a} @]"
pp_cabsloc loc1 pp_cabsloc loc2 pp_block bl
- | SEQUENCE (stmt1, stmt2, loc) ->
- fprintf fmt "@[<hov 2>SEQUENCE stmt(%a), stmt(%a), loc(%a)@]" pp_stmt stmt1 pp_stmt stmt2 pp_cabsloc loc
| IF (exp, stmt1, stmt2, loc) ->
fprintf fmt "@[<hov 2>IF cond(%a), stmt(%a), stmt(%a), loc(%a)@]"
pp_exp exp pp_stmt stmt1 pp_stmt stmt2 pp_cabsloc loc
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 726864b24c343e33238b37d8701b6025d170fc30..8da3a7d6b25bb701ddb6f56062cf3e1824a4569d 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -435,8 +435,6 @@ and print_statement fmt stat =
| NOP _ -> pp_print_string fmt ";"
| COMPUTATION (exp,_) -> fprintf fmt "%a;" print_expression exp
| BLOCK (blk, _,_) -> print_block fmt blk
- | SEQUENCE (s1, s2,_) ->
- fprintf fmt "%a;@ %a" print_statement s1 print_statement s2
| IF (exp, s1, s2, _) ->
fprintf fmt "@[<hov 2>if@ (@[%a@])@ %a@."
print_expression exp print_substatement s1;
@@ -537,7 +535,6 @@ and print_block fmt blk =
and print_substatement fmt stat =
match stat.stmt_node with
IF _
- | SEQUENCE _
| DOWHILE _ ->
fprintf fmt "@ {@ @[%a@]@ }" print_statement stat
| _ ->
diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml
index 66963031273866350b44e2b1944495623ff6d928..518230655be8e52afbe85a255d63f7608e9189a6 100644
--- a/src/kernel_services/parsetree/cabs.ml
+++ b/src/kernel_services/parsetree/cabs.ml
@@ -199,7 +199,6 @@ and raw_statement =
| NOP of attribute option * cabsloc
| COMPUTATION of expression * cabsloc
| BLOCK of block * cabsloc * cabsloc
- | SEQUENCE of statement * statement * cabsloc
| IF of expression * statement * statement * cabsloc
| WHILE of loop_invariant * expression * statement * cabsloc
| DOWHILE of loop_invariant * expression * statement * cabsloc
diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml
index aaa18bc10163263b177c5293f46a3a219d51fd24..732ce601a40f19b22f7d1896dac95a03df68e7af 100644
--- a/src/kernel_services/parsetree/cabshelper.ml
+++ b/src/kernel_services/parsetree/cabshelper.ml
@@ -167,7 +167,6 @@ let get_statementloc (s : statement) : cabsloc =
| NOP(_, loc) -> loc
| COMPUTATION(_,loc) -> loc
| BLOCK(_,loc,_) -> loc
- | SEQUENCE(_,_,loc) -> loc
| IF(_,_,_,loc) -> loc
| WHILE(_,_,_,loc) -> loc
| DOWHILE(_,_,_,loc) -> loc
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index ed9fa5846312b0493a04c8ec62d163c47e29c714..2ca799eab5bf4d4b798424e531bef43985c75bbb 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -292,10 +292,6 @@ and childrenStatement vis s =
| BLOCK (b, l, l') ->
let b' = visitCabsBlock vis b in
if b' != b then {s with stmt_node = BLOCK (b', l, l')} else s
- | SEQUENCE (s1, s2, l) ->
- let s1' = vs l s1 in
- let s2' = vs l s2 in
- if s1' != s1 || s2' != s2 then {s with stmt_node = SEQUENCE (s1', s2', l)} else s
| IF (e, s1, s2, l) ->
let e' = ve e in
let s1' = vs l s1 in
diff --git a/src/plugins/metrics/metrics_cabs.ml b/src/plugins/metrics/metrics_cabs.ml
index cd604b283ee4fa2b2c150f4c20f07fa18dee2c33..b928284ac8f5f53cb1cc59bed4eaf92f6d2c8cee 100644
--- a/src/plugins/metrics/metrics_cabs.ml
+++ b/src/plugins/metrics/metrics_cabs.ml
@@ -207,7 +207,6 @@ class metricsCabsVisitor = object(self)
| COMPGOTO _ -> self#incr_both_metrics incr_gotos;
| DEFINITION _
| ASM _
- | SEQUENCE _
| TRY_CATCH _
| CODE_ANNOT _
| CODE_SPEC _ -> ());
@@ -348,10 +347,6 @@ module Halstead = struct
update_val_incr "{" operator_tbl.otherop_tbl;
update_val_incr "}" operator_tbl.otherop_tbl;
Cil.DoChildren;
- | SEQUENCE _ ->
- print_string "seq\n";
- update_val_incr ";" operator_tbl.otherop_tbl;
- Cil.DoChildren;
| IF _ -> self#add_paren (); reserved "if";
| WHILE _ -> self#add_paren (); reserved "while";
| DOWHILE _ ->