]> andersk Git - splint.git/commitdiff
Committing after merging Evan's changes.
authordrl7x <drl7x>
Mon, 31 Mar 2003 03:29:18 +0000 (03:29 +0000)
committerdrl7x <drl7x>
Mon, 31 Mar 2003 03:29:18 +0000 (03:29 +0000)
This code breaken but atleast it compile making it an improvement over the current version which doesn't compile after yesterday's committs.

19 files changed:
README
src/Headers/constraint.h
src/Headers/constraintList.h
src/Headers/constraintTerm.h
src/Headers/ltoken.h
src/Headers/sort.h
src/Makefile.am
src/Makefile.in
src/abstract.c
src/checking.c
src/constraint.c
src/constraintExpr.c
src/constraintList.c
src/constraintTerm.c
src/imports.c
src/llgrammar.c.der
src/llgrammar.y
src/ltoken.c
src/sort.c

diff --git a/README b/README
index e05b904eca386445917fee712a44151021388cbb..af606830942f35d9226af9ffa4f42076eb144fe0 100644 (file)
--- a/README
+++ b/README
@@ -5,8 +5,9 @@
                        University of Virginia,
                 Massachusetts Institute of Technology
                 
-                           Version 3.0.1.7
-                            2 March 20023
+                           Version 3.0.1.7 
+                            31 March 2003
+
 Splint Documentation
 ====================
 
index 7133a4237690cb6baac7622d4aa56865a3080986..05c7ddfe39661d94ffa4edff3453a50488552558 100644 (file)
@@ -63,12 +63,12 @@ extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/;
 
 extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c);
 
-extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
-# define constraint_unparse constraint_print
+extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ constraint p_c) /*@*/;
+extern /*@only@*/ cstring constraint_unparseOr (/*@temp@*/ constraint p_c) /*@*/ ;
+extern /*@only@*/ cstring constraint_unparseDetailed (constraint p_c) /*@*/ ;
 
-extern /*@only@*/ cstring constraint_print (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
-
-extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind);
+extern /*@only@*/ constraint 
+constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind);
 
 extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/;
 
@@ -79,8 +79,6 @@ extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@de
 extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/;
 extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition,
                                                            exprNodeList p_arglist);
-extern /*@only@*/ cstring  constraint_printDetailed (constraint p_c);
-
 extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
 extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
 
@@ -123,8 +121,6 @@ exprNode_traversEnsuresConstraints (exprNode p_e);
 
 extern constraint constraint_togglePost (/*@returned@*/ constraint p_c);
 extern bool constraint_same (constraint p_c1, constraint p_c2) ;
-
-/*@only@*/ cstring  constraint_printOr (constraint p_c) /*@*/;
 extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ;
 
 extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_c) /*@*/; /*drl add 8-11-001*/
index 85c2f38915e2c79d0ccba9c79f4eec556bb517c6..94b190fc551a1926ea6676feaf02db5249c86c1d 100644 (file)
@@ -55,12 +55,9 @@ extern constraintList constraintList_copy ( /*@observer@*/ /*@temp@*/ constraint
 extern void constraintList_free (/*@only@*/ constraintList p_s) ;
 
 
-extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList p_s) /*@*/;
+extern /*@only@*/ cstring constraintList_unparse (/*@observer@*/ constraintList p_s) /*@*/;
 
-/*@only@*/ extern cstring constraintList_print ( /*@observer@*/ /*@temp@*/ constraintList p_s) /*@*/;
-
-extern cstring
-constraintList_printDetailed ( /*@observer@*/ constraintList p_s) /*@*/;
+extern cstring constraintList_unparseDetailed (/*@observer@*/ constraintList p_s) /*@*/;
 
 extern /*@only@*/ constraintList
 constraintList_logicalOr ( /*@observer@*/ constraintList p_l1, /*@observer@*/  constraintList p_l2);
index 673de12e0b3f0c45d4dbcff32a6e04c87260b9f3..90d6764308d3ae216d9810782683e8df819f74f6 100644 (file)
@@ -9,13 +9,12 @@ typedef union
   long intlit;
 } constraintTermValue;
 
-/*@-namechecks@*/
-
 typedef enum
 {
-  ERRORBADCONSTRAINTTERMTYPE,
- EXPRNODE, SREF,
- INTLITERAL
+  CTT_ERRORBADCONSTRAINTTERMTYPE,
+  CTT_EXPR, 
+  CTT_SREF,
+  CTT_INTLITERAL
 } constraintTermType;
 
 struct _constraintTerm {
@@ -50,8 +49,6 @@ fileloc constraintTerm_getFileloc (constraintTerm t) /*@*/;
 
 bool constraintTerm_isIntLiteral (constraintTerm term) /*@*/;
 
-cstring constraintTerm_print (constraintTerm term) /*@*/;
-
 constraintTerm constraintTerm_makesRef  (/*@temp@*/ /*@observer@*/ sRef s) /*@*/;
 
 /*@unused@*/ bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2) /*@*/;
