Added the flags likely-bounds, likely-bounds-write, and likely-bounds-read

Correspond to error messages for constraints that have only constants.

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 04b735aa39bbd86eb9d603920887e7f652d6f67c..410febd206cffe2df3fe2b91b0fdb5bb81d9b5b7 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -159,7 +159,9 @@ void exprNode_findValue( exprNode p_e);
 /*drl 1/6/2001: I didn't think these functions were solid enough to include in the   stable  release of splint.*/
 /*drl added 12/30/01 */
 /* extern / *@only@* / constraint  constraint_doSRefFixInvarConstraint(constraint p_invar, sRef p_s, ctype p_ct ); */
-     
+
+/*drl added 12/19 */
+bool constraint_isConstantOnly (constraint p_c);
 /*@=czechfcns*/
 /* drl possible problem : warning take this out */
 

diff --git a/src/Headers/constraintExpr.h b/src/Headers/constraintExpr.h
index df65c150305fac2faa11f2e9c50f1640aa67a758..09f1c4381cb88ac2a84328b575fd32956ebfa280 100644 (file)
--- a/src/Headers/constraintExpr.h
+++ b/src/Headers/constraintExpr.h
@@ -128,7 +128,11 @@ int constraintExpr_getDepth (/*@observer@*/ /*@temp@*/ constraintExpr p_ex);
 /* drl added 12/30/001*/
 /* extern / *@only@* / constraintExpr constraintExpr_doSRefFixInvarConstraint (/ *@only@* / constraintExpr p_expr, sRef p_s, ctype p_ct); */
 
-   
+
+
+/*drl added 12/19 */
+bool  constraintExpr_isConstantOnly ( constraintExpr p_e );
+
 #else
 # error "Multiple include"
 #endif

diff --git a/src/Headers/constraintTerm.h b/src/Headers/constraintTerm.h
index 8ea90ee3dd731f9b4787020dd6f597f5bc4867b6..673de12e0b3f0c45d4dbcff32a6e04c87260b9f3 100644 (file)
--- a/src/Headers/constraintTerm.h
+++ b/src/Headers/constraintTerm.h
@@ -86,6 +86,9 @@ extern ctype constraintTerm_getCType (constraintTerm term);
 
 /*@=namechecks@*/
 
+/*drl added 12/19/2002*/
+bool  constraintTerm_isConstantOnly ( constraintTerm p_term );
+     
 #else
 
 #error Multiple Include

diff --git a/src/Makefile.am b/src/Makefile.am
index 4685875c3ff054505a1f6c21be317a95ed127f6a..b642546117b27edde69df6961e8113de65be9200 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -237,6 +237,8 @@ IFILES =  ctbase.i  cttable.i  exprDataQuite.i
 ## Non-built files we need to distribute
 EXTRA_DIST =  $(BISON_SRC) bison.head bison.reset $(HEADERSRC)  \
             flags.def cscanner.l flex.head flex.reset $(IFILES) \
+            .splintrc LICENSE \
+            Headers/cscannerHelp.h \
  Headers/256_random_numbers.nf  Headers/splintMacros.nf        Headers/reservedNames.nf
 #Makefile.binary.am   Makefile.binary.in
 

diff --git a/src/Makefile.in b/src/Makefile.in
index c7f03df49b4a5761b2e3621ab35b05e1c85e6b09..79ceee8fa63940e2fb9abd2ffd5e1bd28926fbb9 100644 (file)
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -332,6 +332,8 @@ IFILES = ctbase.i  cttable.i  exprDataQuite.i
 
 EXTRA_DIST = $(BISON_SRC) bison.head bison.reset $(HEADERSRC)  \
             flags.def cscanner.l flex.head flex.reset $(IFILES) \
+            .splintrc LICENSE \
+            Headers/cscannerHelp.h \
  Headers/256_random_numbers.nf  Headers/splintMacros.nf        Headers/reservedNames.nf
 
 #Makefile.binary.am   Makefile.binary.in

diff --git a/src/constraint.c b/src/constraint.c
index 71c3855093eade6be2c43f29475faf9a22e661a0..2410e1d410b232fdea474ffa59fd8e9d7214f4aa 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -724,6 +724,7 @@ void constraint_printError (constraint c, fileloc loc)
   cstring string;
   fileloc errorLoc, temp;
 
