Temporarily set flags to splintme without warnings.

diff --git a/src/Headers/annotationTable.h b/src/Headers/annotationTable.h
index 25898b5908b4f92f5587e8e08e7389f22f335ad5..4360940bf18ec142a6c27fd7c629b111be4de5c0 100644 (file)
--- a/src/Headers/annotationTable.h
+++ b/src/Headers/annotationTable.h
@@ -37,8 +37,10 @@ extern void annotationTable_insert (annotationTable p_h, /*@only@*/ annotationIn
 
 extern /*@null@*/ /*@dependent@*/ /*@exposed@*/ annotationInfo
    annotationTable_lookup (annotationTable p_h, cstring p_key) /*@*/ ;
+/*@access annotationInfo@*/
 # define annotationTable_lookup(p_h,p_key) \
-  (/*@i32@*/ (annotationInfo) genericTable_lookup ((genericTable) (p_h), p_key))
+  ((annotationInfo) genericTable_lookup ((genericTable) (p_h), p_key))
+/*@noaccess annotationInfo@*/
 
 extern bool annotationTable_contains (annotationTable p_h, cstring p_key) /*@*/ ;
 # define annotationTable_contains(p_h,p_key) \

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 173bf5777d415bdeebaaf569b3d5270a844494b6..04b735aa39bbd86eb9d603920887e7f652d6f67c 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -133,7 +133,7 @@ extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_
 extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ;
 extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) ;
 
-extern bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode p_e) ;
+extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ;
 constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c);
 
 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint p_c);

diff --git a/src/Headers/lctype.h b/src/Headers/lctype.h
index 5bf5a5a5150b8c03cde422b59a0b9b1719838931..135d9eaa8bab43ee2a8fa84a675d2c7c509a3adc 100644 (file)
--- a/src/Headers/lctype.h
+++ b/src/Headers/lctype.h
@@ -260,7 +260,9 @@ extern ctype ctype_getBaseType (ctype p_c) /*@*/ ;
 
 extern ctype ctype_makeArray (ctype p_c);
 extern ctype ctype_makeFixedArray (ctype p_c, long p_size);
+extern ctype ctype_makeInnerArray (ctype p_c);
 extern ctype ctype_makeInnerFixedArray (ctype p_c, long p_size);
+
 extern ctype ctype_makeConj (ctype p_c1, ctype p_c2);
 extern ctype ctype_makeParamsFunction (ctype p_base, /*@only@*/ uentryList p_p);
 extern ctype ctype_makeFunction (ctype p_base, /*@only@*/ uentryList p_p) /*@*/ ;

diff --git a/src/Headers/metaStateTable.h b/src/Headers/metaStateTable.h
index b1a504189010f6fe31c14df652e35d77a8379a92..9a419864effef260a65dbbe69d257125937acbb6 100644 (file)
--- a/src/Headers/metaStateTable.h
+++ b/src/Headers/metaStateTable.h
@@ -43,8 +43,10 @@ extern void metaStateTable_insert (metaStateTable p_h,
 extern /*@null@*/ /*@dependent@*/ /*@exposed@*/ metaStateInfo
    metaStateTable_lookup (metaStateTable p_h, cstring p_key) /*@*/ ;
 
+/*@access metaStateInfo@*/ 
 # define metaStateTable_lookup(p_h,p_key) \
-  (/*@i523@*/ /*@access metaStateInfo@*/ (metaStateInfo) genericTable_lookup ((genericTable) (p_h), p_key) /*@noaccess metaStateInfo@*/)
+  ((metaStateInfo) genericTable_lookup ((genericTable) (p_h), p_key))
+/*@noaccess metaStateInfo@*/
 
 extern bool metaStateTable_contains (metaStateTable p_h, cstring p_key) /*@*/ ;
 # define metaStateTable_contains(p_h,p_key) \

diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h
index 0b007f1eee9615308ea2aabd6742d79321ebc828..16a6ab32e9573266f7b240fd7107ea0bab13d9dd 100644 (file)
--- a/src/Headers/sRef.h
+++ b/src/Headers/sRef.h
@@ -145,7 +145,6 @@ extern void sRef_setNullError (sRef p_s);
 extern void sRef_setNullUnknown (sRef p_s, fileloc p_loc);
 extern void sRef_setNotNull (sRef p_s, fileloc p_loc);
 extern void sRef_setNullState (sRef p_s, nstate p_n, fileloc p_loc);
-extern void sRef_setNullStateN (sRef p_s, nstate p_n);
 extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc);
 extern void sRef_setPosNull (sRef p_s, fileloc p_loc);
 extern void sRef_setDefNull (sRef p_s, fileloc p_loc);
@@ -179,6 +178,10 @@ extern bool sRef_hasLastReference (sRef p_s) /*@*/ ;
 extern bool sRef_isMeaningful (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isMeaningful(s)     (sRef_isValid(s) && sRef_isKnown(s) \
                                   && (s)->kind != SK_NEW && (s)->kind != SK_TYPE)
+
+extern bool sRef_isSomewhatMeaningful (/*@sef@*/ sRef p_s) /*@*/ ;
+# define sRef_isSomewhatMeaningful(s)     (sRef_isValid(s) && sRef_isKnown(s) \
+                                          && (s)->kind != SK_TYPE)
 extern bool sRef_isNew (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isNew(s)            (sRef_isValid(s) && (s)->kind == SK_NEW)
 

diff --git a/src/Headers/usymtab.h b/src/Headers/usymtab.h
index e6a5ada4e1d819dab7bae7160019bd67f5db2984..4f418230c74edaf80dc736526f295662b8591d7c 100644 (file)
--- a/src/Headers/usymtab.h
+++ b/src/Headers/usymtab.h
@@ -405,7 +405,7 @@ extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
   /*@modifies *g_msgstream, p_e@*/ ;
 
 extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ;
-
+extern void usymtab_addReallyForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al) /*@modifies internalState@*/ ;
 extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;
 
 # else

diff --git a/src/Headers/valueTable.h b/src/Headers/valueTable.h
index 51efe10b2a9665c7cacf6bec526f9a03b20f5b83..40fcb1a009d68bccafc965e34e714938b1f34709 100644 (file)
--- a/src/Headers/valueTable.h
+++ b/src/Headers/valueTable.h
@@ -55,17 +55,8 @@ extern /*@only@*/ valueTable valueTable_copy (valueTable p_s) ;
 
 /*@iter valueTable_elements (sef valueTable p_g, yield exposed cstring m_key, yield exposed stateValue m_el)@*/
 
