Code

ADT_C sorry-free#685

Code

Merged

michaelmcinerney merged 7 commits intortseL4/l4v:rtfrom michaelm-adt_c_sorry_freeseL4/l4v:michaelm-adt_c_sorry_freeCopy head branch name to clipboardOct 23, 2023

+1,650-1,110

Commits

Commits on Oct 19, 2023

• rt aspec: zero out budget when finalising a scheduling context

  Show description for 0b8eb8d
  michaelmcinerney

  committed
  0b8eb8d

  Copy full SHA for 0b8eb8d

• rt ainvs: add invariant for inactive sc implies zero budget

  Show description for f1471bd
  michaelmcinerney

  committed
  f1471bd

  Copy full SHA for f1471bd

• rt design+haskell: remove scBudget field from SchedContext record

  Show description for 75f732a
  michaelmcinerney

  committed
  75f732a

  Copy full SHA for 75f732a

Commits on Oct 23, 2023

• rt riscv refine: update after removing scBudget field

  Show description for 18b1641
  michaelmcinerney

  committed
  18b1641

  Copy full SHA for 18b1641

• rt arm refine: update after removing scBudget field

  Show description for fa57dc4
  michaelmcinerney

  committed
  fa57dc4

  Copy full SHA for fa57dc4

• rt crefine: clear sorries related to cpspace_refill_relation_unique

  Show description for d0fdb09
  michaelmcinerney

  committed
  d0fdb09

  Copy full SHA for d0fdb09

• rt crefine: ADT_C.thy sorry free

  Show description for b843dad
  michaelmcinerney

  committed
  b843dad

  Copy full SHA for b843dad