From 320c55590cc30d4ef5b2c1a226f0f940a6bdb445 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 25 Apr 2021 13:57:47 +0200 Subject: Support __builtin_unreachable Not yet used for optimizations. --- cparser/Cflow.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index cc257189..8a2a3fe4 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -23,8 +23,12 @@ open Cutil module StringSet = Set.Make(String) (* Functions declared noreturn by the standard *) +(* We also add our own "__builtin_unreachable" function because, currently, + it is difficult to attach attributes to a built-in function. *) + let std_noreturn_functions = - ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"] + ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"; + "__builtin_unreachable"] (* Statements are abstracted as "flow transformers": functions from possible inputs to possible outcomes. -- cgit