-# define valueTable_elements(p_g, m_key, m_el) \
-   { if (valueTable_isDefined (p_g)) {  int m_ind; \
-     { for (m_ind = 0 ; m_ind < (p_g)->size; m_ind++) \
-       { ghbucket m_hb; m_hb = (p_g)->buckets[m_ind]; \
-         if (m_hb != NULL) { \
-           int m_j; \
-           for (m_j = 0; m_j < (m_hb)->size; m_j++) { \
-             cstring m_key; stateValue m_el; m_key = (m_hb)->entries[m_j]->key; \
-   /*@access stateValue@*/ m_el = (stateValue) (m_hb)->entries[m_j]->val; /*@noaccess stateValue@*/
-
-# define end_valueTable_elements }}}}}}
+# define valueTable_elements(p_g, m_key, m_el) genericTable_elements (p_g, m_key, m_el)
+# define end_valueTable_elements end_genericTable_elements
 
 extern int valueTable_size (valueTable p_h) /*@*/ ;
 # define valueTable_size(p_h) (genericTable_size(p_h))

diff --git a/src/Makefile.am b/src/Makefile.am
index c65153181c396e0b98d044dc35a5e07fe75e1316..14ce3498f6c3fd8217d7fc93c1ab89117d49e5b3 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -42,7 +42,7 @@ CSRC = context.c uentry.c cprim.c macrocache.c qual.c qtype.c stateClause.c \
        functionClauseList.c metaStateConstraint.c metaStateConstraintList.c \
        metaStateExpression.c metaStateSpecifier.c functionConstraint.c
 
-SPLINTSRC = exprNode.c exprChecks.c llmain.c $(OVERFLOWCHSRC)
+SPLINTSRC = exprNode.c exprChecks.c llmain.c
 CHECKSRC = structNames.c transferChecks.c varKinds.c nameChecks.c
 
 GLOBSRC = globals.c flags.c general.c osd.c reader.c mtreader.c
@@ -248,7 +248,7 @@ DER_FILES = $(DER_BISON_FILES)
 COMMONSRC =  $(CPPSRC) $(CSRC) $(CHECKSRC) $(GENERALSRC) \
             $(GLOBSRC) $(IFACESRC) $(LISTSRC) $(SETSRC) $(METASTATESRC)
 
-ALLSRC = $(GRAMSRC) $(COMMONSRC) $(SPLINTSRC) $(DER_FILES) $(HEADERSRC)
+ALLSRC = $(GRAMSRC) $(COMMONSRC) $(SPLINTSRC) $(OVERFLOWCHSRC) $(DER_FILES) $(HEADERSRC)
 
 #files to run Splint on
 LINTSRC = $(COMMONSRC) $(SPLINTSRC)
@@ -299,7 +299,7 @@ Headers/cgrammar_tokens.h cgrammar.c: cgrammar.c.der cgrammar.y
          $(CP) cgrammar.c.der cgrammar.c; \
        else \
          echo '* Making cgrammar.c'; \
-         echo '* Expect 145 shift/reduce conflicts and 111 reduce/reduce conflicts.'; \
+         echo '* Expect 154 shift/reduce conflicts and 115 reduce/reduce conflicts.'; \
          echo '* (see cgrammar.y for explanation)'; \
          $(BISON) $(YFLAGS) cgrammar.y; \
          $(CAT) bison.head cgrammar.tab.c bison.reset >cgrammar.c; \
@@ -375,7 +375,12 @@ etags:
 lintnew: splintme
 
 splintme: 
-       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(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 $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw
+
+splintsome: 
+       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude lcllib.c  -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +partial
+
+/* $(LINTSRC) $(LCLSRC)*/
 
 splinttest: 
        ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude cpplib.c +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +keep +supcounts +partial -null

diff --git a/src/Makefile.in b/src/Makefile.in
index 7bbf655fecf257327fc8bc2f4c8d7da5607258ab..2cadafc188e5d37077ce71279f7975831081ecfb 100644 (file)
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -124,7 +124,7 @@ CSRC = context.c uentry.c cprim.c macrocache.c qual.c qtype.c stateClause.c \
        metaStateExpression.c metaStateSpecifier.c functionConstraint.c
 
 
-SPLINTSRC = exprNode.c exprChecks.c llmain.c $(OVERFLOWCHSRC)
+SPLINTSRC = exprNode.c exprChecks.c llmain.c
 CHECKSRC = structNames.c transferChecks.c varKinds.c nameChecks.c
 
 GLOBSRC = globals.c flags.c general.c osd.c reader.c mtreader.c
@@ -333,7 +333,7 @@ COMMONSRC = $(CPPSRC) $(CSRC) $(CHECKSRC) $(GENERALSRC) \
             $(GLOBSRC) $(IFACESRC) $(LISTSRC) $(SETSRC) $(METASTATESRC)
 
 
-ALLSRC = $(GRAMSRC) $(COMMONSRC) $(SPLINTSRC) $(DER_FILES) $(HEADERSRC)
+ALLSRC = $(GRAMSRC) $(COMMONSRC) $(SPLINTSRC) $(OVERFLOWCHSRC) $(DER_FILES) $(HEADERSRC)
 
 #files to run Splint on
 LINTSRC = $(COMMONSRC) $(SPLINTSRC)
@@ -581,7 +581,7 @@ CCLD = $(CC)
 LINK = $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) $(LDFLAGS) -o $@
 CFLAGS = @CFLAGS@
 DIST_SOURCES = $(lcl_SOURCES) $(splint_SOURCES)
-DIST_COMMON = Makefile.am Makefile.in
+DIST_COMMON = ChangeLog Makefile.am Makefile.in
 SOURCES = $(lcl_SOURCES) $(splint_SOURCES)
 
 all: $(BUILT_SOURCES)
@@ -986,7 +986,7 @@ Headers/cgrammar_tokens.h cgrammar.c: cgrammar.c.der cgrammar.y
          $(CP) cgrammar.c.der cgrammar.c; \
        else \
          echo '* Making cgrammar.c'; \
-         echo '* Expect 145 shift/reduce conflicts and 111 reduce/reduce conflicts.'; \
+         echo '* Expect 154 shift/reduce conflicts and 115 reduce/reduce conflicts.'; \
          echo '* (see cgrammar.y for explanation)'; \
          $(BISON) $(YFLAGS) cgrammar.y; \
          $(CAT) bison.head cgrammar.tab.c bison.reset >cgrammar.c; \
@@ -1051,7 +1051,12 @@ etags:
 lintnew: splintme
 
 splintme: 
-       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(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 $(LINTSRC) $(OVERFLOWCHSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw
+
+splintsome: 
+       ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude lcllib.c  -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +partial
+
+/* $(LINTSRC) $(LCLSRC)*/
 
 splinttest: 
        ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude cpplib.c +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw +keep +supcounts +partial -null

diff --git a/src/cgrammar.c.der b/src/cgrammar.c.der
index 6f6f13237f418be6868c76126051c524fca5c255..a8917c31d1927fc29d28943f5f94b969fce01dc1 100644 (file)
--- a/src/cgrammar.c.der
+++ b/src/cgrammar.c.der
@@ -3280,7 +3280,7 @@ case 22:
 { yyval.ntyp = idDecl_expectFunction (yyvsp[-2].ntyp); ;
     break;}
 case 23:
-{ yyval.ntyp = idDecl_replaceCtype (yyvsp[-2].ntyp, ctype_makeArray (idDecl_getCtype (yyvsp[-2].ntyp))); ;
+{ yyval.ntyp = idDecl_replaceCtype (yyvsp[-2].ntyp, ctype_makeInnerArray (idDecl_getCtype (yyvsp[-2].ntyp))); ;
     break;}
 case 24:
 {
@@ -3294,7 +3294,7 @@ case 24:
        } 
      else
        {
-        yyval.ntyp = idDecl_replaceCtype (yyvsp[-5].ntyp, ctype_makeArray (idDecl_getCtype (yyvsp[-5].ntyp))); 
+        yyval.ntyp = idDecl_replaceCtype (yyvsp[-5].ntyp, ctype_makeInnerArray (idDecl_getCtype (yyvsp[-5].ntyp))); 
        }
    ;
     break;}
@@ -3331,7 +3331,7 @@ case 30:
 { yyval.ntyp = idDecl_expectFunction (yyvsp[-2].ntyp); ;
     break;}
 case 31:
-{ yyval.ntyp = idDecl_replaceCtype (yyvsp[-2].ntyp, ctype_makeArray (idDecl_getCtype (yyvsp[-2].ntyp))); ;
+{ yyval.ntyp = idDecl_replaceCtype (yyvsp[-2].ntyp, ctype_makeInnerArray (idDecl_getCtype (yyvsp[-2].ntyp))); ;
     break;}
 case 32:
 { 
@@ -3347,7 +3347,7 @@ case 32:
         value = 0;
        }
 
-     yyval.ntyp = idDecl_replaceCtype (yyvsp[-5].ntyp, ctype_makeFixedArray (idDecl_getCtype (yyvsp[-5].ntyp), value));
+     yyval.ntyp = idDecl_replaceCtype (yyvsp[-5].ntyp, ctype_makeInnerFixedArray (idDecl_getCtype (yyvsp[-5].ntyp), value));
    ;
     break;}
 case 33:
@@ -4649,7 +4649,7 @@ case 469:
 { yyval.ctyp = ctype_makeFixedArray (ctype_unknown, exprNode_getLongValue (yyvsp[-1].expr)); ;
     break;}
 case 470:
-{ yyval.ctyp = ctype_makeArray (yyvsp[-2].ctyp); ;
+{ yyval.ctyp = ctype_makeInnerArray (yyvsp[-2].ctyp); ;
     break;}
 case 471:
 { yyval.ctyp = ctype_makeInnerFixedArray (yyvsp[-3].ctyp, exprNode_getLongValue (yyvsp[-1].expr)); ;

diff --git a/src/cgrammar.y b/src/cgrammar.y
index b9073bac728e0e6ca00291b38eedab1990e66998..5c4f2d8cebf4a6bb51313191a87637f1b7291de7 100644 (file)
--- a/src/cgrammar.y
+++ b/src/cgrammar.y
@@ -372,7 +372,7 @@ namedDeclBase
  | IsType TLPAREN NotType namedDecl IsType TRPAREN
    { $$ = idDecl_expectFunction ($4); }
  | namedDeclBase TLSQBR TRSQBR 
-   { $$ = idDecl_replaceCtype ($1, ctype_makeArray (idDecl_getCtype ($1))); }
+   { $$ = idDecl_replaceCtype ($1, ctype_makeInnerArray (idDecl_getCtype ($1))); }
  | namedDeclBase TLSQBR IsType constantExpr TRSQBR NotType
    {
      exprNode_findValue ($4);
@@ -385,7 +385,7 @@ namedDeclBase
        } 
      else
        {
-        $$ = idDecl_replaceCtype ($1, ctype_makeArray (idDecl_getCtype ($1))); 
+        $$ = idDecl_replaceCtype ($1, ctype_makeInnerArray (idDecl_getCtype ($1))); 
        }
    }
  | namedDeclBase PushType TLPAREN TRPAREN 
@@ -416,7 +416,7 @@ plainNamedDeclBase
  | IsType TLPAREN NotType plainNamedDecl IsType TRPAREN
    { $$ = idDecl_expectFunction ($4); }
  | plainNamedDeclBase TLSQBR TRSQBR 
-   { $$ = idDecl_replaceCtype ($1, ctype_makeArray (idDecl_getCtype ($1))); }
+   { $$ = idDecl_replaceCtype ($1, ctype_makeInnerArray (idDecl_getCtype ($1))); }
  | plainNamedDeclBase TLSQBR IsType constantExpr TRSQBR NotType
    { 
      int value;
@@ -431,7 +431,7 @@ plainNamedDeclBase
         value = 0;
        }
 
-     $$ = idDecl_replaceCtype ($1, ctype_makeFixedArray (idDecl_getCtype ($1), value));
+     $$ = idDecl_replaceCtype ($1, ctype_makeInnerFixedArray (idDecl_getCtype ($1), value));
    }
  | plainNamedDeclBase PushType TLPAREN TRPAREN 
    { setCurrentParams (uentryList_missingParams); }
@@ -1456,7 +1456,7 @@ abstractDeclBase
  | TLSQBR TRSQBR { $$ = ctype_makeArray (ctype_unknown); }
  | TLSQBR constantExpr TRSQBR 
    { $$ = ctype_makeFixedArray (ctype_unknown, exprNode_getLongValue ($2)); }
- | abstractDeclBase TLSQBR TRSQBR { $$ = ctype_makeArray ($1); }
+ | abstractDeclBase TLSQBR TRSQBR { $$ = ctype_makeInnerArray ($1); }
  | abstractDeclBase TLSQBR constantExpr TRSQBR 
    { $$ = ctype_makeInnerFixedArray ($1, exprNode_getLongValue ($3)); }
  | IsType TLPAREN TRPAREN 

diff --git a/src/constraint.c b/src/constraint.c
index ccdb179aaaca235e2903933af061c8690b920dae..e62b55b8688ea20cfbc7b2d8558188321e5b9044 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -39,8 +39,10 @@
 
 /*@i33*/
 
-/*@access exprNode @*/
-
+/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
 
 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
 

diff --git a/src/constraintExpr.c b/src/constraintExpr.c
index 4249d9ca48bc0b682b3391f05b6bb9ce3a2ed6ce..1ea7f54e41ad4e2de44bc3760f35477ae3cb2ff0 100644 (file)
--- a/src/constraintExpr.c
+++ b/src/constraintExpr.c
@@ -38,10 +38,12 @@
 
 /*@-czechfcns@*/
 
+/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
 
 
-/*@access exprNode constraintExpr@*/
-
 static ctype constraintExpr_getOrigType (constraintExpr p_e);
 static bool constraintExpr_hasTypeChange(constraintExpr p_e) /*@*/;
 

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index 6a71ce16052544b59abbbd2a6d9a870ec1af0836..6331979a9cc18aa32bdc93fe5a8af215f4e75aa1 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -37,8 +37,10 @@
 # include "exprChecks.h"
 # include "exprNodeSList.h"
 
-/*@access exprNode @*/
-
+/*@access exprNode@*/ /* NO! Don't do this recklessly! */
+/*@-nullderef@*/ /* DRL needs to fix this code! */
+/*@-nullpass@*/ /* DRL needs to fix this code! */
+/*@-temptrans@*/ /* DRL needs to fix this code! */
 
 static /*@truewhennull@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e);
 
@@ -548,9 +550,8 @@ static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred,
 
 static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/  exprNode e)
 {
-  /*@-temptrans@*/
+  /* !!! DRL - this is ridiculous!  Read the manual on memory annotations please! */
   return e;
-  /*@=temptrans@*/  
 }
 
 static void 

diff --git a/src/constraintList.c b/src/constraintList.c
index 99dc7e747e9b6438f50d6e731dec52fcca54cba2..e23047ce2501fa8602fca0a5197def048c6a4681 100644 (file)
--- a/src/constraintList.c
+++ b/src/constraintList.c
@@ -33,6 +33,10 @@
 # include "splintMacros.nf"
 # include "llbasic.h"
 
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-nullpass@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
 
 /*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
 # define constraintList_elements_private_only(x, m_el) \

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index eefac7fb39d6afe70d85d3d2fb828e31f9a99fb5..9cbc788d2feed66d4cdd39d7e2cdf0a3987efddd 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -39,7 +39,13 @@
 # include "exprNodeSList.h"
 
 
-/*@access constraint, exprNode @*/
+/*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */
+
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-nullpass@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
+
 
 
 static constraint  inequalitySubstitute  (/*@returned@*/ constraint p_c, constraintList p_p);

diff --git a/src/constraintTerm.c b/src/constraintTerm.c
index 8d1aa1306a42f8d319effd00326941488f61a6e7..a309c9d6d0d119ce98113944339d4470f84180c7 100644 (file)
--- a/src/constraintTerm.c
+++ b/src/constraintTerm.c
@@ -38,8 +38,12 @@
 # include "exprNodeSList.h"
 
 /*@-czechfcns@*/
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-nullpass@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
 
-/*@access exprNode @*/
+/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
 
 bool constraintTerm_isDefined (constraintTerm t)
 {

diff --git a/src/cstring.c b/src/cstring.c
index 4f3dd7a4ef7c779e4b4380186a491d44061d769c..3408eaf2388deee05cc889775f66d9fe396aa37b 100644 (file)
--- a/src/cstring.c
+++ b/src/cstring.c
@@ -910,6 +910,9 @@ extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s)
   return cstring_undefined;
 }
 
+/*@i3534 @*/
+/*@ignore@*/
+
 /* changes strings like "sdf" "sdfsd" into "sdfsdfsd"*/
 /* This function understands that "sdf\"  \"sdfsdf" is okay*/
 static mstring doMergeString (cstring s)
@@ -1175,3 +1178,12 @@ cstring cstring_replaceChar(/*@returned@*/ cstring c, char oldChar, char newChar
 
   return c;
 }
+
+/*@end@*/
+
+
+
+
+
+
+

diff --git a/src/ctype.c b/src/ctype.c
index 31aacd0c3d47df0e3107dc4a7ad470ee8083a51d..3384cb65e4b2878801883a24a544b2afdfb86859 100644 (file)
--- a/src/ctype.c
+++ b/src/ctype.c
@@ -334,11 +334,41 @@ ctype ctype_makeInnerFixedArray (ctype c, long size)
       res = ctype_makeFixedArray (ctype_makeInnerFixedArray (cb, size),
                                  osize);
     }
+  else if (ctype_isArray (c))
+    {
+      ctype cb = ctype_baseArrayPtr (c);
+
+      res = ctype_makeArray (ctype_makeInnerFixedArray (cb, size));
+    }
   else
     {
       res = ctype_makeFixedArray (c, size);
     }
 
+  DPRINTF (("Make inner fixed array: %s", ctype_unparse (res)));
+  return res;
+}
+
+ctype ctype_makeInnerArray (ctype c)
+{
+  ctype res;
+
+  DPRINTF (("Make inner array: %s", ctype_unparse (c)));
+
+  if (ctype_isFixedArray (c))
+    {
+      ctype cb = ctype_baseArrayPtr (c);
+      long osize = ctype_getArraySize (c);
+
+      res = ctype_makeFixedArray (ctype_makeInnerArray (cb),
+                                 osize);
+    }
+  else
+    {
+      res = ctype_makeArray (c);
+    }
+
+  DPRINTF (("Make inner array: %s", ctype_unparse (res)));
   return res;
 }
 
@@ -348,6 +378,8 @@ ctype_makeArray (ctype c)
   ctentry cte = ctype_getCtentry (c);
   ctype clp = ctentry_getArray (cte);
 
+  DPRINTF (("Make array: %s", ctype_unparse (c)));
+
   if /*@+enumint@*/ (clp == CTK_DNE) /*@=enumint@*/
     {
       ctype cnew = cttable_addDerived (CTK_ARRAY, ctbase_makeArray (c), c);
@@ -355,7 +387,9 @@ ctype_makeArray (ctype c)
       return (cnew);
     }
   else
-    return clp;
+    {
+      return clp;
+    }
 }
 
 /*

diff --git a/src/exprNode.c b/src/exprNode.c
index f3040f796fa2efb93015898828b3076726afab58..6c41838b68fe4230a5791363c18db1b77aadf859 100644 (file)
--- a/src/exprNode.c
+++ b/src/exprNode.c
@@ -1652,8 +1652,11 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn,
                          
                        case 'p': /* pointer */
                          expecttype = ctype_makePointer (ctype_void);
-                         uentry_setDefState (regArg, SS_RELDEF); /* need not be defined */
-                         sRef_setPosNull (uentry_getSref (regArg), fileloc_undefined); /* could be null */
+                         /* need not be defined */
+                         uentry_setDefState (regArg, SS_RELDEF); 
+                         sRef_setPosNull (uentry_getSref (regArg), 
+                                          fileloc_undefined); 
+                         /* could be null */
                          /*@switchbreak@*/ break;
                          
                        case 'n': /* pointer to int, modified by call! */
@@ -2186,6 +2189,14 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f,
                        case 'f': expecttype = ctype_float; break;
                        case 'b': expecttype = ctype_bool; break;
                        case 't': expecttype = ctypeType; break;
+                       case 'p': 
+                         expecttype = ctype_makePointer (ctype_void);
+                         /* need not be defined */
+                         uentry_setDefState (regArg, SS_RELDEF); 
+                         sRef_setPosNull (uentry_getSref (regArg), 
+                                          fileloc_undefined); 
+                         /* could be null */
+                         /*@switchbreak@*/ break;
                        case 'l': expecttype = filelocType; break;
                        case '&':  /* a wee bit of a hack methinks */
                          expecttype = ctype_int;

diff --git a/src/lcllib.c b/src/lcllib.c
index efaa31fe5cb40ffacface938ed52291c2319edca..a9e19003e20ee6e5e6170adcc5a9d1c4e7f72e66 100644 (file)
--- a/src/lcllib.c
+++ b/src/lcllib.c
@@ -226,7 +226,15 @@ lcllib_isSkipHeader (cstring sname)
          if (context_getFlag (FLG_SKIPPOSIXHEADERS))
            {
              cstring_free (xname);
-             return TRUE; /* evans 2002-03-02: investigate this warning */
+             /*@-nullstate@*/ 
+             return TRUE; 
+             /*@=nullstate@*/
+             /*@i233@*/
+             /* evans 2002-03-02: 
+                the returned reference is possibly null,
+                but this should not change the null state of the parameter
+                investigate this warning 
+             */
            }
        }
       else
@@ -250,7 +258,9 @@ lcllib_isSkipHeader (cstring sname)
 
   cstring_free (xname);
   /*@noaccess cstring@*/
+  /*@-nullstate@*/ /*@i233@*/ /* same problem as above */
   return FALSE;
+  /*@=nullstate@*/
 }
 
 static void printDot (void)

diff --git a/src/loopHeuristics.c b/src/loopHeuristics.c
index c8057c1d14ba31a9ac716c3b8a59eb2ec8217683..4f7e46c90028daaa507e7cb2ef85a528d31d6f48 100644 (file)
--- a/src/loopHeuristics.c
+++ b/src/loopHeuristics.c
@@ -43,9 +43,14 @@
 
 # include "exprDataQuite.i"
 
-/*@access constraint, exprNode @*/
+/*@access constraint, exprNode @*/  /* !!! NO! */
 
-/*@access constraintExpr @*/
+/*@access constraintExpr @*/ /* !!! NO! */
+
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-nullpass@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
 
 static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
 {
@@ -254,7 +259,10 @@ static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*
 
          }
        else
-         DPRINTF (( message ("getForTimes: %s doesn't increment %s", constraint_print (el2), constraint_print (el) )   ));
+         {
+           ;
+           DPRINTF (( message ("getForTimes: %s doesn't increment %s", constraint_print (el2), constraint_print (el) )   ));
+         }
       }
       end_constraintList_elements;
     }

