Add a byte.
(&mut self, value: u8)
| 540 | |
| 541 | /// Add a byte. |
| 542 | pub fn put1(&mut self, value: u8) { |
| 543 | self.data.push(value); |
| 544 | |
| 545 | // Post-invariant: conceptual-labels_at_tail contains a complete and |
| 546 | // precise list of labels bound at `cur_offset()`. We have advanced |
| 547 | // `cur_offset()`, hence if it had been equal to `labels_at_tail_off` |
| 548 | // before, it is not anymore (and it cannot become equal, because |
| 549 | // `labels_at_tail_off` is always <= `cur_offset()`). Thus the list is |
| 550 | // conceptually empty (even though it is only lazily cleared). No labels |
| 551 | // can be bound at this new offset (by invariant on `label_offsets`). |
| 552 | // Hence the invariant holds. |
| 553 | } |
| 554 | |
| 555 | /// Add 2 bytes. |
| 556 | pub fn put2(&mut self, value: u16) { |