aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Checks.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-02-16 13:23:17 +0100
committerBernhard Schommer <bschommer@users.noreply.github.com>2017-02-17 14:09:56 +0100
commitaa59d2dd11570e8cea3d8c429b94acf1001e2cc6 (patch)
tree80f80d7eabc0778f2a94a64a5ae5beba6233e2ee /cparser/Checks.mli
parent6eb08ac1a681ac06c8b37a7c402e17bf12b82707 (diff)
downloadcompcert-aa59d2dd11570e8cea3d8c429b94acf1001e2cc6.tar.gz
compcert-aa59d2dd11570e8cea3d8c429b94acf1001e2cc6.zip
Added unused attribute and simplified checks.
The attribute unused can be used to indicate if a variable or parameter is unused and no warning should be emitted for it. Furthermore this commit simplifies the check by adding a generic function to traverse the program. Bug 19872
Diffstat (limited to 'cparser/Checks.mli')
0 files changed, 0 insertions, 0 deletions