+  bool isLikely;
 
   /*drl 11/26/2001 avoid printing tautological constraints */
   if (constraint_isAlwaysTrue (c))
@@ -756,8 +757,30 @@ void constraint_printError (constraint c, fileloc loc)
       string = cstring_replaceChar(string, '\n', ' ');
     }
 
+  /*drl added 12/19/2002 print
+    a different error fro "likely" bounds-errors*/
+  
+  isLikely = constraint_isConstantOnly(c);
 
-  if (c->post)
+  if (isLikely)
+    {
+      if (c->post)
+       {
+         voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
+       }
+      else
+       {
+         if (constraint_hasMaxSet (c))
+           {
+             voptgenerror (FLG_LIKELYBOUNDSWRITE, string, errorLoc);
+           }
+         else
+           {
+             voptgenerror (FLG_LIKELYBOUNDSREAD, string, errorLoc);
+           }
+       }
+    }
+  else if (c->post)
     {
       voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
     }
@@ -844,6 +867,7 @@ cstring  constraint_printDetailed (constraint c)
   cstring st = cstring_undefined;
   cstring temp = cstring_undefined;
   cstring genExpr;
+  bool isLikely;
   
   if (!c->post)
     {
@@ -854,13 +878,30 @@ cstring  constraint_printDetailed (constraint c)
       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c));
     }
 
-  if (constraint_hasMaxSet (c))
+  isLikely = constraint_isConstantOnly(c);
+
+  if (isLikely)
     {
-      temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
+      if (constraint_hasMaxSet (c))
+       {
+         temp = cstring_makeLiteral ("Likely out-of-bounds store:\n");
+       }
+      else
+       {
+         temp = cstring_makeLiteral ("Likely out-of-bounds read:\n");
+       }
     }
   else
     {
-      temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
+      
+      if (constraint_hasMaxSet (c))
+       {
+         temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
+       }
+      else
+       {
+         temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
+       }
     }
   
   genExpr = exprNode_unparse (c->generatingExpr);
@@ -1216,3 +1257,25 @@ bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
   return FALSE;
   
 }
+
+/*drl added 12/19/2002*/
+/*whether constraints consist only of
+  terms which are constants*/
+bool constraint_isConstantOnly (constraint c)
+{
+  bool l, r;
+
+  l = constraintExpr_isConstantOnly(c->lexpr);
+  r = constraintExpr_isConstantOnly(c->expr);
+
+  if (l && r)
+    {
+      return TRUE;
+    }
+
+  else
+    {
+      return FALSE;
+    }
+  
+}

diff --git a/src/constraintExpr.c b/src/constraintExpr.c
index 3dcd6666fa180dc77eff323e943d91614f767077..b5c5de443ef4d0d00dd9ab97cb52ea7bde458de4 100644 (file)
--- a/src/constraintExpr.c
+++ b/src/constraintExpr.c
@@ -2500,3 +2500,68 @@ static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ c
   return e;
 }
 
+
+bool  constraintExpr_isConstantOnly ( constraintExpr e )
+{
+  DPRINTF(( (message("constraintExpr_isConstantOnly %s ",
+                    constraintExpr_unparse(e) ) )
+           ));
+
+  switch (e->kind)
+    {
+    case term:
+      {
+       constraintTerm t;
+       
+       t = constraintExprData_termGetTerm(e->data);
+       
+       
+       if (constraintTerm_isConstantOnly (t) )
+         {
+           return TRUE;
+         }
+       else
+         {
+           return FALSE;
+         }
+      }
+      
+    case binaryexpr:
+      {
+       constraintExpr temp1, temp2;
+       
+       temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
+       
+       temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
+       
+       if (constraintExpr_isConstantOnly(temp1) &&
+           constraintExpr_isConstantOnly(temp2) )
+         {
+           return TRUE;
+         }
+       else
+         {
+           return FALSE;
+         }
+      }
+      
+    case unaryExpr:
+      {
+       constraintExpr temp;
+       
+       temp = constraintExprData_unaryExprGetExpr (e->data );
+
+       if (constraintExpr_isConstantOnly(temp) )
+         {
+           return TRUE;
+         }
+       else
+         {
+           return FALSE;
+         }
+      }
+    default:
+      BADEXIT;
+    }
+}
+

