aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cflow.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-02-17 10:15:19 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-02-17 10:15:19 +0100
commitcf274c8dbf0e9dcc0a957e6f1f4b26f0b5453789 (patch)
tree26a2958a056bcc8c1cd26764a2e9abbe496ffcd1 /cparser/Cflow.ml
parent20c7b4d292ca1e69b66d10e8b0054982fe464714 (diff)
downloadcompcert-kvx-cf274c8dbf0e9dcc0a957e6f1f4b26f0b5453789.tar.gz
compcert-kvx-cf274c8dbf0e9dcc0a957e6f1f4b26f0b5453789.zip
Add longjmp. Bug 21009
Diffstat (limited to 'cparser/Cflow.ml')
-rw-r--r--cparser/Cflow.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml
index 718ae421..250dfe26 100644
--- a/cparser/Cflow.ml
+++ b/cparser/Cflow.ml
@@ -24,7 +24,7 @@ module StringSet = Set.Make(String)
(* Functions declared noreturn by the standard *)
let std_noreturn_functions =
- ["exit";"abort";"_Exit";"quick_exit";"thrd_exit"]
+ ["longjmp";"exit";"abort";"_Exit";"quick_exit";"thrd_exit"]
(* Statements are abstracted as "flow transformers":
functions from possible inputs to possible outcomes.