len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-12 06:35:19 -05:00
Code Issues Projects Releases Packages Wiki Activity

Added automatic deletion of void casts (used to suppress warnings) and linked to filed VeriFast issue 335.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-13 14:46:17 -05:00
parent 1e2acf6139
commit a470fec6d0
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
tasks.c
View file

@ -1496,17 +1496,12 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
/* Fill the stack with a known value to assist debugging. */
#ifdef VERIFAST
/* Reason for rewrite:
* - VeriFast does not support casts involving side-effectful
* expressions.
* - VeriFast report type mismatch because
* - VeriFast reports type mismatch because
* `( int ) tskSTACK_FILL_BYTE` is passed for a char argument.
*
* Note: The only affect of void casts is to surpress compiler
* warnings.
*
* TODO: Is the type mismatch a real error?
*/
memset( pxNewTCB->pxStack, ( char ) tskSTACK_FILL_BYTE, ( size_t ) ulStackDepth * sizeof( StackType_t ) );
( void ) memset( pxNewTCB->pxStack, ( char ) tskSTACK_FILL_BYTE, ( size_t ) ulStackDepth * sizeof( StackType_t ) );
#else
( void ) memset( pxNewTCB->pxStack, ( int ) tskSTACK_FILL_BYTE, ( size_t ) ulStackDepth * sizeof( StackType_t ) );
#endif

5
verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh
View file

@ -36,6 +36,11 @@ rewrite "__attribute__(([_a-z]*))" ""
# TODO: Why does matching `\s` or `:space:` not work on MacOs?
rewrite "__attribute__( ( [_a-z]* ) )" ""
echo "Delete void casts (used to suppress compiler warnings)"
echo "Reported issue 335"
echo "https://github.com/verifast/verifast/issues/335"
rewrite "( void ) memset" "memset"
echo "Removing const qualifiers from pointers"
echo "Reported issue 333:"
echo "https://github.com/verifast/verifast/issues/333"