diff --git a/src/constraintTerm.c b/src/constraintTerm.c
index e49f75d96143b42e94ff2493f4429a9924a4598a..234598a7ed5f880f16ac18cd53d379ca8841a332 100644 (file)
--- a/src/constraintTerm.c
+++ b/src/constraintTerm.c
@@ -736,3 +736,37 @@ ctype constraintTerm_getCType (constraintTerm term)
   return ct;
 }
 
+bool constraintTerm_isConstantOnly (constraintTerm term)
+{  
+  switch (term->kind)
+    {
+    case EXPRNODE:
+      if (exprNode_isNumLiteral (term->value.expr) ||
+         exprNode_isStringLiteral (term->value.expr) ||
+         exprNode_isCharLiteral  (term->value.expr) )
+       {
+         return TRUE;
+       }
+      else
+       {
+         return FALSE;
+       }
+
+    case INTLITERAL:
+      return TRUE;
+            
+    case SREF:
+      if ( sRef_isConst (term->value.sref) )
+       {
+         return TRUE;
+       }
+      else
+       {
+         return FALSE;
+       }
+    default:
+      BADEXIT;
+    }
+  
+  BADEXIT;
+}

diff --git a/src/context.c b/src/context.c
index 053a86e1ba60b10de7dab5e7b9ac1f05a50ca650..7c91bfac0f1511fb20a0dcc2a560fd4401b89e0d 100644 (file)
--- a/src/context.c
+++ b/src/context.c
@@ -4140,11 +4140,24 @@ context_setFlagAux (flagcode f, bool b, bool inFile,
       DOSET (FLG_ALLMACROS, b);
       DOSET (FLG_FCNMACROS, b);
       DOSET (FLG_CONSTMACROS, b);
-      break;
+      break;      
     case FLG_BOUNDS:
       DOSET (FLG_BOUNDSREAD, b);
       DOSET (FLG_BOUNDSWRITE, b);
+      DOSET (FLG_LIKELYBOUNDSREAD, b);
+      DOSET (FLG_LIKELYBOUNDSWRITE, b);
+      break;
+    case FLG_BOUNDSREAD:
+      DOSET (FLG_LIKELYBOUNDSREAD, b);
+      break;
+    case FLG_BOUNDSWRITE:
+      DOSET (FLG_LIKELYBOUNDSWRITE, b);
       break;
+    case FLG_LIKELYBOUNDS:
+      DOSET (FLG_LIKELYBOUNDSREAD, b);
+      DOSET (FLG_LIKELYBOUNDSWRITE, b);
+      break;
+      
     case FLG_CZECH:
       if (b) { DOSET (FLG_ACCESSCZECH, b); }
       DOSET (FLG_CZECHFUNCTIONS, b);

diff --git a/src/exprChecks.c b/src/exprChecks.c
index 4b3b81db593fbb0c26172eaef5f59be0a014b157..54fce3ce319f3cca8f9eb7fe0e4bda20e8b795ed 100644 (file)
--- a/src/exprChecks.c
+++ b/src/exprChecks.c
@@ -960,8 +960,10 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
       /* check if errors will printed */
       if (!(context_getFlag(FLG_DEBUGFUNCTIONCONSTRAINT) ||
            context_getFlag(FLG_BOUNDSWRITE) ||
-           context_getFlag(FLG_BOUNDSREAD) ||
-           context_getFlag(FLG_CHECKPOST)))
+           context_getFlag(FLG_BOUNDSREAD)  ||
+           context_getFlag(FLG_LIKELYBOUNDSWRITE) ||
+           context_getFlag(FLG_LIKELYBOUNDSREAD)  ||
+           context_getFlag(FLG_CHECKPOST) ))
        {
          exprNode_free (body);
          context_exitInnerPlain();

diff --git a/src/flags.def b/src/flags.def
index afc3cff08ea93a2a92223f1bf91d071c960056a7..6c0d6361c5e1edee3d4a2933b67129b78b500933 100644 (file)
--- a/src/flags.def
+++ b/src/flags.def
@@ -1885,6 +1885,30 @@ static flaglist flags =
     "memory bounds checking (sets boundsread and boundswrite)",
     "Memory read or write may be out of bounds of allocated storage.", 0, 0
   },
