From 0adb318dd9cb0abff9f709f6d67d6accff63c36f Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Sat, 31 Dec 2022 16:16:52 -0500
Subject: [PATCH] Updated directory structure depicted in README.

---
 Test/VeriFast/tasks/vTaskSwitchContext/README.md | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/README.md
index f6004f5d3..ebde7b2d5 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/README.md
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/README.md
@@ -79,17 +79,14 @@ FreeRTOS-Kernel
 │
 │
 │
-├── tasks.c files
-│   The base directory contains the source files, in particular `tasks.c`.
-│   `tasks.c` has been annotated with the VeriFast proof steps necessary to
-│   prove memory safety and thread safety of `vTaskSwitchContext`.
-│   The proof uses many specifications and lemmas residing in
-│   `verification/verifast/proof_setup` and `verifcation/verifast/proofs`.
+├── *.c files
+│   The base directory contains the source files. Note that our proof uses
+│   annotated copies of these files located in the proof directory.
 │
 │
 ├── include
-│   Contains the header files. Some of the header files have been annotated with
-│   VeriFast contracts and proofs.
+│   Contains the header files. Note that our proof uses annotated copies of
+│   these files located in the proof directory.
 │
 │
 ├── portable