From 1dcdf53dba809734776693d95d09e2079b9d699e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 25 Feb 2019 11:38:19 +0100
Subject: [PATCH] [Kernel] Fix: rejects more gotos that bypass the
initialization of a VLA.
Also inspects the VLA initializations of the destination block, even if it is
not a block opened by the jump.
---
src/kernel_services/analysis/destructors.ml | 17 ++++++++++++++++-
tests/syntax/oracle/vla_goto3.res.oracle | 3 +++
tests/syntax/vla_goto3.i | 10 ++++++++++
3 files changed, 29 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/oracle/vla_goto3.res.oracle
create mode 100644 tests/syntax/vla_goto3.i
diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml
index 366440d2a58..6e9b5379c30 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 00000000000..6278462c8d2
--- /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 00000000000..53ffedf5381
--- /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;
+}
--
GitLab