diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-16 16:45:05 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-16 16:45:05 +0100 |
| commit | 20c7b4d292ca1e69b66d10e8b0054982fe464714 (patch) | |
| tree | 073ff5557711a4b1141445281e56a67764c11c63 /cparser/Cutil.ml | |
| parent | 9b63d90b40974eed35bd199fcfc6ccbabb1ed5b7 (diff) | |
| download | compcert-kvx-20c7b4d292ca1e69b66d10e8b0054982fe464714.tar.gz compcert-kvx-20c7b4d292ca1e69b66d10e8b0054982fe464714.zip | |
Added handling for noreturn std functions.
The C11 standard declares exit,abort,_Exit,quick_exit and
thrd_exit as _Noreturn however this is not included in older C
libs and leads to false negatives in reporting _Noreturn and
return type warnings. This can be avoided by enhancing the
noreturn check of the Cflow analysis to also test if one of the
above functions is called.
Bug 21009
Diffstat (limited to 'cparser/Cutil.ml')
| -rw-r--r-- | cparser/Cutil.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 6cafaf17..124560e5 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -954,6 +954,10 @@ let is_debug_stmt s = is_debug_call e | _ -> false +let is_call_to_fun e s = + match e.edesc with + | EVar id -> id.C.name = s + | _ -> false (* Assignment compatibility check over attributes. Standard attributes ("const", "volatile", "restrict") can safely |