From 62a307d8f9005c22b68486303d368cc24ddc33dc Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 15 Jul 2021 17:37:18 +0200
Subject: [PATCH] [eacsl] Remove assertion in `Label.get_stmt`
If `BuiltinLabel` or `FormalLabel` are encountered, raise `not_yet`.
---
src/plugins/e-acsl/src/code_generator/label.ml | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/label.ml b/src/plugins/e-acsl/src/code_generator/label.ml
index f06c2232dfc..838c192a898 100644
--- a/src/plugins/e-acsl/src/code_generator/label.ml
+++ b/src/plugins/e-acsl/src/code_generator/label.ml
@@ -68,11 +68,14 @@ let get_stmt kf llabel =
| BuiltinLabel Here -> Error.not_yet "Label 'Here'"
| BuiltinLabel(Old | Pre) ->
(try Kernel_function.find_first_stmt kf
- with Kernel_function.No_Statement -> assert false)
+ with Kernel_function.No_Statement -> assert false (* Frama-C invariant*))
| BuiltinLabel(Post) ->
(try Kernel_function.find_return kf
- with Kernel_function.No_Statement -> assert false)
- | BuiltinLabel _ | FormalLabel _ -> assert false
+ with Kernel_function.No_Statement -> assert false (* Frama-C invariant*))
+ | BuiltinLabel _ ->
+ Error.not_yet (Format.asprintf "Label '%a'" Printer.pp_logic_label llabel)
+ | FormalLabel _ ->
+ Error.not_yet "FormalLabel"
in
(* the pointed statement has been visited and modified by the injector:
get its new version. *)
--
GitLab