TODO.md

   1 # General
   2
   3
   4 ## Documentation
   5
   6 Document the build process for a stand-alone library (utilizing
   7 *libhwbase*'s build system).
   8
   9
  10 ## SPARK
  11
  12 * Rework the code to be valid SPARK (no errors from `gnatprove
  13   -m check`)
  14
  15 * Prove absence of runtime errors
  16
  17
  18 ## Configuration options
  19
  20 There are various configuration options throughout the code that
  21 should be moved into `HW.DbC_Config`.
  22
  23
  24 # Current Code
  25
  26
  27 ## `Receive`
  28
  29  * Do not unconditionally poll in Receive and respect poll
  30    deadline.
  31
  32
  33 ## `Transfers.Send`
  34
  35 * On `Start_Now`, make sure we start transferring even if we
  36   only appended to an already queued transfer. Or make it part
  37   of the contract that we are never called with `Start_Now =>
  38   True` when an already queued but not started transfer exists
  39   (which is currently true).
  40
  41 * Don't acquire a `Transfer_Id` (or release it on failure) if
  42   we can't enqueue it. Or make it part of the contract, that
  43   the `Transfer_Rings` are always big enough to hold all
  44   `Transfer_Id`s (which is currently true).
  45
  46
  47 ## `Transfer_Info`
  48
  49 * Use better strings in receive statistics
  50
  51 * Use wider numeric types for statistics
  52
  53
  54 ## `DMA_Buffers`
  55
  56 Currently, DMA addresses are precalculated which results in
  57 redundancies with constants used throughout the code. We could
  58 calculate DMA addresses based on compile time constants instead.