Explained how to check the proof in the REAMDE.

Test/VeriFast/tasks/vTaskSwitchContext/README.md

@@ -98,6 +98,37 @@ FreeRTOS-Kernel
 
 
 
+# Checking the Proof
+The proof can be checked by running one of the scripts 'run-verifast.sh' and
+'run-vfide.sh' residing in this directory (see repo structure above).
+Both scripts preprocess the annotated code with Clang and rewrite syntax
+VeriFast does not understand into something equivalent.
+The result is written to a temporary file ('preprocessed_files/tasks_vf_pp.c')
+before it is processed by VeriFast.
+This file contains a copy of all the code and annotations required to check the
+proof.
+Both scripts expect the command line arguments explained below.
+In the following we use the following variables
+
+- #### run-verifast.sh:
+  Preprocesses the code and proof files and uses the
+  command-line version of VeriFast to check the resulting proof file.
+  A call must have the form:
+  #### run-verifast.sh \<REPO_BASE_DIR\> \<VERIFAST_DIR\>
+  where
+  - \<REPO_BASE_DIR\> is the absolute path to this repository's base directory,
+    i.e., 'FreeRTOS-Kernel' in the repo structure depicted above.
+  - \<VERIFAST_DIR\> is the absolute path to the VeriFast installation
+    directory.
+
+- #### run-vfide.sh:
+  Preprocesses the code and proof files and loads the resulting proof file into
+  the VeriFast IDE.
+  A call must have the form:
+  #### run-vfide.sh \<REPO_BASE_DIR\> \<VERIFAST_DIR\> \[\<FONT_SIZE\>\]
+  where
+  - \<REPO_BASE_DIR\> \<VERIFAST_DIR\> are as explained above
+  - \<FONT_SIZE\> is an optional argument specifying the IDE's font size.
+
 # Proof Setup
 The VeriFast proofs assume a setup for the Raspberry Pi Pico, i.e., RP2040.
-