+  {
+    FK_BOUNDS, FK_MEMORY, specialFlag,
+    "likelybounds",
+    FLG_LIKELYBOUNDS,
+    "memory bounds checking (sets likelyboundsread and likelyboundswrite)",
+    "Memory read or write may be out of bounds of allocated storage.", 0, 0
+  },
+  {
+    FK_BOUNDS, FK_MEMORY, plainFlag,
+    "likely-boundsread",
+    FLG_LIKELYBOUNDSREAD,
+    "likely out of bounds read",
+    "A memory read references memory beyond the allocated storage.",
+    0, 0
+  },
+  {
+    FK_BOUNDS, FK_MEMORY, plainFlag,
+    "likely-boundswrite",
+    FLG_LIKELYBOUNDSWRITE,
+    "likely buffer overflow from an out of bounds write",
+    "A memory write may write to an address beyond the allocated buffer.",
+    0, 0
+  },
+  
   {
     FK_BOUNDS, FK_MEMORY, plainFlag,
     "boundsread",

diff --git a/test/constannot.expect b/test/constannot.expect
index 6cb0756339a74f3cce8ea1dad755371f04af1289..467493b7469c9c0fe56b3876208c8106aced27d6 100644 (file)
--- a/test/constannot.expect
+++ b/test/constannot.expect
@@ -7,7 +7,7 @@ constannot.c:11:3: Possible out-of-bounds store:
      needed to satisfy precondition:
     requires maxSet(str @ constannot.c:11:3) >= 20
 constannot.c: (in function foo3)
-constannot.c:20:3: Possible out-of-bounds store:
+constannot.c:20:3: Likely out-of-bounds store:
     foo(buf)
     Unable to resolve constraint:
     requires <const int=20> <= 19

diff --git a/test/manual.expect b/test/manual.expect
index e5471d8e293e293f15c2beeef0ea4f7ca5460532..e975c0069d5a0c0efae21a8874666cf465665db8 100644 (file)
--- a/test/manual.expect
+++ b/test/manual.expect
@@ -202,7 +202,7 @@ ignore.c:10: Return value (type bool) ignored: fb()
 
 Finished checking --- 1 code warning, as expected
 
-setChar.c:5: Possible out-of-bounds store:
+setChar.c:5: Likely out-of-bounds store:
     buf[10]
     Unable to resolve constraint:
     requires 9 >= 10

diff --git a/test/simplebufferConstraintTests.expect b/test/simplebufferConstraintTests.expect
index e5e79d450575f9ba9fe39271585c0a2886f52b7f..3db1c55e0eb5102e18e9a3d1951ab333952e23b6 100644 (file)
--- a/test/simplebufferConstraintTests.expect
+++ b/test/simplebufferConstraintTests.expect
@@ -3,7 +3,7 @@ m.c: (in function t)
 m.c:9:1: Index of possibly null pointer f: f
    m.c:8:5: Storage f may become null
 sizeof.c: (in function f)
-sizeof.c:17:1: Possible out-of-bounds store:
+sizeof.c:17:1: Likely out-of-bounds store:
     x[(sizeof(x))]
     Unable to resolve constraint:
     requires 2 >= 3
@@ -12,7 +12,7 @@ sizeof.c:17:1: Possible out-of-bounds store:
 test3.c:2:6: Function t defined more than once
    m.c:11:1: Previous definition of t
 test3.c: (in function t)
-test3.c:9:3: Possible out-of-bounds store:
+test3.c:9:3: Likely out-of-bounds store:
     g[101]
     Unable to resolve constraint:
     requires 99 >= 101

diff --git a/test/sizeoftest.expect b/test/sizeoftest.expect
index 7f183efb899207e542473cea20a49f9ff1cd274b..8bbef3c0ceca077f97994a1d451d9c0c97774ece 100644 (file)
--- a/test/sizeoftest.expect
+++ b/test/sizeoftest.expect
@@ -1,6 +1,6 @@
 
 sizeof.c: (in function main)
-sizeof.c:6:2: Possible out-of-bounds store:
+sizeof.c:6:2: Likely out-of-bounds store:
     x[(sizeof(x))]
     Unable to resolve constraint:
     requires 2 >= 3