diff --git a/src/sRef.c b/src/sRef.c
index ed43a689062d4329db77d57e92e1e07b8f1460e7..e3f22df58321373ad7da26e23c1ed23ecc3c0a6d 100644 (file)
--- a/src/sRef.c
+++ b/src/sRef.c
@@ -62,6 +62,7 @@ static void sRef_updateNullState (sRef p_res, sRef p_other) /*@modifies p_res@*/
 
 static bool sRef_isAllocatedStorage (sRef p_s) /*@*/ ;
 static void sRef_setNullErrorLoc (sRef p_s, fileloc) /*@*/ ;
+static void sRef_setNullStateN (sRef p_s, nstate p_n) /*@modifies p_s@*/ ;
 
 static int sRef_depth (sRef p_s) /*@*/ ;
 
@@ -3728,8 +3729,8 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
   llassertfatal (sRef_isValid (other));
   
   DPRINTF (("Merge aux: %s / %s",
-           bool_unparse (sRef_isDefinitelyNull (res)),
-           bool_unparse (sRef_isDefinitelyNull (other))));
+           sRef_unparseFull (res),
+           sRef_unparseFull (other)));
 
   sRef_checkMutable (res);
   sRef_checkMutable (other);
@@ -3989,6 +3990,9 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
   } end_valueTable_elements ; 
 # endif
 
