From 2681ee3970a86d505558ee5def1bfcd16c3c397c Mon Sep 17 00:00:00 2001 From: drl7x Date: Thu, 5 Jul 2001 21:31:36 +0000 Subject: [PATCH] Added basic support for switch statements Also added support the simplifications rules like: x < y => x - 2 < y This is useful for resolving constraints. --- src/Headers/herald.h | 2 +- src/Headers/herald.last | 2 +- src/Headers/local_constants.h | 4 +- src/Headers/local_constants.last | 4 +- src/constraintGeneration.c | 65 ++++++++--- src/constraintResolve.c | 180 +++++++++++++++++-------------- 6 files changed, 153 insertions(+), 104 deletions(-) diff --git a/src/Headers/herald.h b/src/Headers/herald.h index b0c1a78..5920a7a 100644 --- 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 b0c1a78..5920a7a 100644 --- 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 c4c3a88..73e13fc 100644 --- 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 c4c3a88..73e13fc 100644 --- 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 11f978e..ae34b89 100644 --- 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 199a882..38979ad 100644 --- 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") ); -- 2.45.2