eref.c: (in function eref_initMod)
eref.c:63,3: Called procedure bool_initMod may access internal state, but
                globals list does not include globals internalState
  A called function uses internal state, but the globals list for the function
  being checked does not include internalState  Use -internalglobs to suppress
  message.
eref.c:63,3: Undocumented modification of internal state possible from call to
                bool_initMod: bool_initMod()
  An externally-visible object is modified by a function, but not listed in its
  modifies clause.  Use -mods to suppress message.
eref.c:64,3: Called procedure employee_initMod may access internal state, but
                globals list does not include globals internalState
eref.c:64,3: Undocumented modification of internal state possible from call to
                employee_initMod: employee_initMod()
empset.c: (in function empset_insert)
empset.c:35,3: Called procedure empset_insertUnique may access internal state,
                  but globals list does not include globals internalState
empset.c:35,3: Undocumented modification of internal state possible from call
                  to empset_insertUnique: empset_insertUnique(s, e)
dbase.c: (in function db_initMod)
dbase.c:37,3: Called procedure bool_initMod may access internal state, but
                 globals list does not include globals internalState
dbase.c:37,3: Undocumented modification of internal state possible from call to
                 bool_initMod: bool_initMod()
dbase.c:38,3: Called procedure employee_initMod may access internal state, but
                 globals list does not include globals internalState
dbase.c:38,3: Undocumented modification of internal state possible from call to
                 employee_initMod: employee_initMod()
dbase.c:40,3: Called procedure erc_initMod may access internal state, but
                 globals list does not include globals internalState
dbase.c:40,3: Undocumented modification of internal state possible from call to
                 erc_initMod: erc_initMod()
dbase.c:41,3: Called procedure empset_initMod may access internal state, but
                 globals list does not include globals internalState
dbase.c:41,3: Undocumented modification of internal state possible from call to
                 empset_initMod: empset_initMod()
drive.c: (in function main)
drive.c:23,3: Called procedure bool_initMod may access internal state, but
                 globals list does not include globals internalState
drive.c:23,3: Undocumented modification of internal state possible from call to
                 bool_initMod: bool_initMod()
  An externally-visible object is modified by a function with no /*@modifies@*/
  comment.  The /*@modifies ... @*/ control comment can be used to give a
  modifies list for an unspecified function.  Use -modnomods to suppress
  message.
drive.c:24,3: Called procedure employee_initMod may access internal state, but
                 globals list does not include globals internalState
drive.c:24,3: Undocumented modification of internal state possible from call to
                 employee_initMod: employee_initMod()
drive.c:25,3: Called procedure empset_initMod may access internal state, but
                 globals list does not include globals internalState
drive.c:25,3: Undocumented modification of internal state possible from call to
                 empset_initMod: empset_initMod()
drive.c:153,9: Called procedure empset_disjointUnion may access internal state,
                  but globals list does not include globals internalState
drive.c:153,9: Undocumented modification of internal state possible from call
                  to empset_disjointUnion: empset_disjointUnion(em2, em1)