Fixed all /*@i...@*/ tags (except 1).

[splint.git] / src / lslinit.c

diff --git a/src/lslinit.c b/src/lslinit.c
index 9a3deb42518377ce8b291b8ba4ccc549edc822ba..83de1cfcd84cd3a1569f755df1d2dcc42e0c0fe5 100644 (file)
--- a/src/lslinit.c
+++ b/src/lslinit.c
@@ -1,6 +1,6 @@
 /*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2000 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2003 University of Virginia,
 **         Massachusetts Institute of Technology
 **
 ** This program is free software; you can redistribute it and/or modify it
@@ -17,9 +17,9 @@
 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 ** MA 02111-1307, USA.
 **
-** For information on lclint: lclint-request@cs.virginia.edu
-** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
 */
 /*
 ** lslinit.c
@@ -27,8 +27,8 @@
 ** Processor for Larch Shared Language Init Files
 */
 
-# include "lclintMacros.nf"
-# include "llbasic.h"
+# include "splintMacros.nf"
+# include "basic.h"
 # include "signature.h"
 # include "signature2.h"
 # include "scan.h"
@@ -36,6 +36,11 @@
 # include "tokentable.h"
 # include "syntable.h"
 # include "lslinit.h"
+# include "lclinit.h"
+# include "lclscan.h"
+# include "lclscanline.h"
+# include "lclsyntable.h"
+# include "lcltokentable.h"
 
 /* needed to parse init files */
 # include "shift.h"
@@ -48,10 +53,12 @@
 #endif
 
 static void LocalUserError (ltoken p_t, /*@temp@*/ char *p_msg)
-  /*@modifies *g_msgstream@*/;
+  /*@modifies *g_warningstream@*/;
 
 static /*@only@*/ ltoken nextToken;
 
+static /*@only@*/ /*@null@*/ inputStream s_initFile = inputStream_undefined;
+
 static void InitFile (void) /*@modifies nextToken@*/ ;
 static void InitLines (void) /*@modifies nextToken@*/ ;
 static void InitLine (void) /*@modifies nextToken@*/ ;
@@ -146,9 +153,10 @@ hasFirstChar (ltoken tok)
 }
 
 void
-LSLProcessInitFile (void)
+lslinit_setInitFile (inputStream s)
 {
-  InitFile ();
+  llassert (inputStream_isUndefined (s_initFile));
+  s_initFile = s;
 }
 
 /*
@@ -158,8 +166,7 @@ LSLProcessInitFile (void)
 **
 */
 
-static void
-InitFile (void)
+static void lslinit_processInitFile (void)
 {
   InitLines ();
   InitReduce (INITFILE1);
@@ -1324,7 +1331,7 @@ ProcessExtensionChar (void)
      /* Can only have one extension char.  Release old one. */
       lsetCharClass (firstChar, CHC_EXTENSION);
       
-      /* this is a (bogus) type bug! caught by lclint */
+      /* this is a (bogus) type bug! caught by splint */
       /* lsetCharClass (currentExtensionChar, SINGLECHAR); */
 
       lsetCharClass ((char) currentExtensionChar, SINGLECHAR);
@@ -1492,8 +1499,8 @@ static /*@exposed@*/ ltoken insertSimpleToken (char *text)
   return (LSLInsertToken (LST_SIMPLEID, lsymbol_fromChars (text), 0, FALSE));
 }
 
-void
-LSLProcessInitFileInit (void)
+static void
+lslinit_initProcessInitFile (void)
 {
   int i;
 
@@ -1546,10 +1553,154 @@ LSLProcessInitFileInit (void)
   nextToken = LSLScanNextToken ();            
 }
 
