Skip to content
Snippets Groups Projects
Commit 62a307d8 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Remove assertion in `Label.get_stmt`

If `BuiltinLabel` or `FormalLabel` are encountered, raise `not_yet`.
parent 833a1918
No related branches found
No related tags found
No related merge requests found
...@@ -68,11 +68,14 @@ let get_stmt kf llabel = ...@@ -68,11 +68,14 @@ let get_stmt kf llabel =
| BuiltinLabel Here -> Error.not_yet "Label 'Here'" | BuiltinLabel Here -> Error.not_yet "Label 'Here'"
| BuiltinLabel(Old | Pre) -> | BuiltinLabel(Old | Pre) ->
(try Kernel_function.find_first_stmt kf (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) -> | BuiltinLabel(Post) ->
(try Kernel_function.find_return kf (try Kernel_function.find_return kf
with Kernel_function.No_Statement -> assert false) with Kernel_function.No_Statement -> assert false (* Frama-C invariant*))
| BuiltinLabel _ | FormalLabel _ -> assert false | BuiltinLabel _ ->
Error.not_yet (Format.asprintf "Label '%a'" Printer.pp_logic_label llabel)
| FormalLabel _ ->
Error.not_yet "FormalLabel"
in in
(* the pointed statement has been visited and modified by the injector: (* the pointed statement has been visited and modified by the injector:
get its new version. *) get its new version. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment