13 commits

Author	SHA1	Message	Date
Tobias Reinhard	6dcaef48d6	Added loop invariant to main search loop in prvSelectHighestPriorityTask.	2022-11-17 14:24:44 -05:00
Tobias Reinhard	4eb2fa573e	Wrote contracts for lock release operations.	2022-11-16 14:18:03 -05:00
Tobias Reinhard	54523ecdce	Included global variables pxCurrentTCBs and pxYieldingPendings in interrupt invariant.	2022-11-16 13:53:22 -05:00
Tobias Reinhard	d63a8f83cd	Renamed predicate encapsulating access permissions to core local variables to coreLocalInterruptInv_p.	2022-11-16 11:31:12 -05:00
Tobias Reinhard	327423ef67	TCB of currently scheduled task on core C is interrupt protected on core C. Updated invariants to reflect that.	2022-11-16 11:25:37 -05:00
Tobias Reinhard	360afe4374	Cleaned up lock predicate header.	2022-11-16 10:37:12 -05:00
Tobias Reinhard	d95976ebe5	Added info about available tasks to lock predicate.	2022-11-16 10:28:31 -05:00
Tobias Reinhard	d746a27233	Added missing task-ISR lock invariant to post condition of acquision lemma.	2022-11-11 15:07:01 -05:00
Tobias Reinhard	29e14be203	Verified minimal contract for xTaskGetCurrentTaskHandle.	2022-11-10 14:36:04 -05:00
Tobias Reinhard	7e75d7aa8f	Refined lock predicates and contracts for lock macros to match expected locking discipline.	2022-11-10 12:50:48 -05:00
Tobias Reinhard	91eb6eefaa	Included reference to core ID in interrupt predicates and added distinction between global and core local variables.	2022-11-07 14:21:42 -05:00
Tobias Reinhard	25dda73ef9	Started to define predicates encapsulating access permissions to global variables.	2022-11-04 14:22:11 -04:00
Tobias Reinhard	94e0f21574	Added rewrite to remove const qualifiers from pointers.	2022-11-04 11:15:15 -04:00