@@ -66,31 +63,21 @@ cstring constraintTerm_getStringLiteral (constraintTerm c) /*@*/;
 
 constraintTerm constraintTerm_doSRefFixBaseParam (/*@returned@*/ constraintTerm term, exprNodeList arglist) /*@modifies term@*/;
 
-void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f);
-
-/*@only@*/ constraintTerm constraintTerm_undump ( FILE *f);
-
-bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm p_c) /*@*/;
-
-int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm p_c) /*@*/;
-
-bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/;
-
+extern cstring constraintTerm_unparse (constraintTerm)  /*@*/ ;
 
+extern void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f);
+extern /*@only@*/ constraintTerm constraintTerm_undump ( FILE *f);
+extern bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm p_c) /*@*/;
+extern int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm p_c) /*@*/;
+extern bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/;
 extern ctype constraintTerm_getCType (constraintTerm term);
 
-/*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t);
-
-/*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t);
-
-
-/*@=namechecks@*/
+extern /*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t);
+extern /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t);
 
 /*drl added 12/19/2002*/
-bool  constraintTerm_isConstantOnly ( constraintTerm p_term );
+extern bool constraintTerm_isConstantOnly (constraintTerm p_term);
      
 #else
-
-#error Multiple Include
-
+#error "Multiple Include!"
 #endif
index 7b7b68b582de5852f4fa83844ff189184d2b5213..78c994fb4e09d2539bc7787d0c66ee0a0a9a0ed1 100644 (file)
@@ -107,7 +107,7 @@ extern bool ltoken_wasSyn (/*@sef@*/ ltoken p_tok);
 # define ltoken_wasSyn(tok) \
   (ltoken_isValid (tok) ? lsymbol_isDefined ((tok)->rawText) : FALSE)
 
-/*@-namechecks@*/
+/*@-namechecks@*/ /* all of these should start with g_ */
 extern /*@dependent@*/ ltoken ltoken_forall;
 extern /*@dependent@*/ ltoken ltoken_exists;
 extern /*@dependent@*/ ltoken ltoken_true;
index 8e2073bce93734df821870b0bd2e754ff8026208..9540a76597a55cec237644de91bee516a4377407 100644 (file)
@@ -160,15 +160,13 @@ extern sort sort_fromLsymbol (lsymbol p_sortid) /*@modifies internalState@*/ ;
 extern void sort_import (inputStream p_imported, ltoken p_tok, mapping p_map)
    /*@modifies p_imported, internalState@*/ ;
 
-/*@-namechecks@*/
-extern sort sort_bool;
-extern sort sort_capBool;
-extern sort sort_int;
-extern sort sort_char;
-extern sort sort_cstring;
-extern sort sort_float;
-extern sort sort_double;
-/*@=namechecks@*/
+extern sort g_sortBool;
+extern sort g_sortCapBool;
+extern sort g_sortInt;
+extern sort g_sortChar;
+extern sort g_sortCstring;
+extern sort g_sortFloat;
+extern sort g_sortDouble;
 
 # else
 # error "Multiple include"
index d486f22bffe421ca146fae3687ff5e732c2576b1..b4a45f6332d5af9669e0047157fbcde086971b71 100644 (file)
@@ -393,10 +393,10 @@ etags:
 lintnew: splintme
 
 splintme: 
-       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude  $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw 
+       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude  $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw 
 
-splintmenosupcounts: 
-       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude  $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments  -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw 
+splintmesupcounts: 
+       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude  $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments  -fcnuse -incondefs -exportlocal -supcounts -constuse -mts file -mts filerw 
 
 lintbuffercheck: 
        ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +bounds -DLINTBUFFERCHECK
index 8ac5db39ab2594b71b674eea494bb87adbdb6b87..103e7b1e520ad1b01388710e6d70df180a17faf4 100644 (file)
@@ -1124,10 +1124,10 @@ etags:
 lintnew: splintme
 
 splintme: 
-       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude  $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw 
+       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude  $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw 
 
-splintmenosupcounts: 
-       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude  $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments  -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw 
+splintmesupcounts: 
+       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude  $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments  -fcnuse -incondefs -exportlocal -supcounts -constuse -mts file -mts filerw 
 
 lintbuffercheck: 
        ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +bounds -DLINTBUFFERCHECK
index 62f899410556897a3b33990c5b27e82ae8b0da9d..3e95eaea3c3e6ac6d753026b142c5f0db2e78e61 100644 (file)
@@ -186,7 +186,7 @@ abstract_init ()
   ti->modifiable = FALSE;
   ti->abstract = FALSE;
   ti->export = FALSE;          /* this is implicit, not exported */
-  ti->basedOn = sort_float;
+  ti->basedOn = g_sortFloat;
   symtable_enterType (g_symtab, ti);
 }
 
