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

Updated proof directory content listing in README.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-29 14:46:13 -05:00
parent 17004fbf1b
commit b0e2d1e3f0
1 changed files with 32 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

35
Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md
View file

@ -6,11 +6,40 @@ This directory contains the bulk of VeriFast formalizations and proofs.
# Directory Structure # Directory Structure
``` ```
├── *.h files ├── lock_predicates.h
│ Headers containing VeriFast formalizations and proofs. │ Contains the formalization of the lock invariants, i.e., the invariants
│ associated with: Masking interrupts, the task lock and the ISR lock.
│ This file also contains the lemmas to prove that the task state updates
│ in `prvSelectHighestPriorityTask` preserve the lock invariants.
│
├── port_contracts.h
│ Contains VeriFast function contracts for macros with port-specific
│ definitions, e.g., the macros to mask interrupts and to acquire AND
│ release locks. These port-specific definitions often contain contain
│ inline assembly VeriFast cannot reason about. The contracts allow us
│ to abstract the semantics of the assembly.
│
├── ready_list_predicates.h
│ Contains the predicates describing the ready lists as well as lemmas to
│ reason about ready lists.
│
├── stack_predicates.h
│ Contains the formalization of the stack layout used in the RP2040 port.
│
├── task_predicates.h
│ Contains predicates describing task control blocks.
│
├── task_running_states.h
│ `tasks.c` defines macros that are used to denote task run states.
│ The proof headers in this directory cannot refer to these macros.
│ This header contains auxiliary definitions used to expose the run state
│ macros to the proof headers.
│
├── verifast_lists_extended.h
│ Contains list axioms and lemmas that would naturally fit into VeriFast's
│ standard list library `listex.gh`.
│ │
├── README.md ├── README.md
│ Contains more details about the proof.
│ │
├── single_core_proofs ├── single_core_proofs
│ Contains the old list formalization and proofs written by │ Contains the old list formalization and proofs written by