Added files for the splint.sf.net repository as part of the merge process.

[splint.git] / src / codeGeneration.c

diff --git a/src/codeGeneration.c b/src/codeGeneration.c
new file mode 100644 (file)
index 0000000..7919ae6
--- /dev/null
+++ b/src/codeGeneration.c
@@ -0,0 +1,104 @@
+/*
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
+**         Massachusetts Institute of Technology
+**
+** This program is free software; you can redistribute it and/or modify it
+** under the terms of the GNU General Public License as published by the
+** Free Software Foundation; either version 2 of the License, or (at your
+** option) any later version.
+** 
+** This program is distributed in the hope that it will be useful, but
+** WITHOUT ANY WARRANTY; without even the implied warranty of
+** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+** General Public License for more details.
+** 
+** The GNU General Public License is available from http://www.gnu.org/ or
+** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+** MA 02111-1307, USA.
+**
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
+*/
+
+/*
+** constraintGeneration.c
+*/
+
+# include "splintMacros.nf"
+# include "basic.h"
+
+static /*@only@*/ cstring includes = cstring_undefined;
+
+static void  doOutputCode (cstring st, fileloc loc)
+{
+  cstring name, newName;
+  FILE * f;
+      
+  if (context_getFlag(FLG_GENERATECODEANDOVERWRITE) )
+    {
+      if (fileloc_canGetName(loc) )
+       {
+         int tmp;
+         name = fileloc_getName(loc);
+                 
+         newName = cstring_concatChars(name, ".splint.tmp");
+         f = fopen (cstring_toCharsSafe(newName), "a");
+         
+         llassertprint(f != NULL, (message("failed to open file %s", newName)
+                                   ) );
+         
+         if (cstring_isDefined(includes) )
+           {
+             fprintf (f, "%s%s", cstring_toCharsSafe(includes),
+                      cstring_toCharsSafe(st) );
+
+             cstring_free(includes);
+             includes = cstring_undefined;
+           }
+         else
+           {
+             fprintf (f, "%s", cstring_toCharsSafe(st) );
+           }
+         /*@i999*/ /*these may fail they should be handled more cleanly...
+          */
+         tmp = fflush(f);
+         llassert(tmp == 0 );
+         tmp = fclose (f);
+         llassert( tmp  == 0 );
+
+         cstring_free(newName);
+       }
+      else
+       {
+         if (cstring_isUndefined(includes ) )
+           {
+             includes = message ("%s", st);
+           }
+         else
+           {
+             includes = cstring_concatFree1(includes, st);
+           }
+       }
+    }
+  else
+    {
+      fprintf (stderr, "%s", cstring_toCharsSafe(st) );
+    }
+  
+}
+
+void outputCode (cstring st)
+{
+  cstring output;
+
+
+  if (!fileloc_isDotH(g_currentloc) && context_getFlag(FLG_GENERATECODE))
+    {
+      // output = message ("/* %s */ \n %s",fileloc_unparse(g_currentloc), st);
+      output = st;
+      doOutputCode (output, g_currentloc);
+    }
+}
+