Skip to content

Commit

Permalink
Added null terminator to every string
Browse files Browse the repository at this point in the history
  • Loading branch information
Bujain committed Sep 2, 2021
1 parent 1762c85 commit 6d32385
Showing 1 changed file with 11 additions and 2 deletions.
13 changes: 11 additions & 2 deletions test/cbmc/proofs/stringBuilder/stringBuilder_harness.c
Original file line number Diff line number Diff line change
Expand Up @@ -30,19 +30,28 @@ void stringBuilder_harness()
/* pBuffer can never be NULL since it it always initialized before passing it to the stringBuilder function. */
__CPROVER_assume( pBuffer != NULL );

/* The minimum and the maximum number of strings inside the numStrings is 11. */
/* The minimum and the maximum number of strings inside the numStrings are 0 and 11. */
__CPROVER_assume( numStrings > 0 && numStrings < UINT32_MAX );

/* Initializing an array of strings with size numStrings. */
strings = ( char ** ) malloc( numStrings * sizeof( char * ) );

/* The size of each string inside the strings array passed to the stringBuilder
* function is greater than 0. */
__CPROVER_assume( stringSize > 0 );

/* The strings array cannot be NULL as it is always initialized before
* passing to the function. */
__CPROVER_assume( strings != NULL );

for( i = 0; i < numStrings - 1; ++i )
{
strings[ i ] = ( char * ) malloc( stringSize );

/* The strings inside the strings array are defined before passing it to
* the stringBuilder function. */
__CPROVER_assume( strings[ i ] != NULL );
strings[ i ][ stringSize - 1 ] = '\0';
}

/* Strings array is always passed with a NULL string at the end. */
Expand All @@ -53,7 +62,7 @@ void stringBuilder_harness()
/* Free the allocated memory. */
free( pBuffer );

for( i = 0; i < numStrings; ++i )
for( i = 0; i < numStrings - 1; ++i )
{
free( strings[ i ] );
}
Expand Down

0 comments on commit 6d32385

Please sign in to comment.