+  DPRINTF (("Merge aux: %s / %s",
+           sRef_unparseFull (res),
+           sRef_unparseFull (other)));
 }
 
 static sRefSet
@@ -4509,8 +4513,8 @@ sRef_makeUnsafe (sRef s)
 {
   if (sRef_isInvalid (s)) return (cstring_undefined);
 
-  return (message ("[%d] %q - %q [%s] { %q } < %q >", 
-                  (int) s,
+  return (message ("[%p] %q - %q [%s] { %q } < %q >", 
+                  s,
                   sRef_unparseDebug (s), 
                   sRef_unparseState (s),
                   exkind_unparse (s->oexpkind),
@@ -5398,7 +5402,6 @@ void sRef_setLastReference (sRef s, /*@exposed@*/ sRef ref, fileloc loc)
 static
 void sRef_setNullStateAux (/*@notnull@*/ sRef s, nstate ns, fileloc loc)
 {
-  DPRINTF (("Set null state: %s / %s", sRef_unparse (s), nstate_unparse (ns)));
   sRef_checkMutable (s);
   s->nullstate = ns;
   sRef_resetAliasKind (s);
@@ -5804,7 +5807,7 @@ sRef sRef_copy (sRef s)
       t->deriv = sRefSet_newDeepCopy (s->deriv);
       t->state = valueTable_copy (s->state);
 
-      DPRINTF (("Made copy: [%p] %s", t, sRef_unparse (t)));
+      DPRINTF (("Made copy: %s => %s", sRef_unparseFull (s), sRef_unparseFull (t)));
       return t;
     }
   else
@@ -6355,6 +6358,7 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
                }
            }
 
+         DPRINTF (("Set null state: %s / %s", sRef_unparseFull (s), sRef_unparseFull (sp)));
          sRef_setNullStateN (s, sRef_getNullState (sp));
        }
       else
@@ -6541,7 +6545,9 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
       s->info->arrayfetch->indknown = FALSE;
       s->info->arrayfetch->ind = 0;
       s->info->arrayfetch->arr = arr; /* sRef_copy (arr); */ /*@i32@*/
+
       sRef_setArrayFetchState (s, arr);
+
       s->oaliaskind = s->aliaskind;
       s->oexpkind = s->expkind;
 
@@ -6554,7 +6560,7 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
        {
          s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
        }
-
+      
       return (s);
     }
 }
