diff options
Diffstat (limited to 'ident-list.h')
| -rw-r--r-- | ident-list.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/ident-list.h b/ident-list.h index 8049b694..3c08e8ca 100644 --- a/ident-list.h +++ b/ident-list.h @@ -78,6 +78,12 @@ IDENT(memset); IDENT(memcpy); IDENT(copy_to_user); IDENT(copy_from_user); IDENT(main); +/* used by the symbolic checker */ +IDENT(__assume); +IDENT(__assert); +IDENT(__assert_eq); +IDENT(__assert_const); + #undef __IDENT #undef IDENT #undef IDENT_RESERVED |