#
3431ac3d |
|
14-Dec-2014 |
Zaheer Chothia <zchothia@inf.ethz.ch> |
Remove <nodeputy.h> from default flags Summary: Deputy annotations [1] can be used to label safety properties. They are used extensively in the kernel, but in user-space there is only one use. The macros have short names (like 'COUNT', 'SAFE') which can conflict when building other applications. Furthermore, these are not being checked and are just stripped during the build. Note: the change to <kernel.h> is needed because it is included from a generated file: build-x86_64/capabilities/cap_predicates.c [1] http://ivy.cs.berkeley.edu/ivywiki/uploads/deputy-manual.html Test Plan: `make clean && make` was successful Differential Revision: https://code.systems.ethz.ch/D6
|