@@ -6642,7 +6648,7 @@ sRef_setPartsFromUentry (sRef s, uentry ue)
   
   if (sRef_getNullState (s) == NS_UNKNOWN)
     {
-      DPRINTF (("Setting null state!"));
+      DPRINTF (("Set null state: %s / %s", sRef_unparseFull (s), uentry_unparseFull (ue)));
       sRef_setNullStateN (s, sRef_getNullState (uentry_getSref (ue)));
     }
   else
@@ -6902,8 +6908,7 @@ sRef_clearDerivedComplete (sRef s)
 
 /*@exposed@*/ sRef
 sRef_makeAnyArrayFetch (/*@exposed@*/ sRef arr)
-{
-  
+{  
   if (sRef_isAddress (arr))
     {
       return (arr->info->ref);
@@ -7122,7 +7127,7 @@ sRef_copyState (sRef s1, sRef s2)
 
       s1->expkind = s2->expkind;
       s1->expinfo = stateInfo_update (s1->expinfo, s2->expinfo);
-      
+
       s1->nullstate = s2->nullstate;
       s1->nullinfo = stateInfo_update (s1->nullinfo, s2->nullinfo);
 
@@ -8328,6 +8333,7 @@ sRef_aliasSetComplete (void (predf) (sRef, fileloc), sRef s, fileloc loc)
        {
          current = sRef_updateSref (current);
          ((*predf)(current, loc));
+         DPRINTF (("Killed: %s", sRef_unparseFull (current)));
        }
     } end_sRefSet_realElements;
 

diff --git a/src/uentry.c b/src/uentry.c
index fcea58ca7eee40a955570b57e04d90d012328ca2..675df280ae3f062e8d51daeffb653fcef39bbb9c 100644 (file)
--- a/src/uentry.c
+++ b/src/uentry.c
@@ -10613,6 +10613,207 @@ bool uentry_isReturned (uentry u)
              || u->info->var->kind == VKSEFRETPARAM));
 }
 
