From a470fec6d090b9495e7b741ddd55b4750438b495 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Sun, 13 Nov 2022 14:46:17 -0500
Subject: [PATCH] Added automatic deletion of void casts (used to suppress
 warnings) and linked to filed VeriFast issue 335.

---
 tasks.c                                                  | 9 ++-------
 .../verifast/custom_build_scripts_RP2040/vf_rewrite.sh   | 5 +++++
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/tasks.c b/tasks.c
index 717a3dcec..d85d47afe 100644
--- a/tasks.c
+++ b/tasks.c
@@ -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
diff --git a/verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh b/verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh
index efdf96c05..3e95c833b 100755
--- a/verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh
+++ b/verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh
@@ -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"