@@ -236,7 +236,7 @@ void LCLBuiltins (void)
 
   ti->modifiable = FALSE;
   ti->abstract = TRUE;
-  ti->basedOn = sort_bool;
+  ti->basedOn = g_sortBool;
   ti->export = FALSE; /* this wasn't set (detected by Splint) */
   symtable_enterType (g_symtab, ti);
   
@@ -244,7 +244,7 @@ void LCLBuiltins (void)
   vi->id = ltoken_createType (simpleId, SID_VAR, lsymbol_fromChars ("FALSE"));
 
   vi->kind = VRK_CONST;
-  vi->sort = sort_bool;
+  vi->sort = g_sortBool;
   vi->export = TRUE;
 
   (void) symtable_enterVar (g_symtab, vi);
@@ -3701,7 +3701,7 @@ makeQuantifiedTermNode (quantifierNodeList qn, ltoken open,
   termNodeList_free (t->args);
   t->args = termNodeList_new ();
 
-  sort = sort_bool;
+  sort = g_sortBool;
   n->sort = sort;
   (void) sortSet_insert (n->possibleSorts, sort);
 
@@ -4223,7 +4223,7 @@ makeLiteralTermNode (ltoken tok, sort s)
      needed anyway.  */
   /*  symtable_enterOp (g_symtab, nn, sign); */
 
-  if (s == sort_int)
+  if (s == g_sortInt)
     {
       sigNode osign;
       lslOp opn = (lslOp) dmalloc (sizeof (*opn));
@@ -4231,7 +4231,7 @@ makeLiteralTermNode (ltoken tok, sort s)
       /* if it is a C int, we should overload it as double too because
         C allows you to say "x > 2". */
       
-      (void) sortSet_insert (n->possibleSorts, sort_double);
+      (void) sortSet_insert (n->possibleSorts, g_sortDouble);
       
       ltoken_setText (range, lsymbol_fromChars ("double"));
       osign = makesigNode (ltoken_undefined, ltokenList_new (), range);
@@ -4261,7 +4261,7 @@ makeUnchangedTermNode1 (ltoken op, /*@unused@*/ ltoken all)
   t->error_reported = FALSE;
   t->wrapped = 0;
   t->kind = TRM_UNCHANGEDALL;
-  t->sort = sort_bool;
+  t->sort = g_sortBool;
   t->literal = op;
   t->given = sort_makeNoSort ();
   t->name = NULL; /*< missing this >*/
@@ -4286,7 +4286,7 @@ makeUnchangedTermNode2 (ltoken op, storeRefNodeList x)
   t->error_reported = FALSE;
   t->wrapped = 0;
   t->kind = TRM_UNCHANGEDOTHERS;
-  t->sort = sort_bool;
+  t->sort = g_sortBool;
   t->literal = op;
   t->unchanged = x;
   t->given = sort_makeNoSort ();
@@ -4338,7 +4338,7 @@ makeUnchangedTermNode2 (ltoken op, storeRefNodeList x)
   t->error_reported = FALSE;
   t->wrapped = 0;
   t->kind = TRM_SIZEOF;
-  t->sort = sort_int;
+  t->sort = g_sortInt;
   t->literal = op;
   t->sizeofField = type;
   t->given = sort_makeNoSort ();
index 7adb6dbb17385fbb6c7c14b5024d2328943b1391..7e11ce86e9bb7b4290dce4f40c6ebc13369a104d 100644 (file)
@@ -398,7 +398,7 @@ checkLclPredicate (ltoken t, lclPredicateNode n)
     {
      /* check that the sort of n is boolean */
       theSort = n->predicate->sort;
-      if (!sort_compatible (theSort, sort_capBool))
+      if (!sort_compatible (theSort, g_sortCapBool))
        {
          if (sort_isNoSort (theSort))
            {
@@ -582,14 +582,14 @@ standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sor
                      {
                        if (sn->kind == SRT_OBJ ||
                            sn->kind == SRT_ARRAY)
-                       (void) sortSet_insert (ret, sort_bool);   
+                       (void) sortSet_insert (ret, g_sortBool);          
                      }
                    
                    if (cstring_equalLit (text, "maxIndex") || 
                        cstring_equalLit (text, "minIndex"))
                      {
                        if (sn->kind == SRT_ARRAY || sn->kind == SRT_PTR)
-                         (void) sortSet_insert (ret, sort_int);          
+                         (void) sortSet_insert (ret, g_sortInt);         
                        
                        /*                if (lsymbol_fromChars ("maxIndex") */
                      }
@@ -601,14 +601,14 @@ standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sor
                  if (sn->kind == SRT_OBJ ||
                      sn->kind == SRT_ARRAY)
                    {
-                     (void) sortSet_insert (ret, sort_bool);     
+                     (void) sortSet_insert (ret, g_sortBool);    
                    }
                  break;
                case LLT_SIZEOF:
                  if (sn->kind == SRT_OBJ ||
                      sn->kind == SRT_ARRAY ||
                      sn->kind == SRT_VECTOR)
-                 (void) sortSet_insert (ret, sort_int);
+                 (void) sortSet_insert (ret, g_sortInt);
                  break;
                default:
                  break;
@@ -634,7 +634,7 @@ standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sor
            {
              argSet = sortSetList_head (argSorts);
              
-             if (sortSet_member (argSet, sort_bool))
+             if (sortSet_member (argSet, g_sortBool))
                {
                  sortSetList_reset (argSorts);
                  sortSetList_advance (argSorts);
@@ -778,7 +778,7 @@ standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sor
                              {
                                if (sort_equal (cl, cl2))
                                  {
-                                   (void) sortSet_insert (ret, sort_bool);
+                                   (void) sortSet_insert (ret, g_sortBool);
                                  }
                              } end_sortSet_elements;
                          } end_sortSet_elements; 
index fe7b638372d1def9a463154377861c5cdfeb932d..0d39b6eb4d8bd468a0de07a2ccbc36b5dd00a27a 100644 (file)
 
 /* #define DEBUGPRINT 1 */
 
-# include <ctype.h> /* for isdigit */
 # include "splintMacros.nf"
 # include "basic.h"
 # include "cgrammar.h"
 # include "cgrammar_tokens.h"
-
 # include "exprChecks.h"
 # include "exprNodeSList.h"
 
-
-static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
+static /*@only@*/ cstring 
+constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
 
 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
@@ -50,39 +48,6 @@ advanceField (char **s)
   reader_checkChar (s, '@');
 }
 
-# if 0
-static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)    
-{
-  char *t;
-  int c;
-  constraint ret;
-  ret = constraint_makeNew ();
-  llassert (constraintExpr_isDefined (l));
-      
-  ret->lexpr = constraintExpr_copy (l);
-
-
-  if (relOp.tok == GE_OP)
-      ret->ar = GTE;
-  else if (relOp.tok == LE_OP)
-    ret->ar = LTE;
-  else if (relOp.tok == EQ_OP)
-    ret->ar = EQ;
-  else
-  llfatalbug (message ("Unsupported relational operator"));
-
-
-  t =  cstring_toCharsSafe (exprNode_unparse (cconstant));
-  c = atoi ( t);
-  ret->expr = constraintExpr_makeIntLiteral (c);
-
-  ret->post = TRUE;
-  DPRINTF (("GENERATED CONSTRAINT:"));
-  DPRINTF ((message ("%s", constraint_unparse (ret))));
-  return ret;
-}
-# endif
-
 bool constraint_same (constraint c1, constraint c2)
 {
   llassert (c1 != NULL);
@@ -348,7 +313,6 @@ constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
 constraint constraint_makeWriteSafeInt (   exprNode po, int ind)
 {
   constraint ret = constraint_makeNew ();
-
  
   ret->lexpr =constraintExpr_makeMaxSetExpr (po);
   ret->ar = GTE;
index 5ea57e0da93595c468447e1282f73123202aee0a..7093b6efe48731be4b496935b9186240efc422b3 100644 (file)
@@ -1888,25 +1888,23 @@ doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
 {
   constraintTerm t;
   sRef s;
-
-  
   constraintExprData data;
   constraintExprKind kind;
-  
   constraintExpr ret;
-
-  llassert(constraintExpr_isDefined (e) );
+  
+  llassert (constraintExpr_isDefined (e) );
   
   data = e->data;
   kind = e->kind;
-
-  llassert(kind == term);
-
+  
+  llassert (kind == term);
+  
   t = constraintExprData_termGetTerm (data);
-  llassert (constraintTerm_isDefined(t) );
-
+  llassert (constraintTerm_isDefined (t));
+  
   ret = e;
-  switch (constraintTerm_getKind(t) )
+
+  switch (constraintTerm_getKind (t))
     {
     case CTT_EXPR:
     case CTT_INTLITERAL:
@@ -1932,7 +1930,11 @@ doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
   return ret;
   
 }
-/*
+
+#if 0
+
+/*to be used for structure checking */
+
 / *@only@* / static constraintExpr
 doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
  sRef s, ctype ct)
@@ -1991,7 +1993,7 @@ doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
   return ret;
   
 }
-*/
+#endif
  
 /*drl moved from constriantTerm.c 5/20/001*/
 /*@only@*/ static constraintExpr 
index 625d716bee59e15ec127c38636ae6e50a733f3e1..24654bce193043b3f8503a30b1848a5b51725546 100644 (file)
@@ -278,7 +278,7 @@ constraintList_unparse (/*@temp@*/ constraintList s) /*@*/
 
          if (context_getFlag (FLG_ORCONSTRAINT))
            {
-             temp1 = constraint_unparseOr(current);
+             temp1 = constraint_unparseOr (current);
            }
          else
            {
@@ -301,7 +301,7 @@ constraintList_unparse (/*@temp@*/ constraintList s) /*@*/
   return st;
 }
 
-void constraintList_unparseErrorPostConditions (constraintList s, fileloc loc)
+void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
 {
 
   constraintList_elements (s, elem)
@@ -315,7 +315,7 @@ void constraintList_unparseErrorPostConditions (constraintList s, fileloc loc)
   return;
 }
 
-void constraintList_unparseError (constraintList s, fileloc loc)
+void constraintList_printError (constraintList s, fileloc loc)
 {
 
   constraintList_elements (s, elem)
index 8c4ce963238e42aa871e08616b526ef7dd9f74df..807a0bdbeafeee73dd1ec8e2e4c03d36e098a3b8 100644 (file)
@@ -50,23 +50,23 @@ void constraintTerm_free (/*@only@*/ constraintTerm term)
   
   switch (term->kind) 
     {
-    case EXPRNODE:
+    case CTT_EXPR:
       /* we don't free an exprNode*/
       break;
-    case SREF:
+    case CTT_SREF:
       /* sref */
       sRef_free (term->value.sref);
       break;
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       /* don't free an int */
       break;
-    case  ERRORBADCONSTRAINTTERMTYPE:
+    case CTT_ERRORBADCONSTRAINTTERMTYPE:
     default:
       /* type was set incorrectly */
       llcontbug (message("constraintTerm_free type was set incorrectly"));
     }
 
-  term->kind =  ERRORBADCONSTRAINTTERMTYPE;
+  term->kind = CTT_ERRORBADCONSTRAINTTERMTYPE;
   free (term);
 }
 
@@ -83,7 +83,7 @@ bool constraintTerm_isIntLiteral (constraintTerm term)
 {
   llassert(term != NULL);
   
-  if (term->kind == INTLITERAL)
+  if (term->kind == CTT_INTLITERAL)
     return TRUE;
 
   return FALSE;
@@ -93,10 +93,10 @@ bool constraintTerm_isIntLiteral (constraintTerm term)
 bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
 {
   llassert (c != NULL);
-  if (c->kind == EXPRNODE)
+
+  if (c->kind == CTT_EXPR)
     {
-      
-      if (exprNode_isInitBlock(c->value.expr) )
+      if (exprNode_isInitBlock (c->value.expr))
        {
          return TRUE;
        }
@@ -108,7 +108,8 @@ bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@
 bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
 {
   llassert (c != NULL);
-  if (c->kind == EXPRNODE)
+
+  if (c->kind == CTT_EXPR)
     {
       return TRUE;
     }
@@ -118,12 +119,11 @@ bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*
 /*@access exprNode@*/
 int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
 {
-
-  exprNodeList  list;
+  exprNodeList list;
   int ret;
   llassert (c != NULL);
   llassert (constraintTerm_isInitBlock (c) );
-  llassert (c->kind == EXPRNODE);
+  llassert (c->kind == CTT_EXPR);
 
   llassert(exprNode_isDefined(c->value.expr) );
 
@@ -148,7 +148,7 @@ int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm
 bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/
 {
   llassert (c != NULL);
-  if (c->kind == EXPRNODE)
+  if (c->kind == CTT_EXPR)
     {
       if (exprNode_knownStringValue(c->value.expr) )
        {
@@ -164,14 +164,14 @@ cstring constraintTerm_getStringLiteral (constraintTerm c)
 {
   llassert (c != NULL);
   llassert (constraintTerm_isStringLiteral (c) );
-  llassert (c->kind == EXPRNODE);
+  llassert (c->kind == CTT_EXPR);
   
   return (cstring_copy ( multiVal_forceString (exprNode_getValue (c->value.expr) ) ) );
 }
 
 constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/
 {
-  if (term->kind == EXPRNODE)
+  if (term->kind == CTT_EXPR)
     {
       if ( exprNode_knownIntValue (term->value.expr ) )
        {
@@ -179,7 +179,7 @@ constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@m
 
          temp  = exprNode_getLongValue (term->value.expr);
          term->value.intlit = (int)temp;
-         term->kind = INTLITERAL;
+         term->kind = CTT_INTLITERAL;
        }
     }
   return term;
@@ -201,7 +201,7 @@ constraintTermType constraintTerm_getKind (constraintTerm t)
 /*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t)
 {
   llassert (constraintTerm_isDefined(t) );
-  llassert (t->kind == SREF);
+  llassert (t->kind == CTT_SREF);
 
   return (t->value.sref);
 }
@@ -211,7 +211,7 @@ constraintTermType constraintTerm_getKind (constraintTerm t)
   constraintTerm ret = new_constraintTermExpr();
   ret->loc =  fileloc_copy(exprNode_getfileloc(e));
   ret->value.expr = e;
-  ret->kind = EXPRNODE;
+  ret->kind = CTT_EXPR;
   ret = constraintTerm_simplify(ret);
   return ret;
 }
@@ -221,7 +221,7 @@ constraintTermType constraintTerm_getKind (constraintTerm t)
   constraintTerm ret = new_constraintTermExpr();
   ret->loc =  fileloc_undefined;
   ret->value.sref = sRef_saveCopy(s);
-  ret->kind = SREF;
+  ret->kind = CTT_SREF;
   ret = constraintTerm_simplify(ret);
   return ret;
 }
@@ -236,14 +236,14 @@ constraintTerm constraintTerm_copy (constraintTerm term)
   
   switch (term->kind)
     {
-    case EXPRNODE:
+    case CTT_EXPR:
       ret->value.expr = term->value.expr;
       break;
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       ret->value.intlit = term->value.intlit;
       break;
       
-    case SREF:
+    case CTT_SREF:
       ret->value.sref = sRef_saveCopy(term->value.sref);
       break;
     default:
@@ -274,15 +274,15 @@ static cstring constraintTerm_getName (constraintTerm term)
 
   switch (term->kind)
     {
-    case EXPRNODE:
+    case CTT_EXPR:
 
       s = message ("%s", exprNode_unparse (term->value.expr) );
       break;
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       s = message (" %d ", (int) term->value.intlit);
       break;
       
-    case SREF:
+    case CTT_SREF:
       s = message ("%q", sRef_unparse (term->value.sref) );
 
       break;
@@ -302,13 +302,13 @@ constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeLi
   
   switch (term->kind)
     {
-    case EXPRNODE:
+    case CTT_EXPR:
 
       break;
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       break;
       
-    case SREF:
+    case CTT_SREF:
       term->value.sref = sRef_fixBaseParam (term->value.sref, arglist);
       break;
     default:
@@ -318,7 +318,7 @@ constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeLi
   
 }
 
-cstring constraintTerm_print (constraintTerm term)  /*@*/
+cstring constraintTerm_unparse (constraintTerm term)  /*@*/
 {
   cstring s;
   s = cstring_undefined;
@@ -327,16 +327,16 @@ cstring constraintTerm_print (constraintTerm term)  /*@*/
 
   switch (term->kind)
     {
-    case EXPRNODE:
+    case CTT_EXPR:
 
       s = message ("%s @ %q", exprNode_unparse (term->value.expr),
                   fileloc_unparse (term->loc) );
       break;
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       s = message ("%d", (int)term->value.intlit);
       break;
       
-    case SREF:
+    case CTT_SREF:
       s = message ("%q", sRef_unparseDebug (term->value.sref) );
 
       break;
@@ -352,18 +352,18 @@ constraintTerm constraintTerm_makeIntLiteral (long i)
 {
   constraintTerm ret = new_constraintTermExpr();
   ret->value.intlit = i;
-  ret->kind = INTLITERAL;
+  ret->kind = CTT_INTLITERAL;
   ret->loc =  fileloc_undefined;
   return ret;
 }
 
 bool constraintTerm_canGetValue (constraintTerm term)
 {
-  if (term->kind == INTLITERAL)
+  if (term->kind == CTT_INTLITERAL)
     {
       return TRUE;
     }
-  else if (term->kind == SREF)
+  else if (term->kind == CTT_SREF)
     {
       if (sRef_hasValue (term->value.sref))
        {
@@ -376,7 +376,7 @@ bool constraintTerm_canGetValue (constraintTerm term)
          return FALSE;
        }
     }
-  else if (term->kind == EXPRNODE)
+  else if (term->kind == CTT_EXPR)
     {
       return FALSE;
     }
@@ -390,11 +390,11 @@ long constraintTerm_getValue (constraintTerm term)
 {
   llassert (constraintTerm_canGetValue (term));
 
-  if (term->kind == INTLITERAL)
+  if (term->kind == CTT_INTLITERAL)
     {
       return term->value.intlit; 
     }
-  else if (term->kind == SREF)
+  else if (term->kind == CTT_SREF)
     {
       if (sRef_hasValue (term->value.sref))
        {
@@ -407,7 +407,7 @@ long constraintTerm_getValue (constraintTerm term)
          BADBRANCH;
        }
     }
-  else if (term->kind == EXPRNODE)
+  else if (term->kind == CTT_EXPR)
     {
       BADBRANCH;
     }
@@ -426,7 +426,7 @@ long constraintTerm_getValue (constraintTerm term)
 {
   llassert (t != NULL);
   
-  llassert (t->kind == EXPRNODE);
+  llassert (t->kind == CTT_EXPR);
 
   return t->value.expr;
 
@@ -435,12 +435,12 @@ long constraintTerm_getValue (constraintTerm term)
  /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t)
 {
   llassert (t != NULL);
-  if (t->kind == EXPRNODE)
+  if (t->kind == CTT_EXPR)
     {
       return exprNode_getSref(t->value.expr);
     }
 
-  if (t->kind == SREF)
+  if (t->kind == CTT_SREF)
     {
       return t->value.sref;
     }
@@ -482,7 +482,9 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
   llassert (term1 !=NULL && term2 !=NULL);
   
   if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2))
-    /* evans 2001-07-24: was (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) */
+
+    /*3/30/2003 comment updated to reflect name change form INTLITERAL to CTT_INTLITERAL*/
+    /* evans 2001-07-24: was (term1->kind == CTT_INTLITERAL) && (term2->kind == CTT_INTLITERAL) ) */
     {
       long t1, t2;
 
@@ -542,12 +544,12 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t,  FILE *f)
   switch (kind)
     {
       
-    case EXPRNODE:
+    case CTT_EXPR:
       u = exprNode_getUentry(t->value.expr);
       fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
       break;
       
-    case SREF:
+    case CTT_SREF:
       {
        sRef s;
 
@@ -585,7 +587,7 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t,  FILE *f)
       }
       break;
       
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       fprintf (f, "%ld\n", t->value.intlit);
       break;
       
@@ -620,7 +622,7 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t,  FILE *f)
   switch (kind)
     {
       
-    case SREF:
+    case CTT_SREF:
       {
        sRef s;
        char * term;
@@ -674,7 +676,7 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t,  FILE *f)
       }
       break;
 
-    case EXPRNODE:
+    case CTT_EXPR:
       {
        sRef s;
        char * term;
@@ -699,7 +701,7 @@ void constraintTerm_dump (/*@observer@*/ constraintTerm t,  FILE *f)
       break;
       
       
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       {
        int i;
 
@@ -725,16 +727,16 @@ ctype constraintTerm_getCType (constraintTerm term)
   
   switch (term->kind)
     {
-    case EXPRNODE:
+    case CTT_EXPR:
       ct = exprNode_getType (term->value.expr);
       break;
 
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       /*@i888*/ /* hack */
       ct = ctype_signedintegral;
       break;
       
-    case SREF:
+    case CTT_SREF:
       ct = sRef_getType (term->value.sref) ;
       break;
     default:
@@ -747,7 +749,7 @@ bool constraintTerm_isConstantOnly (constraintTerm term)
 {  
   switch (term->kind)
     {
-    case EXPRNODE:
+    case CTT_EXPR:
       if (exprNode_isNumLiteral (term->value.expr) ||
          exprNode_isStringLiteral (term->value.expr) ||
          exprNode_isCharLiteral  (term->value.expr) )
@@ -759,10 +761,10 @@ bool constraintTerm_isConstantOnly (constraintTerm term)
          return FALSE;
        }
 
-    case INTLITERAL:
+    case CTT_INTLITERAL:
       return TRUE;
             
-    case SREF:
+    case CTT_SREF:
       if ( sRef_isConst (term->value.sref) )
        {
          return TRUE;
index 55c937bfe3a1e2a07869529bd59465d7718694f4..bc91fe91a1cdb8ec3d4cf7fca0b9de4b78610106 100644 (file)
@@ -124,7 +124,7 @@ importCTrait (void)
          callLSL (cstring_makeLiteralTemp (CTRAITSPECNAME),
                   message ("includes %s (%s for String)",
                            cstring_fromChars (CTRAITFILENAMEN), 
-                           cstring_fromChars (sort_getName (sort_cstring))));
+                           cstring_fromChars (sort_getName (g_sortCstring))));
          cstring_free (infile);
          break;
        }
index 1dc52a1e50702b76572dfd6774cdd493b059c4af..2ce2282ab40f46e7d22b9725f63dbb0275bd819a 100644 (file)
@@ -3441,16 +3441,16 @@ case 392:
 { yyval.term = makeSizeofTermNode (yyvsp[-3].ltok, yyvsp[-1].lcltypespec); ;
     break;}
 case 393:
-{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, sort_int); ;
+{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, g_sortInt); ;
     break;}
 case 394:
-{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, sort_cstring); ;
+{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, g_sortCstring); ;
     break;}
 case 395:
-{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, sort_char); ;
+{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, g_sortChar); ;
     break;}
 case 396:
-{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, sort_double); ;
+{ yyval.term = makeLiteralTermNode (yyvsp[0].ltok, g_sortDouble); ;
     break;}
 case 397:
 { yyval.quantifiers = quantifierNodeList_add (quantifierNodeList_new (),  yyvsp[0].quantifier); ;
index e83c59875d6a718871cda78ec2c579ff68ae710f..ab30d80142dfa475f0147d52d68e994715d5c6e9 100644 (file)
@@ -1361,10 +1361,10 @@ lclPrimary
 */
 
 cLiteral   
- : LLT_CINTEGER  { $$ = makeLiteralTermNode ($1, sort_int); }
- | LLT_LCSTRING  { $$ = makeLiteralTermNode ($1, sort_cstring); }
- | LLT_CCHAR     { $$ = makeLiteralTermNode ($1, sort_char); }
- | LLT_CFLOAT    { $$ = makeLiteralTermNode ($1, sort_double); }
+ : LLT_CINTEGER  { $$ = makeLiteralTermNode ($1, g_sortInt); }
+ | LLT_LCSTRING  { $$ = makeLiteralTermNode ($1, g_sortCstring); }
+ | LLT_CCHAR     { $$ = makeLiteralTermNode ($1, g_sortChar); }
+ | LLT_CFLOAT    { $$ = makeLiteralTermNode ($1, g_sortDouble); }
 ;
 
 quantifiers   
index 8136819572495b1e7f2f627ea62834d3ba4da099..cc6e383ecebcda0edd96a7413c24cb5a9c403b07 100644 (file)
@@ -37,7 +37,7 @@
 ** set in LCLScanLineInit of lclscanline.c or in scanline.c 
 */
 
-/*@-namechecks@*/
+/*@-namechecks@*/ /* These should all start with g_ */
 ltoken ltoken_forall;
 ltoken ltoken_exists;
 ltoken ltoken_true;
index 119673872b89ea0c845ee5f2af43c2c3410a68d8..e8266ed0b100f1552aac73b6ac32775497388401 100644 (file)
@@ -110,15 +110,13 @@ static /*@only@*/ nameNode makeArrowFieldOp (lsymbol p_field);
 static lsymbol sp (lsymbol p_s1, lsymbol p_s2);
 static void sortError (ltoken p_t, sort p_oldsort, sortNode p_newnode);
 
-/*@-namechecks@*/
-sort sort_bool;
-sort sort_capBool;
-sort sort_int;
-sort sort_char;
-sort sort_float;
-sort sort_double;
-sort sort_cstring;
-/*@=namechecks@*/
+sort g_sortBool;
+sort g_sortCapBool;
+sort g_sortInt;
+sort g_sortChar;
+sort g_sortFloat;
+sort g_sortDouble;
+sort g_sortCstring;
 
 static sort sort_void;
 static sort char_obj_ptrSort;
@@ -1909,31 +1907,31 @@ sort_init (void)
   
   /* Other builtin sorts */
   
-  sort_bool = sort_makeImmutable (ltoken_undefined, lsymbol_fromChars ("bool"));
-  sort_capBool = sort_makeSortNoOps (ltoken_undefined, lsymbol_fromChars ("Bool"));
+  g_sortBool = sort_makeImmutable (ltoken_undefined, lsymbol_fromChars ("bool"));
+  g_sortCapBool = sort_makeSortNoOps (ltoken_undefined, lsymbol_fromChars ("Bool"));
   
   llassert (sortTable != NULL);
 
-  /* make sort_Bool a synonym for sort_bool */
-  sortTable[sort_capBool]->kind = SRT_SYN;
-  sortTable[sort_capBool]->baseSort = sort_bool;
-  sortTable[sort_capBool]->mutable = FALSE;
-  sortTable[sort_capBool]->abstract = TRUE;
+  /* make g_sortBool a synonym for g_sortBool */
+  sortTable[g_sortCapBool]->kind = SRT_SYN;
+  sortTable[g_sortCapBool]->baseSort = g_sortBool;
+  sortTable[g_sortCapBool]->mutable = FALSE;
+  sortTable[g_sortCapBool]->abstract = TRUE;
   
-  sort_int = sort_makeLiteralSort (ltoken_undefined, 
+  g_sortInt = sort_makeLiteralSort (ltoken_undefined, 
                                   lsymbol_fromChars ("int"));
-  sort_char = sort_makeLiteralSort (ltoken_undefined,
+  g_sortChar = sort_makeLiteralSort (ltoken_undefined,
                                    lsymbol_fromChars ("char"));
   sort_void = sort_makeLiteralSort (ltoken_undefined,
                                    lsymbol_fromChars ("void"));
   
-  /* sort_cstring is char__Vec, for C strings eg: "xyz" */
-  char_obj_ptrSort = sort_makePtr (ltoken_undefined, sort_char);
-  char_obj_ArrSort = sort_makeArr (ltoken_undefined, sort_char);
+  /* g_sortCstring is char__Vec, for C strings eg: "xyz" */
+  char_obj_ptrSort = sort_makePtr (ltoken_undefined, g_sortChar);
+  char_obj_ArrSort = sort_makeArr (ltoken_undefined, g_sortChar);
   
-  sort_cstring = sort_makeVal (char_obj_ArrSort);
-  sort_float = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("float"));
-  sort_double = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("double"));
+  g_sortCstring = sort_makeVal (char_obj_ArrSort);
+  g_sortFloat = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("float"));
+  g_sortDouble = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("double"));
 }
 
 sort
@@ -3082,7 +3080,7 @@ sort_compatible_modulo_cstring (sort s1, sort s2)
     return TRUE;
   syn1 = sort_getUnderlying (s1);
   syn2 = sort_getUnderlying (s2);
-  if (sort_cstring == syn2 &&
+  if (g_sortCstring == syn2 &&
       (syn1 == char_obj_ptrSort || syn1 == char_obj_ArrSort))
     return TRUE;
   return FALSE;
This page took 0.102128 seconds and 5 git commands to generate.