Added basic support for switch statements

Also added support the simplifications rules like:
 x < y => x - 2 < y
This is useful for resolving constraints.

diff --git a/src/Headers/herald.h b/src/Headers/herald.h
index b0c1a785d1daa9bd3d23635602020ef1cb2a028d..5920a7a25e23cbd36eeb63499b9d4b800880dabb 100644 (file)
--- a/src/Headers/herald.h
+++ b/src/Headers/herald.h
@@ -4,4 +4,4 @@
 /*@constant observer char *LCL_PARSE_VERSION;@*/
 # define LCL_PARSE_VERSION "LCLint 3.0b-alpha"
 /*@constant observer char *LCL_COMPILE;@*/
-# define LCL_COMPILE "Compiled using gcc -Wall -g on Linux paisley 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by evans"
+# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on Linux fowler 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by drl7x"

diff --git a/src/Headers/herald.last b/src/Headers/herald.last
index b0c1a785d1daa9bd3d23635602020ef1cb2a028d..5920a7a25e23cbd36eeb63499b9d4b800880dabb 100644 (file)
--- a/src/Headers/herald.last
+++ b/src/Headers/herald.last
@@ -4,4 +4,4 @@
 /*@constant observer char *LCL_PARSE_VERSION;@*/
 # define LCL_PARSE_VERSION "LCLint 3.0b-alpha"
 /*@constant observer char *LCL_COMPILE;@*/
-# define LCL_COMPILE "Compiled using gcc -Wall -g on Linux paisley 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by evans"
+# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on Linux fowler 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by drl7x"

diff --git a/src/Headers/local_constants.h b/src/Headers/local_constants.h
index c4c3a887ac645344e32355e5979556d4d408aa9a..73e13fc02ff2ff0ec28919e4f5adc9cc5c4dac80 100644 (file)
--- a/src/Headers/local_constants.h
+++ b/src/Headers/local_constants.h
@@ -2,6 +2,6 @@
 /*@constant observer char *SYSTEM_LIBDIR;@*/
 # define SYSTEM_LIBDIR "/usr/include"
 /*@constant observer char *DEFAULT_LARCHPATH;@*/
-# define DEFAULT_LARCHPATH "/usr/local/lclint-2.5m/lib"
+# define DEFAULT_LARCHPATH ".:/af9/drl7x/re3/LCLintDev/lib"
 /*@constant observer char *DEFAULT_LCLIMPORTDIR;@*/
-# define DEFAULT_LCLIMPORTDIR "/usr/local/lclint-2.5m/imports"
+# define DEFAULT_LCLIMPORTDIR "/af9/drl7x/re3/LCLintDev/imports"

diff --git a/src/Headers/local_constants.last b/src/Headers/local_constants.last
index c4c3a887ac645344e32355e5979556d4d408aa9a..73e13fc02ff2ff0ec28919e4f5adc9cc5c4dac80 100644 (file)
--- a/src/Headers/local_constants.last
+++ b/src/Headers/local_constants.last
@@ -2,6 +2,6 @@
 /*@constant observer char *SYSTEM_LIBDIR;@*/
 # define SYSTEM_LIBDIR "/usr/include"
 /*@constant observer char *DEFAULT_LARCHPATH;@*/
-# define DEFAULT_LARCHPATH "/usr/local/lclint-2.5m/lib"
+# define DEFAULT_LARCHPATH ".:/af9/drl7x/re3/LCLintDev/lib"
 /*@constant observer char *DEFAULT_LCLIMPORTDIR;@*/
-# define DEFAULT_LCLIMPORTDIR "/usr/local/lclint-2.5m/imports"
+# define DEFAULT_LCLIMPORTDIR "/af9/drl7x/re3/LCLintDev/imports"

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index 11f978e1d8d4387aa31a0145b717d85324d7039a..ae34b89d9096b4dbab3231a9d48d5df2ba5e310b 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -74,7 +74,7 @@ static bool exprNode_isUnhandled (/*@dependent@*/ /*@obsever@*/ exprNode e)
     case XPR_TOK:
     case XPR_FTDEFAULT:
     case XPR_DEFAULT:
-    case XPR_SWITCH:
+      //    case XPR_SWITCH:
     case XPR_FTCASE:
     case XPR_CASE:
       //    case XPR_INIT:
@@ -180,6 +180,7 @@ if (exprNode_handleError (e) != NULL)
     case XPR_BLOCK:
     case XPR_STMT:
     case XPR_STMTLIST:
+    case XPR_SWITCH:
       return TRUE;
     default:
       return FALSE;
@@ -571,17 +572,23 @@ static exprNode doSwitch (/*@returned@*/ exprNode e)
   exprData data;
 
   data = e->edata;
-  llassert(FALSE);
-  //DPRINTF (( message ("doSwitch for: switch (%s) %s", 
-  //        exprNode_unparse (exprData_getPairA (data)),
-  //                exprNode_unparse (exprData_getPairB (data))) ));
-
+  //  llassert(FALSE);
+  DPRINTF (( message ("doSwitch for: switch (%s) %s", 
+                     exprNode_unparse (exprData_getPairA (data)),
+                     exprNode_unparse (exprData_getPairB (data))) ));
+  
   body = exprData_getPairB (data);
   
-  // exprNode_generateConstraints(body);
+  exprNode_generateConstraints(body);
   
-  // e->requiresConstraints = constraintList_copy ( body->requiresConstraints );
-  //e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints );
+  constraintList_free(e->requiresConstraints);
+  constraintList_free(e->ensuresConstraints);
+  
+  e->requiresConstraints = NULL;
+  e->ensuresConstraints  = NULL;
+
+  e->requiresConstraints = constraintList_copy ( body->requiresConstraints );
+  e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints );
   
   return e;
 }
@@ -1353,14 +1360,14 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
   exprData data;
   constraintList ret;
 
-   if (exprNode_handleError (e))
-     {
-       ret = constraintList_makeNew();
-       return ret;
-     }
+  if (exprNode_handleError (e))
+    {
+      ret = constraintList_makeNew();
+      return ret;
+    }
   ret = constraintList_copy (e->trueEnsuresConstraints );
    
-   handledExprNode = TRUE;
+  handledExprNode = TRUE;
    
   data = e->edata;
   
@@ -1392,6 +1399,14 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
       ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
                                    (exprData_getUopNode (data) ) );
       break;
+
+    case XPR_INIT:
+      ret = constraintList_addListFree (ret,
+                                       exprNode_traversTrueEnsuresConstraints
+                                       (exprData_getInitNode (data) ) );
+       break;
+
+
     case XPR_ASSIGN:
         ret = constraintList_addListFree (ret,
                                    exprNode_traversTrueEnsuresConstraints
@@ -1530,6 +1545,12 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
       ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
                                    (exprData_getUopNode (data) ) );
       break;
+    case XPR_INIT:
+        ret = constraintList_addListFree (ret,
+                                   exprNode_traversFalseEnsuresConstraints
+                                   (   exprData_getInitNode (data) ) );
+       break;
+
     case XPR_ASSIGN:
         ret = constraintList_addListFree (ret,
                                    exprNode_traversFalseEnsuresConstraints
@@ -1670,6 +1691,12 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
       ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
                                    (exprData_getUopNode (data) ) );
       break;
+    case XPR_INIT:
+      ret = constraintList_addListFree (ret,
+                                       exprNode_traversRequiresConstraints
+                                       (exprData_getInitNode (data) ) );
+       break;
+
     case XPR_ASSIGN:
         ret = constraintList_addListFree (ret,
                                    exprNode_traversRequiresConstraints
@@ -1821,6 +1848,14 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
       ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
                                    (exprData_getUopNode (data) ) );
       break;