+void lslinit_process (void)
+  /*@globals undef g_symtab; @*/
+  /*@modifies g_symtab, internalState, fileSystem; @*/
+{
+  /*
+  ** Open init file provided by user, or use the default LCL init file 
+  */
+  
+  cstring larchpath = context_getLarchPath ();
+  inputStream initstream = inputStream_undefined;
+
+  setCodePoint ();
+
+  if (inputStream_isUndefined (s_initFile))
+    {
+      s_initFile = inputStream_create (cstring_makeLiteral (INITFILENAME), 
+                                      cstring_makeLiteralTemp (LCLINIT_SUFFIX),
+                                      FALSE);
+      
+      if (!inputStream_getPath (larchpath, s_initFile))
+       {
+         lldiagmsg (message ("Continuing without LCL init file: %s",
+                             inputStream_fileName (s_initFile)));
+       }
+      else 
+       {
+         if (!inputStream_open (s_initFile))
+           {
+             lldiagmsg (message ("Continuing without LCL init file: %s",
+                                 inputStream_fileName (s_initFile)));
+           }
+       }
+    }
+  else 
+    {
+      if (!inputStream_open (s_initFile))
+       {
+         lldiagmsg (message ("Continuing without LCL init file: %s",
+                             inputStream_fileName (s_initFile)));
+       }
+    }
+
+  /* Initialize checker */
+
+  lsymbol_initMod ();
+  LCLSynTableInit ();
+
+  setCodePoint ();
+
+  LCLSynTableReset ();
+  LCLTokenTableInit ();
+
+  setCodePoint ();
+
+  LCLScanLineInit ();
+  setCodePoint ();
+  LCLScanLineReset ();
+  setCodePoint ();
+  LCLScanInit ();
 
+  setCodePoint ();
 
+  /* need this to initialize LCL checker */
 
+  llassert (inputStream_isDefined (s_initFile));      
+  if (inputStream_isOpen (s_initFile))
+    {
+      setCodePoint ();
+
+      LCLScanReset (s_initFile);
+      lclinit_initMod ();
+      lclinit_reset ();
 
+      setCodePoint ();
+      lclinit_process ();
+      lclinit_cleanup ();
+
+      setCodePoint ();
+      check (inputStream_close (s_initFile));
+    }
+  
+  /* Initialize LSL init files, for parsing LSL signatures from LSL */
+  
+  initstream = inputStream_create (cstring_makeLiteral ("lslinit.lsi"), 
+                                   cstring_makeLiteralTemp (".lsi"),
+                                   FALSE);
+  
+  if (!inputStream_getPath (larchpath, initstream))
+    {
+      lldiagmsg (message ("Continuing without LSL init file: %s",
+                         inputStream_fileName (initstream)));
+    }
+  else 
+    {
+      if (!inputStream_open (initstream))
+       {
+         lldiagmsg (message ("Continuing without LSL init file: %s",
+                             inputStream_fileName (initstream)));
+       }
+    }
+      
+  setCodePoint ();
+  lsynTableInit ();
+  lsynTableReset ();
 
+  setCodePoint ();
+  ltokenTableInit ();
 
+  setCodePoint ();
+  lscanLineInit ();
+  lscanLineReset ();
+  LSLScanInit ();
 
+  if (inputStream_isOpen (initstream))
+    {
+      setCodePoint ();
+      LSLScanReset (initstream);
+      lslinit_initProcessInitFile ();
+      lslinit_processInitFile ();
+      check (inputStream_close (initstream));
+    }
+      
+  inputStream_free (initstream);
+  
+  if (lclHadError ())
+    {
+      lclplainerror 
+       (cstring_makeLiteral ("LSL init file error.  Attempting to continue."));
+    }
+  
+  setCodePoint ();
+  g_symtab = symtable_new ();
+  
+  /* 
+  ** sort_init must come after symtab has been initialized 
+  */
+  sort_init ();
+  abstract_init ();
+  setCodePoint ();
+  
+  /* 
+  ** Equivalent to importing old spec_csupport.lcl
+  ** define immutable LCL type "bool" and bool constants TRUE and FALSE
+  ** and initialized them to be equal to LSL's "true" and "false".
+  **
+  ** Reads in CTrait.syms (derived from CTrait.lsl) on LARCH_PATH.
+  */
+      
+  LCLBuiltins (); 
+  LCLReportEolTokens (FALSE);
+}