[splint-discuss] How to use bounds checks?
Wenzel, Bodo
wenzel at bbr-vt.de
Tue Sep 19 06:13:52 EDT 2006
Hi.
Starting a new project we thought that using Splint would be a good
idea. But we ran into problems, especially with bounds checks. The
source code (with a silly example) below contains comments that
describe our difficulties, any help is welcome!
Oh, and sorry for the long posting.
Splint (Win32 version 3.1.1) is called with:
============================================
+checks +partial +bounds -export-header
Source code:
============
int no_sub_no_error(const int *pointer)
/*@modifies nothing@*/
/*@requires maxRead(pointer) >= 9@*/
;
int no_sub_no_error(const int *pointer) {
int array[12];
int pointer_index, array_index;
int sum;
pointer_index = 0;
for (array_index = 0; array_index < 10; array_index++) {
array[array_index + 0] = pointer[pointer_index++];
array[array_index + 1] = 0;
array[array_index + 2] = 0;
}
#if defined(S_SPLINT_S)
/* Apparently Splint doesn't remember which cells were written
* just above.
*/
array_index = 10 - 1; /* set loop maximum */
array[11] = 0; /* set maxRead(array) */
#endif
sum = 0;
for (array_index = 0; array_index < 10; array_index++) {
sum += array[array_index + 0]
* array[array_index + 1]
* array[array_index + 2];
}
return sum;
}
/*----------------------------------------------------------------*/
int no_sub_error_caught(const int *pointer)
/*@modifies nothing@*/
/*@requires maxRead(pointer) >= 10@*/
;
int no_sub_error_caught(const int *pointer) {
int array[12];
int pointer_index, array_index;
int sum;
pointer_index = 0;
for (array_index = 0; array_index < 11; array_index++) {
array[array_index + 0] = pointer[pointer_index++];
array[array_index + 1] = 0;
array[array_index + 2] = 0; /* must report an error */
}
#if defined(S_SPLINT_S)
/* Apparently Splint doesn't remember which cells were written
* just above.
*/
array_index = 11 - 1; /* set loop maximum */
array[11] = 0; /* set maxRead(array) */
#endif
sum = 0;
for (array_index = 0; array_index < 11; array_index++) {
sum += array[array_index + 0]
* array[array_index + 1]
* array[array_index + 2]; /* must report an error */
}
return sum;
}
/*----------------------------------------------------------------*/
int no_sub_false_error(const int *pointer)
/*@modifies nothing@*/
/*@requires maxRead(pointer) >= 9@*/
;
int no_sub_false_error(const int *pointer) {
int array[12];
int pointer_index, array_index, index;
int sum;
pointer_index = 0;
array_index = 0;
for (index = 0; index < 10; index++) {
array[array_index + 0] = pointer[pointer_index++];
array[array_index + 1] = 0;
array[array_index + 2] = 0;
array_index++;
}
sum = 0;
array_index = 0;
for (index = 0; index < 10; index++) {
/* Apparently Splint doesn't remember which cells were written
* just above. So false errors are reported...
*/
sum += array[array_index + 0]
* array[array_index + 1]
* array[array_index + 2];
array_index++;
}
return sum;
}
/*----------------------------------------------------------------*/
int with_sub_no_error(const int *pointer)
/*@modifies nothing@*/
/*@requires maxRead(pointer) >= 9@*/
;
static void prepare_array_no_error(/*@out@*/ int *array, const int
*pointer)
/*@modifies array[]@*/
/*@requires maxSet(array) >= 11
/\ maxRead(pointer) >= 9@*/
/*@ensures maxRead(array) == 11@*/
;
static int calculate_sum_no_error(const int *array)
/*@modifies nothing@*/
/*@requires maxRead(array) >= 11@*/
;
int with_sub_no_error(const int *pointer) {
int array[12];
prepare_array_no_error(array, pointer);
return calculate_sum_no_error(array);
}
static void prepare_array_no_error(int *array, const int *pointer) {
int pointer_index, array_index, index;
/* Everything is fine in this part :-)
* But the extra variable 'index' doesn't look nice.
*/
pointer_index = 0;
array_index = 0;
for (index = 0; index < 10; index++) {
array[array_index + 0] = pointer[pointer_index++];
array[array_index + 1] = 0;
array[array_index + 2] = 0;
array_index++;
}
}
static int calculate_sum_no_error(const int *array) {
int sum;
int array_index, index;
/* Everything is fine in this part :-)
* But the extra variable 'index' doesn't look nice.
*/
sum = 0;
array_index = 0;
for (index = 0; index < 10; index++) {
sum += array[array_index + 0]
* array[array_index + 1]
* array[array_index + 2];
array_index++;
}
return sum;
}
/*----------------------------------------------------------------*/
int with_sub_error_caught(const int *pointer)
/*@modifies nothing@*/
/*@requires maxRead(pointer) >= 10@*/
;
static void prepare_array_error_caught(/*@out@*/ int *array, const
int *pointer)
/*@modifies array[]@*/
/*@requires maxSet(array) >= 11
/\ maxRead(pointer) >= 10@*/
/*@ensures maxRead(array) == 11@*/
;
static int calculate_sum_error_caught(const int *array)
/*@modifies nothing@*/
/*@requires maxRead(array) >= 11@*/
;
int with_sub_error_caught(const int *pointer) {
int array[12];
prepare_array_error_caught(array, pointer);
return calculate_sum_error_caught(array);
}
static void prepare_array_error_caught(int *array, const int
*pointer) {
int pointer_index, array_index, index;
/* Everything is fine in this part :-)
* But the extra variable 'index' doesn't look nice.
*/
pointer_index = 0;
array_index = 0;
for (index = 0; index < 11; index++) {
array[array_index + 0] = pointer[pointer_index++];
array[array_index + 1] = 0;
array[array_index + 2] = 0;
array_index++;
}
}
static int calculate_sum_error_caught(const int *array) {
int sum;
int array_index, index;
/* Everything is fine in this part :-)
* But the extra variable 'index' doesn't look nice.
*/
sum = 0;
array_index = 0;
for (index = 0; index < 11; index++) {
sum += array[array_index + 0]
* array[array_index + 1]
* array[array_index + 2];
array_index++;
}
return sum;
}
/*----------------------------------------------------------------*/
int with_sub_false_error(const int *pointer)
/*@modifies nothing@*/
/*@requires maxRead(pointer) >= 9@*/
;
static void prepare_array_false_error(/*@out@*/ int *array, const int
*pointer)
/*@modifies array[]@*/
/*@requires maxSet(array) >= 11
/\ maxRead(pointer) >= 9@*/
/*@ensures maxRead(array) == 11@*/
;
static int calculate_sum_false_error(const int *array)
/*@modifies nothing@*/
/*@requires maxRead(array) >= 11@*/
;
int with_sub_false_error(const int *pointer) {
int array[12];
prepare_array_false_error(array, pointer);
return calculate_sum_false_error(array);
}
static void prepare_array_false_error(int *array, const int *pointer)
{
int index;
for (index = 0; index < 10; index++) {
/* Splint doesn't know exactly which cells are written to,
* when the extra variable 'index' is "optimized away".
*/
array[index + 0] = pointer[index];
array[index + 1] = 0;
array[index + 2] = 0;
}
}
static int calculate_sum_false_error(const int *array) {
int sum;
int index;
sum = 0;
for (index = 0; index < 10; index++) {
/* Splint doesn't know exactly which cells are read,
* when the extra variable 'index' is "optimized away".
*/
sum += array[index + 0]
* array[index + 1]
* array[index + 2];
}
return sum;
}
Splint output:
==============
Splint 3.1.1 --- 12 April 2003
bounds060919.c: (in function no_sub_error_caught)
bounds060919.c(51,5): Possible out-of-bounds store:
array[array_index + 2]
Unable to resolve constraint:
requires array_index @ bounds060919.c(51,11) <= 9
needed to satisfy precondition:
requires maxSet(array @ bounds060919.c(51,5)) >= array_index @
bounds060919.c(51,11) + 2
A memory write may write to an address beyond the allocated buffer.
(Use
-boundswrite to inhibit warning)
bounds060919.c(65,14): Possible out-of-bounds read:
array[array_index + 2]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(65,14)) >= 12
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(65,14)) >= array_index @
bounds060919.c(65,20) + 2
A memory read references memory beyond the allocated storage. (Use
-boundsread to inhibit warning)
bounds060919.c: (in function no_sub_false_error)
bounds060919.c(98,12): Possible out-of-bounds read:
array[array_index + 0]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(98,12)) >= 9
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(98,12)) >= array_index @
bounds060919.c(98,18) + 0
bounds060919.c(98,12): Possible out-of-bounds read:
array[array_index + 0]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(98,12)) >= 0
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(98,12)) >= array_index @
bounds060919.c(98,18) + 0
bounds060919.c(99,14): Possible out-of-bounds read:
array[array_index + 1]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(99,14)) >= 10
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(99,14)) >= array_index @
bounds060919.c(99,20) + 1
bounds060919.c(99,14): Possible out-of-bounds read:
array[array_index + 1]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(99,14)) >= 1
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(99,14)) >= array_index @
bounds060919.c(99,20) + 1
bounds060919.c(100,14): Possible out-of-bounds read:
array[array_index + 2]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(100,14)) >= 11
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(100,14)) >= array_index @
bounds060919.c(100,20) + 2
bounds060919.c(100,14): Possible out-of-bounds read:
array[array_index + 2]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(100,14)) >= 2
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(100,14)) >= array_index @
bounds060919.c(100,20) + 2
bounds060919.c: (in function prepare_array_error_caught)
bounds060919.c(208,5): Possible out-of-bounds store:
array[array_index + 2]
Unable to resolve constraint:
requires maxSet(array @ bounds060919.c(208,5)) >= 12
needed to satisfy precondition:
requires maxSet(array @ bounds060919.c(208,5)) >= array_index @
bounds060919.c(208,11) + 2
bounds060919.c: (in function calculate_sum_error_caught)
bounds060919.c(226,14): Possible out-of-bounds read:
array[array_index + 2]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(226,14)) >= 12
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(226,14)) >= array_index @
bounds060919.c(226,20) + 2
bounds060919.c: (in function prepare_array_false_error)
bounds060919.c(268,5): Possible out-of-bounds store:
array[index + 2]
Unable to resolve constraint:
requires maxSet(array @ bounds060919.c(268,5)) >= index @
bounds060919.c(268,11) + 2
needed to satisfy precondition:
requires maxSet(array @ bounds060919.c(268,5)) >= index @
bounds060919.c(268,11) + 2
bounds060919.c: (in function calculate_sum_false_error)
bounds060919.c(282,14): Possible out-of-bounds read:
array[index + 1]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(282,14)) >= index @
bounds060919.c(282,20) + 1
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(282,14)) >= index @
bounds060919.c(282,20) + 1
bounds060919.c(283,14): Possible out-of-bounds read:
array[index + 2]
Unable to resolve constraint:
requires maxRead(array @ bounds060919.c(283,14)) >= index @
bounds060919.c(283,20) + 2
needed to satisfy precondition:
requires maxRead(array @ bounds060919.c(283,14)) >= index @
bounds060919.c(283,20) + 2
Finished checking --- 13 code warnings
With regards,
Bodo Wenzel
- Software Development -
--
BBR - Baudis Bergmann Rösch
Verkehrstechnik GmbH
Pillaustraße 1e
D - 38126 Braunschweig
T: +49.531.27300-766
F: +49.531.27300-999
@: wenzel at bbr-vt.de
W: http://www.bbr-vt.de
More information about the splint-discuss
mailing list