diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml
index 366440d2a58930a27ac6f61d9191bd4c32af8856..6e9b5379c30b37d53e7593165422781bf20e4da1 100644
--- a/src/kernel_services/analysis/destructors.ml
+++ b/src/kernel_services/analysis/destructors.ml
@@ -219,8 +219,23 @@ class vis flag = object(self)
           Kernel_function.pretty (Extlib.the self#current_kf)
     in
     let treat_succ_open kind s succ =
+      (* The jump must not bypass a vla initialization in the opened blocks. *)
       let blocks = Kernel_function.blocks_opened_by_edge s succ in
-      List.iter (fun b -> inspect_local_vars kind b succ b.blocals) blocks
+      if blocks <> []
+      then List.iter (fun b -> inspect_local_vars kind b succ b.blocals) blocks
+      else begin
+        (* If there is no opened block, check that the jump does not bypass a
+           vla initialization in the destination block. [s] is in this block. *)
+        let block = Kernel_function.find_enclosing_block succ in
+        (* Does the definition of variable [v] dominates the statement [s]? *)
+        let dominate_s v =
+          v.vdefined && Dominators.dominates (Cil.find_def_stmt block v) s
+        in
+        (* Only consider variables defined after statement [s]. *)
+        let lvs = List.filter (fun v -> not (dominate_s v)) block.blocals in
+        (* Check that they are not defined before statement [succ]. *)
+        inspect_local_vars kind block succ lvs
+      end
     in
     let treat_jump_open k s = List.iter (treat_succ_open k s) s.succs in
     match s.skind with
diff --git a/tests/syntax/oracle/vla_goto3.res.oracle b/tests/syntax/oracle/vla_goto3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6278462c8d29811a497f44fe505f53fb69ae7b1e
--- /dev/null
+++ b/tests/syntax/oracle/vla_goto3.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/syntax/vla_goto3.i (no preprocessing)
+[kernel] User Error: tests/syntax/vla_goto3.i:5, cannot jump from goto statement bypassing initialization of variable vla, declared at tests/syntax/vla_goto3.i:6
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/vla_goto3.i b/tests/syntax/vla_goto3.i
new file mode 100644
index 0000000000000000000000000000000000000000..53ffedf53814469ef1c76dcd7caeffdbce744189
--- /dev/null
+++ b/tests/syntax/vla_goto3.i
@@ -0,0 +1,10 @@
+volatile int nondet;
+
+int main () {
+  int i = 42;
+  if (nondet) goto end; // Invalid goto, as it skips the initialization of vla.
+  char vla[i];
+  if (nondet) return 1;
+ end:
+  return 0;
+}