*** empty log message ***

[splint.git] / test / db3 / dbase.c

diff --git a/test/db3/dbase.c b/test/db3/dbase.c
index fba31468431aaf20d07ff3ed60b90c3fc4584d0d..96b7c7743bf472a2094b45e4108550c3a28a115f 100644 (file)
--- a/test/db3/dbase.c
+++ b/test/db3/dbase.c
@@ -32,7 +32,7 @@ void db_initMod (void)
 {
   if (initDone)
     {
-      return;
+      /*@-compdef@*/ return; /*@=compdef@*/
     }
   
   bool_initMod ();
@@ -43,11 +43,11 @@ void db_initMod (void)
   
   employeeKinds_all (ek)
     {
-      db[(int)ek] = erc_create ();
+      /*@-mustfree@*/ db[(int)ek] = erc_create (); /*@=mustfree@*/
     } end_employeeKinds_all ;
   
-  initDone = TRUE;
-}
+  initDone = TRUE; /*@-compdef@*/ /* db[] is really defined */
+} /*@=compdef@*/
 
 static eref db_ercKeyGet(erc c, int key)  /*@*/
 {