Update the test cases accordingly.
14 files changed:
# define cstring_compareLit(c,sub) \
(cstring_compare (c, cstring_fromChars (sub)))
# define cstring_compareLit(c,sub) \
(cstring_compare (c, cstring_fromChars (sub)))
+/*drl added 2/4/2002*/
+/*replaces every instance of the character old with the character new
+ old can not be '\0'
+*/
+cstring cstring_replaceChar(/*@returned@*/ cstring p_c, char p_oldChar, char p_newChar);
+
# else
# error "Multiple include"
# endif
# else
# error "Multiple include"
# endif
temp = constraint_getFileloc (c);
temp = constraint_getFileloc (c);
+
+ if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+ {
+ string = cstring_replaceChar(string, '\n', ' ');
+ }
+
if (fileloc_isDefined (temp))
{
errorLoc = temp;
if (fileloc_isDefined (temp))
{
errorLoc = temp;
fileloc_free (temp);
errorLoc = fileloc_copy (errorLoc);
}
fileloc_free (temp);
errorLoc = fileloc_copy (errorLoc);
}
+
+
+ if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+ {
+ string = cstring_replaceChar(string, '\n', ' ');
+ }
+
+
if (c->post)
{
voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
if (c->post)
{
voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
{
cstring st = cstring_undefined;
cstring temp = cstring_undefined;
{
cstring st = cstring_undefined;
cstring temp = cstring_undefined;
/*
Changed for 3.0.0.19
*/
/*
Changed for 3.0.0.19
*/
- gc.flags[FLG_ORCONSTRAINT] = TRUE;
+
+ /* commenting ou until some output issues are fixed */
+ /* gc.flags[FLG_ORCONSTRAINT] = TRUE;*/
+
gc.flags[FLG_CONSTRAINTLOCATION] = TRUE;
/*drl 1/18/2002*/
gc.flags[FLG_CONSTRAINTLOCATION] = TRUE;
/*drl 1/18/2002*/
+cstring cstring_replaceChar(/*@returned@*/ cstring c, char oldChar, char newChar)
+{
+ char *ptr;
+ llassert(oldChar != '\0');
+ if (cstring_isUndefined(c) )
+ {
+ llcontbug(cstring_makeLiteral("cstring_replaceChar called with undefined string"));
+ return c;
+ }
+
+ ptr = c;
+ while (*ptr != '\0')
+ {
+ if (*ptr == oldChar)
+ *ptr = newChar;
+ ptr++;
+ }
+
+ return c;
+}
"Memory read or write may be out of bounds of allocated storage.", 0, 0
},
{
"Memory read or write may be out of bounds of allocated storage.", 0, 0
},
{
- FK_BOUNDS, FK_MEMORY, modeFlag,
+ FK_BOUNDS, FK_MEMORY, plainFlag,
"boundsread",
FLG_BOUNDSREAD,
"possible out of bounds read",
"boundsread",
FLG_BOUNDSREAD,
"possible out of bounds read",
- FK_BOUNDS, FK_MEMORY, modeFlag,
+ FK_BOUNDS, FK_MEMORY, plainFlag,
"boundswrite",
FLG_BOUNDSWRITE,
"possible buffer overflow from an out of bounds write",
"boundswrite",
FLG_BOUNDSWRITE,
"possible buffer overflow from an out of bounds write",
- FK_BOUNDS, FK_DISPLAY, modeFlag,
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
"fcnpost",
FLG_FUNCTIONPOST,
"display function post conditions",
"fcnpost",
FLG_FUNCTIONPOST,
"display function post conditions",
- FK_BOUNDS, FK_DISPLAY, modeFlag,
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
"redundantconstraints",
FLG_REDUNDANTCONSTRAINTS,
"display seemingly redundant constraints",
"redundantconstraints",
FLG_REDUNDANTCONSTRAINTS,
"display seemingly redundant constraints",
- FK_BOUNDS, FK_MEMORY, modeFlag,
+ FK_BOUNDS, FK_MEMORY, plainFlag,
"implictconstraint",
FLG_IMPLICTCONSTRAINT,
"generate implicit constraints for functions",
"implictconstraint",
FLG_IMPLICTCONSTRAINT,
"generate implicit constraints for functions",
},
/*drl7x added 4/29/01 */
{
},
/*drl7x added 4/29/01 */
{
- FK_BOUNDS, FK_MEMORY, modeFlag,
+ FK_BOUNDS, FK_MEMORY, plainFlag,
"orconstraint",
FLG_ORCONSTRAINT,
"use limited OR expressions to resolve constraints",
"orconstraint",
FLG_ORCONSTRAINT,
"use limited OR expressions to resolve constraints",
- FK_BOUNDS, FK_MEMORY, modeFlag,
+ FK_BOUNDS, FK_MEMORY, plainFlag,
"nullterminated",
FLG_NULLTERMINATEDWARNING,
"misuse of nullterminated allocation",
"nullterminated",
FLG_NULLTERMINATEDWARNING,
"misuse of nullterminated allocation",
- FK_BOUNDS, FK_DISPLAY, modeFlag,
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
"showconstraintparens",
FLG_PARENCONSTRAINT,
"display parentheses around constraint terms",
NULL,
0, 0
},
"showconstraintparens",
FLG_PARENCONSTRAINT,
"display parentheses around constraint terms",
NULL,
0, 0
},
+ /*drl added 2/4/2002*/
+ {
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
+ "boundscompacterrormessages",
+ FLG_BOUNDSCOMPACTERRORMESSAGES,
+ "Display fewer new lines in bounds checking error messages",
+ NULL,
+ 0, 0
+ },
- FK_BOUNDS, FK_DISPLAY, modeFlag,
+ FK_BOUNDS, FK_DISPLAY, plainFlag,
"showconstraintlocation",
FLG_CONSTRAINTLOCATION,
"display location for every constraint generated",
"showconstraintlocation",
FLG_CONSTRAINTLOCATION,
"display location for every constraint generated",
- FK_DEBUG, FK_BOUNDS, modeFlag,
+ FK_DEBUG, FK_BOUNDS, plainFlag,
"debugfcnconstraint",
FLG_DEBUGFUNCTIONCONSTRAINT,
"debug function constraints",
"debugfcnconstraint",
FLG_DEBUGFUNCTIONCONSTRAINT,
"debug function constraints",
constannot.c: (in function foo2)
constannot.c:11:3: Possible out-of-bounds store:
constannot.c: (in function foo2)
constannot.c:11:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(str @ constannot.c:11:3) >= 20
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:
Unable to resolve constraint:
requires maxSet(str @ constannot.c:11:3) >= 20
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:
Unable to resolve constraint:
requires <const int=20> <= 19
needed to satisfy precondition:
Unable to resolve constraint:
requires <const int=20> <= 19
needed to satisfy precondition:
for.c: (in function f)
for.c:13:5: Possible out-of-bounds store:
for.c: (in function f)
for.c:13:5: Possible out-of-bounds store:
Unable to resolve constraint:
requires i @ for.c:13:7 <= 10
needed to satisfy precondition:
Unable to resolve constraint:
requires i @ for.c:13:7 <= 10
needed to satisfy precondition:
maxsetnoannotations.c: (in function noancopy)
maxsetnoannotations.c:2:3: Possible out-of-bounds store:
maxsetnoannotations.c: (in function noancopy)
maxsetnoannotations.c:2:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(a @ maxsetnoannotations.c:2:11) >= maxRead(b @
maxsetnoannotations.c:2:13)
Unable to resolve constraint:
requires maxSet(a @ maxsetnoannotations.c:2:11) >= maxRead(b @
maxsetnoannotations.c:2:13)
initialization.c: (in function initialization)
initialization.c:5:10: Variable g declared but not used
initialization.c:5:14: Possible out-of-bounds read:
initialization.c: (in function initialization)
initialization.c:5:10: Variable g declared but not used
initialization.c:5:14: Possible out-of-bounds read:
Unable to resolve constraint:
requires maxRead(d @ initialization.c:3:14) >= 22
needed to satisfy precondition:
requires maxRead(e @ initialization.c:5:14) >= 22
initialization.c:8:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxRead(d @ initialization.c:3:14) >= 22
needed to satisfy precondition:
requires maxRead(e @ initialization.c:5:14) >= 22
initialization.c:8:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(d @ initialization.c:3:14) >= 2
needed to satisfy precondition:
requires maxSet(f @ initialization.c:8:3) >= 2
simplifyTest.c: (in function fooSub)
simplifyTest.c:3:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(d @ initialization.c:3:14) >= 2
needed to satisfy precondition:
requires maxSet(f @ initialization.c:8:3) >= 2
simplifyTest.c: (in function fooSub)
simplifyTest.c:3:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
needed to satisfy precondition:
requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
simplifyTest.c: (in function fooAdd)
simplifyTest.c:10:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
needed to satisfy precondition:
requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
simplifyTest.c: (in function fooAdd)
simplifyTest.c:10:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
needed to satisfy precondition:
Unable to resolve constraint:
requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
needed to satisfy precondition:
strncatNotReallyGood.c:4:29: Passed storage buffer not completely defined
(*buffer is undefined): strncat (buffer, ...)
strncatNotReallyGood.c:4:21: Possible out-of-bounds store:
strncatNotReallyGood.c:4:29: Passed storage buffer not completely defined
(*buffer is undefined): strncat (buffer, ...)
strncatNotReallyGood.c:4:21: Possible out-of-bounds store:
+ strncat(buffer, str, sizeof((buffer)) - 1)
Unable to resolve constraint:
requires maxRead(buffer @ strncatNotReallyGood.c:4:29) <= 0
needed to satisfy precondition:
Unable to resolve constraint:
requires maxRead(buffer @ strncatNotReallyGood.c:4:29) <= 0
needed to satisfy precondition:
unknownsize.c: (in function uknSize1)
unknownsize.c:9:3: Possible out-of-bounds store:
unknownsize.c: (in function uknSize1)
unknownsize.c:9:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(c @ unknownsize.c:9:3) >= 9
needed to satisfy precondition:
Unable to resolve constraint:
requires maxSet(c @ unknownsize.c:9:3) >= 9
needed to satisfy precondition:
fixedArrayType.c: (in function fixedArrayTouch)
fixedArrayType.c:9:3: Possible out-of-bounds store:
fixedArrayType.c: (in function fixedArrayTouch)
fixedArrayType.c:9:3: Possible out-of-bounds store:
+ buffer[sizeof(Array) - 1]
Unable to resolve constraint:
requires sizeof(Array) @ fixedArrayType.c:9:23 <= 10
needed to satisfy precondition:
Unable to resolve constraint:
requires sizeof(Array) @ fixedArrayType.c:9:23 <= 10
needed to satisfy precondition:
mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
mystrncat (b, ...)
mystrncat.c:12:3: Possible out-of-bounds store:
mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
mystrncat (b, ...)
mystrncat.c:12:3: Possible out-of-bounds store:
+ mystrncat(buffer, str, sizeof((buffer)) - 1)
Unable to resolve constraint:
requires maxRead(buffer @ mystrncat.c:12:13) <= 0
needed to satisfy precondition:
Unable to resolve constraint:
requires maxRead(buffer @ mystrncat.c:12:13) <= 0
needed to satisfy precondition:
derived from mystrncat precondition:
requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
mystrncat.c:13:3: Possible out-of-bounds store:
derived from mystrncat precondition:
requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
mystrncat.c:13:3: Possible out-of-bounds store:
+ mystrncat(b, str, sizeof((buffer)) - 1)
Unable to resolve constraint:
requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0
needed to satisfy precondition:
Unable to resolve constraint:
requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0
needed to satisfy precondition:
;;; Splint Library null6.lcd
;;Splint 3.0.1.4 --- 19 Jan 2002
;;; Splint Library null6.lcd
;;Splint 3.0.1.4 --- 19 Jan 2002
;;ctTable
0 u-2 19 38
0 p1|-2 20 39
;;ctTable
0 u-2 19 38
0 p1|-2 20 39
m.c:8:5: Storage f may become null
sizeof.c: (in function f)
sizeof.c:17:1: Possible out-of-bounds store:
m.c:8:5: Storage f may become null
sizeof.c: (in function f)
sizeof.c:17:1: Possible out-of-bounds store:
Unable to resolve constraint:
requires 2 >= 3
needed to satisfy precondition:
Unable to resolve constraint:
requires 2 >= 3
needed to satisfy precondition:
m.c:11:1: Previous definition of t
test3.c: (in function t)
test3.c:9:3: Possible out-of-bounds store:
m.c:11:1: Previous definition of t
test3.c: (in function t)
test3.c:9:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires 99 >= 101
needed to satisfy precondition:
Unable to resolve constraint:
requires 99 >= 101
needed to satisfy precondition:
m.c:11:1: Previous definition of t
test7.c: (in function t)
test7.c:6:3: Possible out-of-bounds store:
m.c:11:1: Previous definition of t
test7.c: (in function t)
test7.c:6:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(g @ test7.c:4:3) >= 4
needed to satisfy precondition:
requires maxSet(g @ test7.c:6:3) >= 2
test7.c:8:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(g @ test7.c:4:3) >= 4
needed to satisfy precondition:
requires maxSet(g @ test7.c:6:3) >= 2
test7.c:8:3: Possible out-of-bounds store:
Unable to resolve constraint:
requires maxSet(j @ test7.c:8:3) >= 0
needed to satisfy precondition:
Unable to resolve constraint:
requires maxSet(j @ test7.c:8:3) >= 0
needed to satisfy precondition:
;;; Splint Library newlint.lcd
;;Splint 3.0.1.4 --- 19 Jan 2002
;;; Splint Library newlint.lcd
;;Splint 3.0.1.4 --- 19 Jan 2002
;;ctTable
0 u-2 19 38
0 p1|-2 20 39
;;ctTable
0 u-2 19 38
0 p1|-2 20 39