diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml
index 6e9b5379c30b37d53e7593165422781bf20e4da1..bf2949535759afab05435ca2840746b3aede3b5b 100644
--- a/src/kernel_services/analysis/destructors.ml
+++ b/src/kernel_services/analysis/destructors.ml
@@ -162,12 +162,7 @@ class vis flag = object(self)
Cil.DoChildrenPost post
method! vstmt_aux s =
- let inspect_closed_blocks b =
- (* blocks are sorted from innermost to outermost. The fold_left
- will give us the list in appropriate order for add_destructors
- which expects variable from oldest to newest.
- *)
- let vars = List.fold_left (fun acc b -> b.blocals @ acc) [] b in
+ let insert_destructors vars =
let has_destructors, stmts = add_destructors vars in
if has_destructors then begin
flag:=true;
@@ -184,6 +179,29 @@ class vis flag = object(self)
end;
Cil.SkipChildren
in
+ let vars_from_blocks blocks =
+ List.fold_left (fun acc b -> b.blocals @ acc) [] blocks
+ in
+ let vars_from_edge s succ =
+ let closed_blocks = Kernel_function.blocks_closed_by_edge s succ in
+ (* blocks are sorted from innermost to outermost. The fold_left
+ will give us the list in appropriate order for add_destructors
+ which expects variable from oldest to newest.
+ *)
+ let current_block = Kernel_function.common_block s succ in
+ let vars = vars_from_blocks closed_blocks in
+ (* for the common block, we have to check whether we are backjumping
+ over some definitions in the middle of the block, that is
+ definitions that dominate s but not its successor.
+ *)
+ let is_backjump_var v =
+ v.vdefined &&
+ let def = Cil.find_def_stmt current_block v in
+ Dominators.dominates def s && not (Dominators.dominates def succ)
+ in
+ let current_vars = List.filter is_backjump_var current_block.blocals in
+ current_vars @ vars
+ in
let abort_if_non_trivial_type kind v =
if Cil.hasAttribute Cabs2cil.frama_c_destructor v.vattr then
Kernel.abort
@@ -208,10 +226,17 @@ class vis flag = object(self)
let inspect_local_vars kind b s lv =
List.iter (check_def_domination kind b s) lv
in
+ let inspect_var_current_block kind b s succ v =
+ if v.vdefined then begin
+ let def = Cil.find_def_stmt b v in
+ if Kernel_function.is_between b s def succ then
+ (* we are forward-jumping over def *)
+ abort_if_non_trivial_type kind v
+ end else abort_if_non_trivial_type kind v
+ in
let treat_jump_close s =
match s.succs with
- | [ succ ] ->
- inspect_closed_blocks (Kernel_function.blocks_closed_by_edge s succ)
+ | [ succ ] -> insert_destructors (vars_from_edge s succ)
| _ ->
Kernel.fatal ~current:true
"%a in function %a is expected to have a single successor"
@@ -221,21 +246,11 @@ class vis flag = object(self)
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
- 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
+ let current_block = Kernel_function.common_block s succ in
+ List.iter (fun b -> inspect_local_vars kind b succ b.blocals) blocks;
+ List.iter
+ (inspect_var_current_block kind current_block s succ)
+ current_block.blocals
in
let treat_jump_open k s = List.iter (treat_succ_open k s) s.succs in
match s.skind with
@@ -254,7 +269,8 @@ class vis flag = object(self)
| Switch _ -> treat_jump_open "switch" s; Cil.DoChildren
(* jump outside of the function: all currently opened blocks are closed. *)
| Return _ | Throw _ ->
- inspect_closed_blocks (Kernel_function.find_all_enclosing_blocks s)
+ insert_destructors
+ (vars_from_blocks (Kernel_function.find_all_enclosing_blocks s))
(* no jump yet, visit children *)
| _ -> Cil.DoChildren
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index 8e876e4d23bfee17053055c823884a4565903dd8..35ee82a3805dd515db5b4823bf4bbe908e088a8c 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -211,6 +211,94 @@ let find_all_enclosing_blocks s =
let table = compute () in
let (_,_,b) = Datatype.Int.Hashtbl.find table s.sid in b
+let find_stmt_in_block b s =
+ let has_stmt l =
+ List.exists (fun (s',_,_,_,_) -> Cil_datatype.Stmt.equal s s') l
+ in
+ let rec aux = function
+ | [] ->
+ Kernel.fatal "statement %a is not inside block@\n%a"
+ Cil_printer.pp_stmt s Cil_printer.pp_block b
+ | s' :: _ when Cil_datatype.Stmt.equal s s' -> s'
+ | { skind = UnspecifiedSequence l } as s':: _ when has_stmt l -> s'
+ | _ :: l -> aux l
+ in aux b.bstmts
+
+let find_stmt_of_block outer inner =
+ let rec is_stmt_of_block s =
+ match s.skind with
+ | Block b -> b == inner
+ | If (_,b1,b2,_) -> b1 == inner || b2 == inner
+ | Switch (_,b,_,_) -> b == inner
+ | Loop (_,b,_,_,_) -> b == inner
+ | UnspecifiedSequence l -> is_stmt_of_unspecified l
+ | TryCatch (b, l, _) ->
+ b == inner || List.exists (fun (_,b) -> b == inner) l
+ | TryFinally (b1,b2,_) -> b1 == inner || b2 == inner
+ | TryExcept (b1,_,b2,_) -> b1 == inner || b2 == inner
+ | _ -> false
+ and is_stmt_of_unspecified l =
+ List.exists (fun (s,_,_,_,_) -> is_stmt_of_block s) l
+ in
+ try
+ List.find is_stmt_of_block outer.bstmts
+ with Not_found ->
+ Kernel.fatal "inner block@\n%a@\nis not a direct child of outer block@\n%a"
+ Cil_printer.pp_block inner Cil_printer.pp_block outer
+
+let find_enclosing_stmt_in_block b s =
+ let blocks = find_all_enclosing_blocks s in
+ let rec aux prev l =
+ match l, prev with
+ | [], _ ->
+ Kernel.fatal "statement %a is not part of block@\n%a"
+ Cil_printer.pp_stmt s Cil_printer.pp_block b
+ | b' :: _, None when b' == b -> find_stmt_in_block b s
+ | b' :: _, Some prev when b' == b -> find_stmt_of_block b prev
+ | b' :: l, _ -> aux (Some b') l
+ in
+ aux None blocks
+
+let is_between b s1 s2 s3 =
+ let s1 = find_enclosing_stmt_in_block b s1 in
+ let s2 = find_enclosing_stmt_in_block b s2 in
+ let s3 = find_enclosing_stmt_in_block b s3 in
+ let rec aux has_s1 l =
+ match l with
+ | [] ->
+ Kernel.fatal
+ "Unexpected end of block while looking for %a"
+ Cil_printer.pp_stmt s3
+ | s :: l when Cil_datatype.Stmt.equal s s1 -> aux true l
+ | s :: _ when Cil_datatype.Stmt.equal s s2 -> has_s1
+ | s :: _ when Cil_datatype.Stmt.equal s s3 -> false
+ | _ :: l -> aux has_s1 l
+ in
+ aux false b.bstmts
+
+let common_block s1 s2 =
+ let kf1 = find_englobing_kf s1 in
+ let kf2 = find_englobing_kf s2 in
+ if not (equal kf1 kf2) then
+ Kernel.fatal
+ "cannot find a common block for statements occurring \
+ in two distinct functions";
+ let b1 = find_all_enclosing_blocks s1 in
+ let b2 = find_all_enclosing_blocks s2 in
+ let rec aux last l1 l2 =
+ match l1,l2 with
+ | [], _ | _, [] -> last
+ | b1 :: l1, b2 :: l2 when b1 == b2 -> aux b1 l1 l2
+ | _ :: _, _ :: _ -> last
+ in
+ match List.rev b1, List.rev b2 with
+ | [], _ | _, [] ->
+ Kernel.fatal "Statement not contained in any block"
+ | b1 :: l1, b2 :: l2 when b1 == b2 -> aux b1 l1 l2
+ | _ :: _, _ :: _ ->
+ Kernel.fatal
+ "Statements do not share their function body as outermost common block"
+
let () = Globals.find_all_enclosing_blocks := find_all_enclosing_blocks
let stmt_in_loop kf stmt =
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index 18c1dac1287a83abf9be394c92e837802c8c22c9..dc999bb6dc809590ce5b9f4c0c9c638eaecbf75c 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -108,8 +108,16 @@ val blocks_opened_by_edge: stmt -> stmt -> block list
@raise Invalid_argument if [s2] is not a successor of [s1] in the cfg.
@since Magnesium-20151001 *)
+val common_block: stmt -> stmt -> block
+(** [common_block s1 s2] returns the innermost block that contains
+ both [s1] and [s2], provided the statements belong to the same function.
+ raises a fatal error if this is not the case.
+
+ @since Frama-C+dev
+*)
+
val stmt_in_loop: t -> stmt -> bool
- (** [stmt_in_loop kf stmt] is [true] iff [stmt] strictly
+ (** [stmt_in_loop kf stmt] is [true] iff [stmt] strictly
occurs in a loop of [kf].
@since Oxygen-20120901 *)
@@ -135,6 +143,27 @@ val var_is_in_scope: stmt -> varinfo -> bool
@since Frama-C+dev *)
+val find_enclosing_stmt_in_block: block -> stmt -> stmt
+ (** [find_enclosing_stmt_in_block b s] returns the statements [s']
+ inside [b.bstmts] that contains [s]. It might be [s] itself, but also
+ an inner block (recursively) containing [s].
+
+ @raise AbortFatal if [b] is not equal to [find_enclosing_block s]
+ @since Frama-C+dev
+ *)
+
+val is_between: block -> stmt -> stmt -> stmt -> bool
+(** [is_between b s1 s2 s3] returns [true] if the statement [s2] appears
+ between [s1] and [s3] inside the [b.bstmts] list. All three statements
+ must actually occur in [b.bstmts], either directly or indirectly
+ (see {!Kernel_function.find_enclosing_stmt_in_block}).
+
+ @raise AbortFatal if pre-conditions are not met.
+
+ @since Frama-C+dev
+*)
+
+
(* ************************************************************************* *)
(** {2 Checkers} *)
(* ************************************************************************* *)
diff --git a/tests/syntax/oracle/vla_goto_same_block_above.res.oracle b/tests/syntax/oracle/vla_goto_same_block_above.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9d5bd2d88c817afd6daf3fab6976ca2c35b17ddc
--- /dev/null
+++ b/tests/syntax/oracle/vla_goto_same_block_above.res.oracle
@@ -0,0 +1,64 @@
+[kernel] Parsing tests/syntax/vla_goto_same_block_above.i (no preprocessing)
+/* Generated by Frama-C */
+int volatile nondet;
+/*@ assigns \nothing;
+ frees p; */
+ __attribute__((__FC_BUILTIN__)) void __fc_vla_free(void *p);
+
+/*@ assigns \result;
+ assigns \result \from \nothing;
+ allocates \result; */
+ __attribute__((__FC_BUILTIN__)) void *__fc_vla_alloc(unsigned int size);
+
+int main(void)
+{
+ int __retres;
+ unsigned int __lengthof_vla;
+ int i = 42;
+ toto: ;
+ /*@ assert alloca_bounds: 0 < sizeof(char) * i ≤ 4294967295; */ ;
+ __lengthof_vla = (unsigned int)i;
+ char *vla = __fc_vla_alloc(sizeof(char) * __lengthof_vla);
+ if (nondet) {
+ __fc_vla_free((void *)vla);
+ goto toto;
+ }
+ __retres = 0;
+ __fc_vla_free((void *)vla);
+ return __retres;
+}
+
+int f(void)
+{
+ int __retres;
+ unsigned int __lengthof_vla;
+ int i = 42;
+ if (nondet) toto: ;
+ /*@ assert alloca_bounds: 0 < sizeof(char) * i ≤ 4294967295; */ ;
+ __lengthof_vla = (unsigned int)i;
+ char *vla = __fc_vla_alloc(sizeof(char) * __lengthof_vla);
+ if (nondet) {
+ __fc_vla_free((void *)vla);
+ goto toto;
+ }
+ __retres = 0;
+ __fc_vla_free((void *)vla);
+ return __retres;
+}
+
+int g(void)
+{
+ int __retres;
+ unsigned int __lengthof_vla;
+ int i = 42;
+ /*@ assert alloca_bounds: 0 < sizeof(char) * i ≤ 4294967295; */ ;
+ __lengthof_vla = (unsigned int)i;
+ char *vla = __fc_vla_alloc(sizeof(char) * __lengthof_vla);
+ if (nondet) toto: ;
+ if (nondet) goto toto;
+ __retres = 0;
+ __fc_vla_free((void *)vla);
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/vla_goto_same_block_below.res.oracle b/tests/syntax/oracle/vla_goto_same_block_below.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b61b6e96000ef532c750da0b271ca5ad84ddcfd8
--- /dev/null
+++ b/tests/syntax/oracle/vla_goto_same_block_below.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/syntax/vla_goto_same_block_below.i (no preprocessing)
+[kernel] User Error: tests/syntax/vla_goto_same_block_below.i:6, cannot jump from goto statement bypassing initialization of variable vla, declared at tests/syntax/vla_goto_same_block_below.i:9
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/vla_goto_same_block_above.i b/tests/syntax/vla_goto_same_block_above.i
new file mode 100644
index 0000000000000000000000000000000000000000..11704dbc2a72a5efeb51ac7ae4ac0b0cc237b9b9
--- /dev/null
+++ b/tests/syntax/vla_goto_same_block_above.i
@@ -0,0 +1,24 @@
+volatile int nondet ;
+int main() {
+ int i = 42 ;
+ toto : ;
+ char vla[i] ;
+ if (nondet) goto toto ;
+ return 0 ;
+}
+
+int f() {
+ int i = 42 ;
+ if (nondet) { toto : ; }
+ char vla[i] ;
+ if (nondet) goto toto ;
+ return 0 ;
+}
+
+int g() {
+ int i = 42 ;
+ char vla[i] ;
+ if (nondet) { toto : ; }
+ if (nondet) goto toto ;
+ return 0 ;
+}
diff --git a/tests/syntax/vla_goto_same_block_below.i b/tests/syntax/vla_goto_same_block_below.i
new file mode 100644
index 0000000000000000000000000000000000000000..3e163f3bb8227dafc50fa189d2842831938ebf39
--- /dev/null
+++ b/tests/syntax/vla_goto_same_block_below.i
@@ -0,0 +1,15 @@
+volatile int nondet ;
+
+int main() {
+
+int i = 42;
+if (nondet) goto toto; // KO: we are jumping over
+ // a constructor/destructor definition
+
+char vla[i];
+
+toto: ;
+
+return 0;
+
+}