diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-02-17 13:47:54 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-02-17 13:47:54 +0100 |
| commit | 920686c5feabda7a7b7310e89e9d0e18a822284e (patch) | |
| tree | 78971539decbd3f8d7abca5ff1107e0295d275a9 /cparser/Cflow.ml | |
| parent | 9b63d90b40974eed35bd199fcfc6ccbabb1ed5b7 (diff) | |
| parent | db98d9de791c997ccb659ede00239d74926f68f4 (diff) | |
| download | compcert-kvx-920686c5feabda7a7b7310e89e9d0e18a822284e.tar.gz compcert-kvx-920686c5feabda7a7b7310e89e9d0e18a822284e.zip | |
Merge pull request #172 from AbsInt/std_noreturn_fun
Treat as _Noreturn the standard C11 functions that are _Noreturn but not always declared as such in header files.
Diffstat (limited to 'cparser/Cflow.ml')
| -rw-r--r-- | cparser/Cflow.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index 790d9079..7b3d3d32 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -22,6 +22,10 @@ open Cutil module StringSet = Set.Make(String) +(* Functions declared noreturn by the standard *) +let std_noreturn_functions = + ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"] + (* Statements are abstracted as "flow transformers": functions from possible inputs to possible outcomes. Possible inputs are: @@ -177,9 +181,10 @@ let rec outcomes env s : flow = | Sskip -> normal | Sdo {edesc = ECall(fn, args)} -> - if find_custom_attributes ["noreturn"; "__noreturn__"] - (attributes_of_type env fn.etyp) = [] - then normal else noflow + let returns = find_custom_attributes ["noreturn"; "__noreturn__"] + (attributes_of_type env fn.etyp) = [] in + let std_noreturn = List.exists (is_call_to_fun fn) std_noreturn_functions in + if returns && not std_noreturn then normal else noflow | Sdo e -> normal | Sseq(s1, s2) -> |