From 34f0c5e711b8f61f6376414948f4c116f1c5a22c Mon Sep 17 00:00:00 2001 From: drl7x Date: Wed, 29 Nov 2000 05:01:50 +0000 Subject: [PATCH] We're now able to generate Maxset constraints for fixed sized arrays. e.g. int x[3]; produces maxset(x) >= 2; --- src/Headers/constraint.h | 9 ++ src/Headers/herald.h | 2 +- src/Headers/herald.last | 2 +- src/Headers/lltok.h | 13 +++ src/Headers/sRef.h | 9 +- src/Makefile.sources | 1 + src/cgrammar.tab.c | 8 +- src/cgrammar.y | 8 +- src/constraint.c | 56 ++++++++-- src/constraintGeneration.c | 212 +++++++++++++++++++++++++++++++------ src/constraintResolve.c | 70 +++++++++++- src/ctype.c | 19 ++++ src/exprChecks.c | 13 ++- src/lltok.c | 24 +++++ src/sRef.c | 20 ++++ 15 files changed, 405 insertions(+), 61 deletions(-) diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index d8e1b50..e8436fa 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -86,6 +86,15 @@ constraint constraint_doSRefFixBaseParam (constraint precondition, cstring constraint_printDetailed (constraint c); +constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint); + +constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); +constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint); +constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); + +/*drl add 11/28/2000 */ +constraint constraint_makeSRefWriteSafeInt (sRef s, int ind); + /*@=czechfcns*/ #warning take this out #include "constraintList.h" diff --git a/src/Headers/herald.h b/src/Headers/herald.h index a19b946..05019e4 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 2.5q" /*@constant observer char *LCL_COMPILE;@*/ -# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on SunOS cobra.cs.Virginia.EDU 5.6 Generic_105181-13 sun4u sparc SUNW,Ultra-60 by drl7x" +# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 on SunOS mamba.cs.Virginia.EDU 5.6 Generic_105181-09 sun4u sparc SUNW,Ultra-60 by drl7x" diff --git a/src/Headers/herald.last b/src/Headers/herald.last index a19b946..424bb62 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 2.5q" /*@constant observer char *LCL_COMPILE;@*/ -# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on SunOS cobra.cs.Virginia.EDU 5.6 Generic_105181-13 sun4u sparc SUNW,Ultra-60 by drl7x" +# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on SunOS mamba.cs.Virginia.EDU 5.6 Generic_105181-09 sun4u sparc SUNW,Ultra-60 by drl7x" diff --git a/src/Headers/lltok.h b/src/Headers/lltok.h index 4cace03..317704a 100644 --- a/src/Headers/lltok.h +++ b/src/Headers/lltok.h @@ -43,6 +43,19 @@ extern bool lltok_isOr_Op (lltok tok); extern bool lltok_isNot_Op (lltok tok); +/*drl7x added this function 11/20/00 */ + +bool lltok_isLt_Op (lltok tok); + +bool lltok_isGt_Op (lltok tok); + +bool lltok_isGe_Op (lltok tok); + +bool lltok_isLe_Op (lltok tok); + +/* end drl7x added */ + + # else # error "Multiple include" # endif diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h index 448cfc8..94ae544 100644 --- a/src/Headers/sRef.h +++ b/src/Headers/sRef.h @@ -613,14 +613,19 @@ extern bool sRef_isNullTerminated(sRef p_s); extern bool sRef_isPossiblyNullTerminated(sRef p_s); # define sRef_isPossiblyNullTerminated(p_s) \ - ( sRef_hasBufStateInfo(p_s) ? (p_s->bufinfo.bufstate \ + ( sRef_hasBufStateInfo((p_s)) ? ( (p_s)->bufinfo.bufstate \ == BB_POSSIBLYNULLTERMINATED) : FALSE) extern bool sRef_isNotNullTerminated(sRef p_s); # define sRef_isNotNullTerminated(p_s) \ ( sRef_hasBufStateInfo(p_s) ? (p_s->bufinfo.bufstate \ == BB_NOTNULLTERMINATED) : FALSE) - + + /*drl7x 11/28/00*/ +extern bool sRef_isFixedArray (sRef p_s); + +extern int sRef_getArraySize (sRef p_s); + extern /*@observer@*/ cstring sRef_ntMessage (sRef p_s); /* end modifications */ diff --git a/src/Makefile.sources b/src/Makefile.sources index a936d99..e365890 100644 --- a/src/Makefile.sources +++ b/src/Makefile.sources @@ -30,6 +30,7 @@ GENERALSRC = cstring.c fileloc.c message.c source.c \ constraintExpr.c \ constraintExprData.c \ constraintResolve.c \ + constraintOutput.c \ environmentTable.c \ constraintList.c \ constraintGeneration.c \ diff --git a/src/cgrammar.tab.c b/src/cgrammar.tab.c index 137c76f..1ef0039 100644 --- a/src/cgrammar.tab.c +++ b/src/cgrammar.tab.c @@ -3169,7 +3169,7 @@ case 27: yyval.ntyp = idDecl_replaceCtype (yyvsp[-7].ntyp, ctype_makeFunction (idDecl_getCtype (yyvsp[-7].ntyp), yyvsp[-4].entrylist)); context_popLoc (); - printf("Done nameDeclBase\n"); + // printf("Done nameDeclBase\n"); ; break;} case 28: @@ -3280,7 +3280,7 @@ case 47: case 49: #line 407 "cgrammar.y" { - TPRINTF ( ("doing optGlobBufConstraintsAux\n") ); + DPRINTF ( ("doing optGlobBufConstraintsAux\n") ); context_setProtectVars (); enterParamsTemp (); sRef_setGlobalScopeSafe (); @@ -3311,12 +3311,12 @@ case 54: break;} case 61: #line 441 "cgrammar.y" -{yyval.sr = constraintExpr_parseMakeUnaryOp (yyvsp[-3].tok, yyvsp[-1].sr); TPRINTF( ("Got BufConstraintExpr UNary Op ") ); ; +{yyval.sr = constraintExpr_parseMakeUnaryOp (yyvsp[-3].tok, yyvsp[-1].sr); DPRINTF( ("Got BufConstraintExpr UNary Op ") ); ; break;} case 62: #line 442 "cgrammar.y" { - TPRINTF( ("Got BufConstraintExpr BINary Op ") ); + DPRINTF( ("Got BufConstraintExpr BINary Op ") ); yyval.sr = constraintExpr_parseMakeBinaryOp (yyvsp[-3].sr, yyvsp[-2].tok, yyvsp[-1].sr); ; break;} case 63: diff --git a/src/cgrammar.y b/src/cgrammar.y index ba88dae..3cfd7b1 100644 --- a/src/cgrammar.y +++ b/src/cgrammar.y @@ -328,7 +328,7 @@ namedDeclBase $$ = idDecl_replaceCtype ($1, ctype_makeFunction (idDecl_getCtype ($1), $4)); context_popLoc (); - printf("Done nameDeclBase\n"); + // printf("Done nameDeclBase\n"); } plainNamedDeclBase @@ -405,7 +405,7 @@ optGlobBufConstraintsRest optGlobBufConstraintsAux : { - TPRINTF ( ("doing optGlobBufConstraintsAux\n") ); + DPRINTF ( ("doing optGlobBufConstraintsAux\n") ); context_setProtectVars (); enterParamsTemp (); sRef_setGlobalScopeSafe (); @@ -438,9 +438,9 @@ relationalOp BufConstraintExpr : BufConstraintTerm - | BufUnaryOp TLPAREN BufConstraintExpr TRPAREN {$$ = constraintExpr_parseMakeUnaryOp ($1, $3); TPRINTF( ("Got BufConstraintExpr UNary Op ") ); } + | BufUnaryOp TLPAREN BufConstraintExpr TRPAREN {$$ = constraintExpr_parseMakeUnaryOp ($1, $3); DPRINTF( ("Got BufConstraintExpr UNary Op ") ); } | TLPAREN BufConstraintExpr BufBinaryOp BufConstraintExpr TRPAREN { - TPRINTF( ("Got BufConstraintExpr BINary Op ") ); + DPRINTF( ("Got BufConstraintExpr BINary Op ") ); $$ = constraintExpr_parseMakeBinaryOp ($2, $3, $4); } BufConstraintTerm diff --git a/src/constraint.c b/src/constraint.c index bcf358a..6c3b069 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -203,7 +203,21 @@ constraint constraint_makeWriteSafeInt (exprNode po, int ind) ret->expr = constraintExpr_makeValueInt (ind); /*@i1*/return ret; } - + + +constraint constraint_makeSRefWriteSafeInt (sRef s, int ind) +{ + constraint ret = constraint_makeNew(); + + + ret->lexpr = constraintExpr_makeSRefMaxset (s); + ret->ar = GTE; + ret->expr = constraintExpr_makeValueInt (ind); + ret->post = TRUE; + /*@i1*/return ret; +} + + constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) { constraint ret = constraint_makeNew(); @@ -214,7 +228,8 @@ constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) ret->expr = constraintExpr_makeValueExpr (ind); /*@i1*/return ret; } - + + constraint constraint_makeReadSafeInt ( exprNode po, int ind) { constraint ret = constraint_makeNew(); @@ -246,27 +261,52 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, filelo } -/* make constraint ensures e1 == e2 */ - -constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar) { constraint ret = constraint_makeNew(); exprNode e; e = exprNode_fakeCopy(e1); ret->lexpr = constraintExpr_makeValueExpr (e); - ret->ar = EQ; + ret->ar = ar; ret->post = TRUE; e = exprNode_fakeCopy(e2); ret->expr = constraintExpr_makeValueExpr (e); ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); -// fileloc_incColumn ( ret->lexpr->term->loc); -// fileloc_incColumn ( ret->lexpr->term->loc); return ret; } +/* make constraint ensures e1 == e2 */ + +constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) ); +} + +/*make constraint ensures e1 < e2 */ +constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) ); +} + +constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) ); +} + +constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) ); +} + +constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) ); +} + + exprNode exprNode_copyConstraints (exprNode dst, exprNode src) { dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints ); diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 1feaaf1..2d4d649 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -14,8 +14,9 @@ # include "exprNodeSList.h" # include "exprData.i" +# include "exprDataQuite.i" -void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e); +bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e); static bool exprNode_handleError( exprNode p_e); //static cstring exprNode_findConstraints ( exprNode p_e); @@ -31,9 +32,10 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e); extern constraintList reflectChanges (constraintList pre2, constraintList post1); void mergeResolve (exprNode parent, exprNode child1, exprNode child2); +exprNode makeDataTypeConstraints (exprNode e); +constraintList constraintList_makeFixedArrayConstraints (sRefSet s); +constraintList checkCall (exprNode fcn, exprNodeList arglist); - - bool exprNode_isUnhandled (exprNode e) { llassert( exprNode_isDefined(e) ); @@ -93,7 +95,7 @@ bool exprNode_handleError( exprNode e) return FALSE; } -void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) +bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) { if (exprNode_isError (e) ) return FALSE; @@ -109,7 +111,8 @@ void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) return FALSE; } - + + // e = makeDataTypeConstraints (e); DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e), fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); @@ -123,6 +126,17 @@ void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) // llassert(FALSE); return FALSE; } + + { + constraintList c; + + c = constraintList_makeFixedArrayConstraints (e->uses); + e->requiresConstraints = reflectChanges (e->requiresConstraints, c); + + // e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints); + + } + /* printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) ); printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); */ return FALSE; @@ -167,6 +181,7 @@ bool exprNode_stmt (exprNode e) } e->requiresConstraints = constraintList_new(); e->ensuresConstraints = constraintList_new(); + // e = makeDataTypeConstraints(e); DPRINTF(( "STMT:") ); @@ -222,6 +237,7 @@ bool exprNode_stmtList (exprNode e) e->requiresConstraints = constraintList_new(); e->ensuresConstraints = constraintList_new(); + // e = makeDataTypeConstraints(e); /*Handle case of stmtList with only one statement: The parse tree stores this as stmt instead of stmtList*/ @@ -263,6 +279,68 @@ exprNode doIf (exprNode e, exprNode test, exprNode body) return e; } +constraintList constraintList_makeFixedArrayConstraints (sRefSet s) +{ + constraintList ret; + ret = constraintList_new(); + + sRefSet_elements (s, el) + { + llassert (el); + if (sRef_isFixedArray(el) ) + { + int s; + constraint con; + s = sRef_getArraySize(el); + DPRINTF( (message("%s is a fixed array with size %d", + sRef_unparse(el), s) ) ); + con = constraint_makeSRefWriteSafeInt (el, (s - 1)); + ret = constraintList_add(ret, con); + } + else + { + DPRINTF( (message("%s is not a fixed array", + sRef_unparse(el)) ) ); + } + } + end_sRefSet_elements + + return ret; +} + +exprNode makeDataTypeConstraints (exprNode e) +{ + constraintList c; + DPRINTF(("makeDataTypeConstraints")); + + c = constraintList_makeFixedArrayConstraints (e->uses); + + e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c); + +/* sRefSet_elements (e->uses, el) */ +/* llassert (el); */ +/* if (sRef_isFixedArray(el) ) */ +/* { */ +/* int s; */ +/* constraint con; */ +/* s = sRef_getArraySize(el); */ +/* DPRINTF( (message("%s is a fixed array with size %d", */ +/* sRef_unparse(el), s) ) ); */ +/* con = constraint_makeSRefWriteSafeInt (el, (s - 1)); */ +/* e->ensuresConstraints = constraintList_add(e->ensuresConstraints, */ +/* con); */ +/* } */ +/* else */ +/* { */ +/* DPRINTF( (message("%s is not a fixed array", */ +/* sRef_unparse(el)) ) ); */ +/* } */ +/* end_sRefSet_elements */ + + return e; +} + + bool exprNode_multiStatement (exprNode e) { @@ -278,7 +356,8 @@ bool exprNode_multiStatement (exprNode e) e->ensuresConstraints = constraintList_new(); e->trueEnsuresConstraints = constraintList_new(); e->falseEnsuresConstraints = constraintList_new(); - + + // e = makeDataTypeConstraints(e); DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e), fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); @@ -453,6 +532,25 @@ bool lltok_isBoolean_Op (lltok tok) return TRUE; } + if (lltok_isGt_Op (tok) ) + { + return TRUE; + } + if (lltok_isLt_Op (tok) ) + { + return TRUE; + } + + if (lltok_isLe_Op (tok) ) + { + return TRUE; + } + + if (lltok_isGe_Op (tok) ) + { + return TRUE; + } + return FALSE; } @@ -460,41 +558,87 @@ bool lltok_isBoolean_Op (lltok tok) void exprNode_booleanTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint) { - constraint cons; - exprNode t1, t2; - exprData data; - lltok tok; - constraintList tempList; - data = e->edata; + constraint cons; +exprNode t1, t2; +exprData data; +lltok tok; +constraintList tempList; +data = e->edata; + +tok = exprData_getOpTok (data); + + +t1 = exprData_getOpA (data); +t2 = exprData_getOpB (data); - tok = exprData_getOpTok (data); +/* arithmetic tests */ + +if (lltok_isEq_Op (tok) ) +{ + cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); +} + + + if (lltok_isLt_Op (tok) ) + { + cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); + e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); + } + + +if (lltok_isGe_Op (tok) ) +{ - t1 = exprData_getOpA (data); - t2 = exprData_getOpB (data); + cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); - if (lltok_isEq_Op (tok) ) - { - cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); - e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); - } + cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); + e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); - if (lltok_isAnd_Op (tok) ) +} - { - //true ensures - tempList = constraintList_copy (t1->trueEnsuresConstraints); - tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); - e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList); - + + if (lltok_isGt_Op (tok) ) +{ + cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); + e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); +} + +if (lltok_isLe_Op (tok) ) +{ + cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + + cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); + e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); +} + + + +/*Logical operations */ + + if (lltok_isAnd_Op (tok) ) + + { + //true ensures + tempList = constraintList_copy (t1->trueEnsuresConstraints); + tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); + e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList); + //false ensures: fens t1 or tens t1 and fens t2 - tempList = constraintList_copy (t1->trueEnsuresConstraints); - tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); - tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints); + tempList = constraintList_copy (t1->trueEnsuresConstraints); + tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); + tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints); e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList); - } - + } + if (lltok_isOr_Op (tok) ) { //false ensures @@ -519,7 +663,6 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel bool handledExprNode; exprData data; constraint cons; - constraintList tempList; if (exprNode_handleError (e)) { @@ -534,7 +677,8 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel e->trueEnsuresConstraints = constraintList_new();; e->falseEnsuresConstraints = constraintList_new();; - + // e = makeDataTypeConstraints (e); + handledExprNode = TRUE; data = e->edata; diff --git a/src/constraintResolve.c b/src/constraintResolve.c index f8c1f44..8495f9c 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -53,6 +53,27 @@ constraintList constraintList_mergeEnsures (constraintList list1, constraintList //return ret; } + +/* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */ +/* { */ + +/* constraintList ret; */ +/* constraintList temp; */ +/* ret = constraintList_new(); */ + +/* ret = reflectChangesEnsures (list1, list2); */ +/* ret = constraintList_fixConflicts (ret, list2); */ +/* ret = constraintList_subsumeEnsures (ret, list2); */ +/* list2 = constraintList_subsumeEnsures (list2, ret); */ +/* temp = constraintList_copy(list2); */ + +/* temp = constraintList_addList (temp, ret); */ +/* return temp; */ +/* //ret = constraintList_addList (ret, list2); */ +/* //return ret; */ +/* } */ + + constraintList checkCall (exprNode fcn, exprNodeList arglist) { constraintList preconditions; @@ -170,7 +191,17 @@ constraintList reflectChanges (constraintList pre2, constraintList post1) { temp = substitute (el, post1); if (!resolve (temp, post1) ) - ret = constraintList_add (ret, temp); + { + // try inequality substitution + constraint temp2; + + // the inequality substitution may cause us to lose information + //so we don't want to store the result but we do it anyway + temp2 = constraint_copy (temp); + temp2 = inequalitySubstitute (temp, post1); + if (!resolve (temp2, post1) ) + ret = constraintList_add (ret, temp2); + } } } end_constraintList_elements; @@ -323,7 +354,7 @@ bool arithType_canResolve (arithType ar1, arithType ar2) case LT: case LTE: - llassert(FALSE); + // llassert(FALSE); if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) ) return TRUE; } @@ -385,7 +416,7 @@ bool constraint_search (constraint c, constraintExpr old) return ret; } - +//adjust file locs and stuff constraint constraint_adjust (constraint substitute, constraint old) { fileloc loc1, loc2, loc3; @@ -418,6 +449,39 @@ constraint constraint_adjust (constraint substitute, constraint old) } +constraint inequalitySubstitute (constraint c, constraintList p) +{ + if (c->ar != GTE) + return c; + + constraintList_elements (p, el) + { + if ( el->ar == LT) + // if (!constraint_conflict (c, el) ) + { + constraint temp; + temp = constraint_copy(el); + + // temp = constraint_adjust(temp, c); + + if (constraintExpr_same (el->lexpr, c->expr) ) + { + DPRINTF((message ("Replacing %s in %s with %s", + constraintExpr_print (c->expr), + constraint_print (c), + constraintExpr_print (el->expr) ) + )); + c->expr = constraintExpr_copy (el->expr); + } + + } + } + end_constraintList_elements; + + c = constraint_simplify(c); + return c; +} + constraint substitute (constraint c, constraintList p) { constraintList_elements (p, el) diff --git a/src/ctype.c b/src/ctype.c index cfd20bf..911c00b 100644 --- a/src/ctype.c +++ b/src/ctype.c @@ -2377,3 +2377,22 @@ ctype_widest (ctype c1, ctype c2) return c1; } } + +/*drl 11/28/2000 */ +/* requires that the type is an fixed array */ +/* return the size of the array */ + +int ctype_getArraySize (ctype c) +{ + ctentry cte = ctype_getCtentry (c); + ctbase ctb; + llassert ( (ctentry_getKind (cte) == CTK_COMPLEX) || (ctentry_getKind(cte) == CTK_ARRAY) ); + + ctb = cte->ctbase; + + llassert (ctbase_isDefined (ctb) ); + + llassert (ctb->type == CT_FIXEDARRAY); + + return (ctb->contents.farray->size); +} diff --git a/src/exprChecks.c b/src/exprChecks.c index 7ed778c..cbcae41 100644 --- a/src/exprChecks.c +++ b/src/exprChecks.c @@ -896,6 +896,7 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) constraintList c, t; /* drl added 8-8-2000 */ + return; exprNode_generateConstraints (body); c = uentry_getFcnPreconditions (ue); @@ -922,15 +923,19 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) if (c) { - TPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) ); + DPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) ); } else { - TPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) ); + DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) ); } - printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) ); - printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) ); + ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(body->requiresConstraints) ), g_currentloc); + + ConPrint (message ("LCLint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc); + + // printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) ); + // printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) ); context_exitInnerPlain(); /* exprNode_free (body); */ diff --git a/src/lltok.c b/src/lltok.c index 93dc662..c9aaa6e 100644 --- a/src/lltok.c +++ b/src/lltok.c @@ -69,6 +69,30 @@ bool lltok_isNot_Op (lltok tok) { return (tok.tok == TEXCL); } +/*drl7x added this function 11/20/00 */ + +bool lltok_isLt_Op (lltok tok) +{ + return (tok.tok == TLT); +} + +bool lltok_isGt_Op (lltok tok) +{ + return (tok.tok == TGT); +} + +bool lltok_isGe_Op (lltok tok) +{ + return (tok.tok == GE_OP); +} + +bool lltok_isLe_Op (lltok tok) +{ + return (tok.tok == LE_OP); +} + +/* end drl7x added */ + cstring lltok_unparse (lltok tok) diff --git a/src/sRef.c b/src/sRef.c index 8a5bc80..d776cc4 100644 --- a/src/sRef.c +++ b/src/sRef.c @@ -9091,3 +9091,23 @@ void sRef_resetLen(sRef p_s) { llfatalbug (message ("sRef_setLen passed an invalid sRef\n")); } } + +/*drl7x 11/28/2000 */ + +bool sRef_isFixedArray (sRef p_s) { + ctype c; + c = sRef_getType (p_s); + return ( ctype_isFixedArray (c) ); +} + +int sRef_getArraySize (sRef p_s) { + ctype c; + llassert (sRef_isFixedArray(p_s) ); + + c = sRef_getType (p_s); + + return (ctype_getArraySize (c) ); +} + + + -- 2.45.2