+/*@i52323@*/
+# if 0
+/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args)
+{
+  llassert (uentry_isRealFunction (u));
+
+  if (ctype_isFunction (u->utype) && sRef_isStateSpecial (uentry_getSref (u)))
+    {
+      stateClauseList clauses = uentry_getStateClauseList (u);
+      sRef res = sRef_makeNew (ctype_getReturnType (u->utype), u->sref, u->uname);
+
+      DPRINTF (("Returned: %s", sRef_unparseFull (res)));
+      sRef_setAllocated (res, g_currentloc);
+
+      DPRINTF (("ensures clause: %s / %s", uentry_unparse (u), 
+               stateClauseList_unparse (clauses)));
+
+      /*
+      ** This should be in exprNode_reflectEnsuresClause
+      */
+
+      stateClauseList_postElements (clauses, cl)
+       {
+         if (!stateClause_isGlobal (cl))
+           {
+             sRefSet refs = stateClause_getRefs (cl);
+             sRefMod modf = stateClause_getEffectFunction (cl);
+             
+             sRefSet_elements (refs, el)
+               {
+                 sRef base = sRef_getRootBase (el);
+                 
+                 if (sRef_isResult (base))
+                   {
+                     if (modf != NULL)
+                       {
+                         sRef sr = sRef_fixBase (el, res);
+                         modf (sr, g_currentloc);
+                       }
+                   }
+                 else
+                   {
+                     ;
+                   }
+               } end_sRefSet_elements ;
+           }
+       } end_stateClauseList_postElements ;
+       
+      return res;
+    }
+  else
+    {
+      uentryList params;
+      alkind ak;
+      sRefSet prefs = sRefSet_new ();
+      sRef res = sRef_undefined;
+      sRef tcref = sRef_undefined;
+      sRef tref = sRef_undefined;
+      int paramno = 0;
+      
+      params = uentry_getParams (u);
+
+      /*
+      ** Setting up aliases has to happen *after* setting null state!
+      */
+
+      uentryList_elements (params, current)
+       {
+         if (uentry_isReturned (current))
+           {
+             if (exprNodeList_size (args) >= paramno)
+               {
+                 exprNode ecur = exprNodeList_nth (args, paramno);
+                 tref = exprNode_getSref (ecur);
+                 
+                 DPRINTF (("Returned reference: %s", sRef_unparseFull (tref)));
+
+                 if (sRef_isValid (tref))
+                   {
+                     tcref = sRef_copy (tref);
+                     
+                     if (sRef_isDead (tcref))
+                       {
+                         sRef_setDefined (tcref, g_currentloc);
+                         sRef_setOnly (tcref, g_currentloc);
+                       }
+                     
+                     if (sRef_isRefCounted (tcref))
+                       {
+                         /* could be a new ref now (but only if its returned) */
+                         sRef_setAliasKindComplete (tcref, AK_ERROR, g_currentloc);
+                       }
+                     
+                     sRef_makeSafe (tcref);
+                     prefs = sRefSet_insert (prefs, tcref);
+                   }
+               }
+           }
+         
+         paramno++;
+       } end_uentryList_elements ;
+
+      if (sRefSet_size (prefs) > 0)
+       {
+         nstate n = sRef_getNullState (u->sref);
+
+         if (sRefSet_size (prefs) == 1)
+           {
+             sRef rref = sRefSet_choose (prefs);
+             tref = rref;
+             res = sRef_makeType (sRef_getType (rref));
+             sRef_copyState (res, tref);
+           }
+         else
+           {
+             /* should this ever happen? */ /*@i534 evans 2001-05-27 */
+             res = sRefSet_mergeIntoOne (prefs);
+           }
+         
+         if (nstate_isKnown (n))
+           {
+             sRef_setNullState (res, n, g_currentloc);
+             DPRINTF (("Setting null: %s", sRef_unparseFull (res)));
+           }
+       }
+      else
+       {
+         if (ctype_isFunction (u->utype))
+           {
+             DPRINTF (("Making new from %s  -->", uentry_unparseFull (u)));
+             res = sRef_makeNew (ctype_getReturnType (u->utype), u->sref, u->uname);
+           }
+         else
+           {
+             DPRINTF (("Making new from %s  -->", uentry_unparseFull (u)));
+             res = sRef_makeNew (ctype_unknown, u->sref, u->uname);
+           }
+         
+         if (sRef_isRefCounted (res))
+           {
+             sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
+           }
+       }
+      
+      if (sRef_getNullState (res) == NS_ABSNULL)
+       {
+         ctype ct = ctype_realType (u->utype);
+         
+         if (ctype_isAbstract (ct))
+           {
+             sRef_setNotNull (res, g_currentloc);
+           }
+         else
+           {
+             if (ctype_isUser (ct))
+               {
+                 sRef_setStateFromUentry (res, usymtab_getTypeEntry (ctype_typeId (ct)));
+               }
+             else
+               {
+                 sRef_setNotNull (res, g_currentloc);
+               }
+           }
+       }
+      
+      if (sRef_isRefCounted (res))
+       {
+         sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
+       }
+      else if (sRef_isKillRef (res))
+       {
+         sRef_setAliasKind (res, AK_REFCOUNTED, g_currentloc);
+       }
+      else
+       {
+         ;
+       }
+      
+      ak = sRef_getAliasKind (res);
+      
+      if (alkind_isImplicit (ak))
+       {
+         sRef_setAliasKind (res, alkind_fixImplicit (ak), g_currentloc);
+       }
+
+# if 0
+      DPRINTF (("Aliasing: %s / %s", sRef_unparseFull (res), sRef_unparseFull (tref)));
+      usymtab_addReallyForceMustAlias (tref, res); /* evans 2001-05-27 */
+
+      /* evans 2002-03-03 - need to be symettric explicitly, since its not a local now */
+      usymtab_addReallyForceMustAlias (res, tref);
+# endif
+
+      sRefSet_free (prefs);
+      
+      DPRINTF (("Returns ref: %s", sRef_unparseFull (res)));
+      return res;
+    }
+}
+# endif
+
 /*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args)
 {
   llassert (uentry_isRealFunction (u));

diff --git a/src/usymtab.c b/src/usymtab.c
index 3d3f1a9d797935ec518b69af88d2faac35ae238d..b5a8f98d7820c224b71153d576ac7a46120e05d1 100644 (file)
--- a/src/usymtab.c
+++ b/src/usymtab.c
@@ -2905,13 +2905,17 @@ updateNullState (sRef el, /*@notnull@*/ usymtab ttab,
              if (!guardSet_isGuarded (ttab->guards, el) 
                  && !sRef_isNotNull (sr))
                {
+                 DPRINTF (("Here! %s / %s",
+                           sRef_unparseFull (sr),
+                           sRef_unparseFull (el)));
                  sRef_setDerivNullState (sr, el, NS_DEFNULL);
-                               }
+               }
            }
        }
       else
        {
-               }
+         ;
+       }
       
       ue = usymtab_getRefTab (ftab, level, index);
       