+      
+    case XPR_INIT:
+      ret = constraintList_addListFree (ret,
+                                       exprNode_traversEnsuresConstraints
+                                       (exprData_getInitNode (data) ) );
+       break;
+
+
     case XPR_ASSIGN:
         ret = constraintList_addListFree (ret,
                                    exprNode_traversEnsuresConstraints

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index 199a882e4fd538e4ef91c00dcd1c78c49bd99d1e..38979ad7f432a654a2406607dfc85b66063e4614 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -736,95 +736,109 @@ static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arit
   switch (ar1)
  {
  case GTE:
-      if (constraintExpr_similar (expr1, expr2) )
-        return TRUE;
-      /*@fallthrough@*/
- case GT:
-   if (!  (constraintExpr_canGetValue (expr1) &&
-          constraintExpr_canGetValue (expr2) ) )
-     {
-       constraintExpr e1, e2;
-       bool p1, p2;
-       int const1, const2;
-       
-       e1 = constraintExpr_copy(expr1);
-       e2 = constraintExpr_copy(expr2);
-
-       e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
-
-       e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
-
-       if (p1 && p2)
-        if (const1 <= const2)
-          if (constraintExpr_similar (e1, e2) )
-            {
-              constraintExpr_free(e1);
-              constraintExpr_free(e2);
-              return TRUE;
-            }
-       
-       DPRINTF( ("Can't Get value"));
-       
-       constraintExpr_free(e1);
-       constraintExpr_free(e2);
-       return FALSE;
-     }
-   
-   if (constraintExpr_compare (expr2, expr1) >= 0)
-     return TRUE;
-  
-  return FALSE;
- case EQ:
-   if (constraintExpr_similar (expr1, expr2) )
-        return TRUE;
-   
-   return FALSE;
- case LTE:
-   if (constraintExpr_similar (expr1, expr2) )
-        return TRUE;
-   /*@fallthrough@*/
- case LT:
+       if (constraintExpr_similar (expr1, expr2) )
+         return TRUE;
+       /*@fallthrough@*/
+  case GT:
     if (!  (constraintExpr_canGetValue (expr1) &&
-          constraintExpr_canGetValue (expr2) ) )
-     {
-      constraintExpr e1, e2;
-       bool p1, p2;
-       int const1, const2;
-       
-       e1 = constraintExpr_copy(expr1);
-       e2 = constraintExpr_copy(expr2);
-
-       e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
-
-       e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
-
-       if (p1 && p2)
-        if (const1 >= const2)
-          if (constraintExpr_similar (e1, e2) )
-            {
-              constraintExpr_free(e1);
-              constraintExpr_free(e2);
-              return TRUE;
-            }
-       constraintExpr_free(e1);
-       constraintExpr_free(e2);
-       
-       DPRINTF( ("Can't Get value"));
-       return FALSE;
-     }
-   
-   if (constraintExpr_compare (expr2, expr1) <= 0)
-     return TRUE;
+              constraintExpr_canGetValue (expr2) ) )
+           {
+                 constraintExpr e1, e2;
+                 bool p1, p2;
+                 int const1, const2;
+
+                 e1 = constraintExpr_copy(expr1);
+                 e2 = constraintExpr_copy(expr2);
+
+                 e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
+
+                 e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
+
+                 if (p1 || p2)
+                    {
+                     if (!p1)
+                          const1 = 0;
+
+                     if (!p2)
+                          const2 = 0;
+
+                     if (const1 <= const2)
+                          if (constraintExpr_similar (e1, e2) )
+                                 {
+                                        constraintExpr_free(e1);
+                                        constraintExpr_free(e2);
+                                        return TRUE;
+                                      }
+                     }
+                 DPRINTF( ("Can't Get value"));
+
+                 constraintExpr_free(e1);
+                 constraintExpr_free(e2);
+                 return FALSE;
+               }
+
+    if (constraintExpr_compare (expr2, expr1) >= 0)
+           return TRUE;
 
    return FALSE;
-   
- default:
-     llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1) ) ) );
- }
+  case EQ:
+    if (constraintExpr_similar (expr1, expr2) )
+       return TRUE;
+
+    return FALSE;
+  case LTE:
+    if (constraintExpr_similar (expr1, expr2) )
+       return TRUE;
+    /*@fallthrough@*/
+  case LT:
+     if (!  (constraintExpr_canGetValue (expr1) &&
+               constraintExpr_canGetValue (expr2) ) )
+            {
+                 constraintExpr e1, e2;
+                  bool p1, p2;
+                  int const1, const2;
+
+                  e1 = constraintExpr_copy(expr1);
+                  e2 = constraintExpr_copy(expr2);
+
+                  e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
+
+                  e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
+
+                  if (p1 || p2)
+                     {
+                      if (!p1)
+                           const1 = 0;
+
+                      if (!p2)
+                           const2 = 0;
+
+                      if (const1 >= const2)
+                           if (constraintExpr_similar (e1, e2) )
+                                  {
+                                         constraintExpr_free(e1);
+                                         constraintExpr_free(e2);
+                                         return TRUE;
+                                       }
+                      }
+                  constraintExpr_free(e1);
+                  constraintExpr_free(e2);
+
+                  DPRINTF( ("Can't Get value"));
+                  return FALSE;
+                }
+
+    if (constraintExpr_compare (expr2, expr1) <= 0)
+           return TRUE;
+
+    return FALSE;
+
+  default:
+      llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1) ) ) );
+  }
   BADEXIT;
 }
 
-
 static constraint constraint_searchandreplace (/*@returned@*/ constraint c, constraintExpr old, constraintExpr newExpr)
 {
   DPRINTF (("Doing replace for lexpr") );