From 96cddc05697836b004fdad461adad31a0b2e527e Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 10 Oct 2023 11:03:49 +0200
Subject: [PATCH] [oneret] More explanations of the problem we try to solve.
---
src/kernel_internals/typing/oneret.ml | 22 ++++++++++++++++------
1 file changed, 16 insertions(+), 6 deletions(-)
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index 7c78d2dac0a..6806eed86d6 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -120,12 +120,22 @@ let collect_returns (ca : Cil_types.code_annotation) =
| _ -> []
let encapsulate_local_vars f =
- (* we must ensure that our gotos to the end of the function do not
- bypass declaration of objects with destructors, or there will be
- issues when inserting the destructor calls. If needed, enclose
- the main body (except return and the declaration of the retvar)
- inside its own block.
- *)
+ (* We must ensure that our gotos to the end of the function do not bypass
+ declarations of objects with destructors, or we may miss to insert the
+ corresponding destructor calls. Here is an example, with T a class:
+
+ extern void Ctor(T* x);
+
+ int f(void) {
+ goto L;
+ T __attribute__((__fc_destructor)) x;
+ Ctor(&x);
+ L: return 42;
+ }
+
+ Treating such a special case may be hard and not sufficient. Then, although
+ coarse, our general solution is to enclose the function body (except the
+ return statement and the declaration of the retvar) inside a block. *)
if
List.exists
(fun v -> Cil.hasAttribute Cabs2cil.frama_c_destructor v.vattr)
--
GitLab