@@ -2919,7 +2923,6 @@ updateNullState (sRef el, /*@notnull@*/ usymtab ttab,
        {
          sRef sr = uentry_getSref (ue);
          
-         
          if (!trueGuard) /* yikes!  forgot the ! */
            {
              sRef_setDerivNullState (sr, el, NS_NOTNULL);
@@ -2931,7 +2934,7 @@ updateNullState (sRef el, /*@notnull@*/ usymtab ttab,
                  && !sRef_isNotNull (sr))
                {
                  sRef_setDerivNullState (sr, el, NS_DEFNULL);
-                               }
+               }
            }
        }
       else
@@ -3693,7 +3696,7 @@ checkGlobalReturn (uentry glob, sRef orig)
          else
            {
              ctype ct = ctype_realType (uentry_getType (glob));
-
+             
              DPRINTF (("Check global destroyed: %s", uentry_unparseFull (glob)));
 
              if (ctype_isVisiblySharable (ct))
@@ -3771,6 +3774,7 @@ checkGlobalReturn (uentry glob, sRef orig)
                }
              else
                {
+                 DPRINTF (("Check transfer: %s", uentry_unparseFull (glob)));
                  transferChecks_globalReturn (glob);
                }
            }
@@ -5648,6 +5652,7 @@ void usymtab_addMustAlias (/*@exposed@*/ sRef s, /*@exposed@*/ sRef al)
 void usymtab_addForceMustAlias (/*@exposed@*/ sRef s, /*@exposed@*/ sRef al)
   /*@modifies utab@*/
 {
+  /* evans 2002-03-3: was sRef_isMeaningful -- but we need to keep aliases for new storage also! */
   if (sRef_isMeaningful (s) 
       && sRef_isMeaningful (al)
       && !(sRef_isConst (s) || sRef_isConst (al))
@@ -5667,10 +5672,17 @@ void usymtab_addForceMustAlias (/*@exposed@*/ sRef s, /*@exposed@*/ sRef al)
     }
   else
     {
-      ;
+      DPRINTF (("Not aliasing! %s / %s", sRef_unparseFull (s), sRef_unparseFull (al)));
+      DPRINTF (("meaningful: %d %d", sRef_isMeaningful (s), sRef_isMeaningful (al)));
     }
 }
 
