X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/16c024b587f5ddc115928d5cca7095508aa208d9..ed62d3fbeda6bb085991cdd683ceacfc57f7afbe:/src/stateInfo.c

diff --git a/src/stateInfo.c b/src/stateInfo.c
index 01e213b..6d80a88 100644
--- a/src/stateInfo.c
+++ b/src/stateInfo.c
@@ -1,6 +1,6 @@
 /*
 ** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
 **         Massachusetts Institute of Technology
 **
 ** This program is free software; you can redistribute it and/or modify it
@@ -25,6 +25,15 @@
 # include "splintMacros.nf"
 # include "basic.h"
 
+# ifdef WIN32
+/*
+** Make Microsoft VC++ happy: its control checking produces too
+** many spurious warnings.
+*/
+
+# pragma warning (disable:4715) 
+# endif
+
 static /*@observer@*/ cstring stateAction_unparse (stateAction p_sa) /*@*/ ;
 
 void stateInfo_free (/*@only@*/ stateInfo a)
@@ -97,9 +106,9 @@ static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo sinfo)
 
       if (!fileloc_lessthan (sinfo->loc, snext->loc))
 	{
-	  /*@i888@*/ sinfo->previous = sfirst;
+	  /*@i2@*/ sinfo->previous = sfirst; /* spurious? */
 	  DPRINTF (("Sorted ==> %s", stateInfo_unparse (sinfo)));
-	  /*@i888@*/ return sinfo;
+	  /*@i2@*/ return sinfo; /* spurious? */
 	}
       else
 	{
@@ -116,18 +125,24 @@ static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo sinfo)
       
 	      snext->loc = sinfo->loc;
 	      snext->action = sinfo->action;
-	      /*@i888@*/ snext->ref = sinfo->ref;
+	      /*@-modobserver@*/
+	      snext->ref = sinfo->ref; /* Doesn't actually modifie sfirst */ 
+	      /*@=modobserver@*/
 	      
 	      sinfo->loc = tloc;
 	      sinfo->action = taction;
 	      sinfo->ref = tref;
-	      /*@i888@*/ sinfo->previous = snext->previous;
+	      /*@-mustfreeonly@*/
+	      sinfo->previous = snext->previous;
+	      /*@=mustfreeonly@*/
 	      snext = snext->previous;
 	      DPRINTF (("in while: sinfo/sext: %s // %s", stateInfo_unparse (sinfo), stateInfo_unparse (snext)));
 	    }
 	  
 	  DPRINTF (("Sorted ==> %s", stateInfo_unparse (sfirst)));
-	  /*@i888@*/ return sfirst;
+	  /*@-compmempass@*/
+	  return sfirst;
+	  /*@=compmempass@*/
 	}
     }
 }