Updated html and word versions of the manual

[splint.git] / src / stateInfo.c

diff --git a/src/stateInfo.c b/src/stateInfo.c
index 01e213b6eca7ce1dbadd61dea601ca1686146153..6d80a88a87d359d297309e860e3837caa40525cc 100644 (file)
--- 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@*/
        }
     }
 }