+void usymtab_addReallyForceMustAlias (/*@exposed@*/ sRef s, /*@exposed@*/ sRef al)
+  /*@modifies utab@*/
+{
+  utab->aliases = aliasTable_addMustAlias (utab->aliases, s, al); 
+}
+
 void usymtab_clearAlias (sRef s)
   /*@modifies utab, s@*/
 {
@@ -5681,7 +5693,7 @@ void usymtab_clearAlias (sRef s)
 sRefSet usymtab_allAliases (sRef s)
    /*@globals utab@*/  
 {
-  if (sRef_isMeaningful (s))
+  if (sRef_isSomewhatMeaningful (s))
     {
       sRefSet ret;
             
@@ -5699,7 +5711,7 @@ sRefSet usymtab_allAliases (sRef s)
 /*@only@*/ sRefSet usymtab_canAlias (sRef s)
      /*@globals utab@*/
 {
-  if (sRef_isMeaningful (s))
+  if (sRef_isSomewhatMeaningful (s))
     {
       sRefSet res = aliasTable_canAlias (utab->aliases, s);
       return res;

diff --git a/test/Makefile.am b/test/Makefile.am
index e14febf654da8bccf51ddf767265c0451397cc16..ebb22b6f92580f4d6e6dae37634c8b2cbe82e975 100644 (file)
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -37,7 +37,7 @@ SPLINTRNEST   = $(SPLINTRNNEST) -exportlocal +debugfcnconstraint
 UNITTESTS = \
   help \
   abstptr abstract alias alttypes ansireserved argorder \
-  args arraydims blocks break cases cast charlit clauses commentchar compdestroy \
+  args arraydims arrayinit blocks break cases cast charlit clauses commentchar compdestroy \
   compoundliterals compoundstmt constannot controldepth csyntax czechnames czechoslovaknames deadparam \
   decl divzero enum exports external fields flags forbody format freearray \
   funcpointer functionmacro glob globals impabstract info init inparam internal iter keep libs \
@@ -222,6 +222,10 @@ arraydims:
        -$(SPLINTR) arraydims.c -varuse -expect 2
        -$(SPLINTR) arraydims.c -initsize -varuse
 
+.PHONY: arrayinit
+arrayinit:
+       -$(SPLINTR) arrayinit.c -expect 9
+
 .PHONY: blocks
 blocks:
        -$(SPLINTR) blocks.c -expect 4

diff --git a/test/Makefile.in b/test/Makefile.in
index f9ae307ee8f2fb4e1b7bc08c060199fb037eb178..1b157b94e273f1ccf39f56916b7e60e880c9d231 100644 (file)
--- a/test/Makefile.in
+++ b/test/Makefile.in
@@ -114,7 +114,7 @@ SPLINTRNEST = $(SPLINTRNNEST) -exportlocal +debugfcnconstraint
 UNITTESTS = \
   help \
   abstptr abstract alias alttypes ansireserved argorder \
-  args arraydims blocks break cases cast charlit clauses commentchar compdestroy \
+  args arraydims arrayinit blocks break cases cast charlit clauses commentchar compdestroy \
   compoundliterals compoundstmt constannot controldepth csyntax czechnames czechoslovaknames deadparam \
   decl divzero enum exports external fields flags forbody format freearray \
   funcpointer functionmacro glob globals impabstract info init inparam internal iter keep libs \
@@ -1041,6 +1041,10 @@ arraydims:
        -$(SPLINTR) arraydims.c -varuse -expect 2
        -$(SPLINTR) arraydims.c -initsize -varuse
 
+.PHONY: arrayinit
+arrayinit:
+       -$(SPLINTR) arrayinit.c -expect 9
+
 .PHONY: blocks
 blocks:
        -$(SPLINTR) blocks.c -expect 4

diff --git a/test/arrayinit.c b/test/arrayinit.c
index ff985b9c0084551be1129d739414789dfb3e8cd9..215f56a99663c5eeb384f2f36be529cdd27a7076 100644 (file)
--- a/test/arrayinit.c
+++ b/test/arrayinit.c
@@ -12,3 +12,6 @@ char cs2[3] = "abcd"; /* gcc warns for this with -Wall */ /* stringliteraltoolon
 char cs3[3] = "a"; /* stringliteral smaller (not on default) */ 
 
 char csx[3][3] = { { 'a', 'b', 'c' } , "def", "gasdf" } ; /* 2 errors */
+
+int a2[][2] = {{1,2},{3,4},{5,6}};
+int a3[][2] = {{1,2},{3,4,5},{5,6}};

diff --git a/test/arrayinit.expect b/test/arrayinit.expect
index f7ed636619095dfff6ce167705c5cca15a96203f..cdc2b08aea13b945389e8869e356849c7059f354 100644 (file)
--- a/test/arrayinit.expect
+++ b/test/arrayinit.expect
@@ -7,34 +7,15 @@ arrayinit.c:3:16: Initializer block for aa has 2 elements, but declared as int
                      [3] [3]: { 1, 2, 3 }, { 4, 5 }
 arrayinit.c:4:18: Initializer block for aa[1] has 2 elements, but declared as
                      int [3]: 4, 5
-arrayinit.c:10:15: String literal with 3 characters is assigned to char [3] (no
+arrayinit.c:10:15: String literal with 4 characters is assigned to char [3] (no
                       room for null terminator): "abc"
-arrayinit.c:11:15: Stirng literal with 4 characters (counting null terminator)
+arrayinit.c:11:15: String literal with 5 characters (counting null terminator)
     is assigned to char [3] (insufficient storage available): "abcd"
-arrayinit.c:14:40: String literal with 3 characters is assigned to char [3] (no
+arrayinit.c:14:40: String literal with 4 characters is assigned to char [3] (no
                       room for null terminator): "def"
-arrayinit.c:14:47: Stirng literal with 5 characters (counting null terminator)
+arrayinit.c:14:47: String literal with 6 characters (counting null terminator)
     is assigned to char [3] (insufficient storage available): "gasdf"
+arrayinit.c:17:22: Initializer block for a3[1] has 3 elements, but declared as
+                      int [2]: 3, 4, 5
 
-Finished LCLint checking --- 8 code errors found, as expected
-
-arrayinit.c:1:12: Initializer block for x has 4 elements, but declared as int
-                     [3]: 1, 2, 3, 4
-arrayinit.c:2:12: Initializer block for a has 2 elements, but declared as int
-                     [3]: 1, 2
-arrayinit.c:3:16: Initializer block for aa has 2 elements, but declared as int
-                     [3] [3]: { 1, 2, 3 }, { 4, 5 }
-arrayinit.c:4:18: Initializer block for aa[1] has 2 elements, but declared as
-                     int [3]: 4, 5
-arrayinit.c:10:15: String literal with 3 characters is assigned to char [3] (no
-                      room for null terminator): "abc"
-arrayinit.c:11:15: Stirng literal with 4 characters (counting null terminator)
-    is assigned to char [3] (insufficient storage available): "abcd"
-arrayinit.c:12:15: String literal with 1 character is assigned to char [3]
-                      (possible waste of storage): "a"
-arrayinit.c:14:40: String literal with 3 characters is assigned to char [3] (no
-                      room for null terminator): "def"
-arrayinit.c:14:47: Stirng literal with 5 characters (counting null terminator)
-    is assigned to char [3] (insufficient storage available): "gasdf"
-
-Finished LCLint checking --- 9 code errors found, as expected
+Finished checking --- 9 code warnings, as expected