8 commits

Author	SHA1	Message	Date
Tobias Reinhard	eedbfe3255	Typo.	2022-10-28 13:26:17 -04:00
Tobias Reinhard	06b924d818	Verified alignment properties of stack top pointer.	2022-10-28 13:24:01 -04:00
Tobias Reinhard	551d1da628	Renamed TCB_p predicate into uninit_TCB_p.	2022-10-27 12:58:18 -04:00
Tobias Reinhard	b5f0b2f74d	Added snippet from RP2040 port.c to verification code base to allow verification of contract from portable.h	2022-10-26 10:08:29 -04:00
Tobias Reinhard	40931d229d	Justified memset of TCB fields in prvInitialiseNewTask. ... Fields: `pxNewTCB->ucNotifyState` and `pxNewTCB->ulNotifiedValue`	2022-10-25 16:56:28 -04:00
Tobias Reinhard	8a8f0ab9b1	Proved memory safety of name-writing loop in prvInitialiseNewTask.	2022-10-25 14:57:26 -04:00
Tobias Reinhard	1042ea8cf8	Refined task control block predicate TCB_p such that it can be used to justify memset-ing the stack.	2022-10-25 13:22:10 -04:00
Tobias Reinhard	5a7916bff0	Added predicates to reason about TCB_t and substructures.	2022-10-24 16:17:41 -04:00