Merged this branch with the one in the splint.sf.net repository.

[splint.git] / src / Headers / llmain.h

diff --git a/src/Headers/llmain.h b/src/Headers/llmain.h
index 3d7b0fc997a9e3dfc55ab9fc975a2403aa15394c..89ca3dcc5437ff0aa42f2958a2790b558d84b735 100644 (file)
--- a/src/Headers/llmain.h
+++ b/src/Headers/llmain.h
@@ -10,17 +10,21 @@ extern int main (int p_argc, char *p_argv[])
 # ifdef NOLCL
   /*@globals killed undef g_currentloc,
             killed undef yyin,
-                    undef g_warningstream;@*/
-  /*@modifies g_currentloc, fileSystem, internalState, yyin;@*/
+                    undef g_warningstream,
+   @*/
+  /*@modifies g_currentloc, fileSystem, internalState, yyin; 
+  @*/
 # else
   /*@globals killed undef g_currentloc,
+            killed       g_localSpecPath,  
             killed undef g_currentSpec,
             killed undef g_currentSpecName,
             killed undef g_currentloc,
             killed undef yyin,
                     undef g_warningstream;
    @*/
-  /*@modifies g_currentloc, g_currentSpec, g_currentSpecName,
+  /*@modifies g_currentloc,
+              g_localSpecPath, g_currentSpec, g_currentSpecName,
              yyin, internalState, fileSystem; 
   @*/ 
 # endif