begriffs open source - cmsis-freertos/blob - Test/VeriFast/scripts/diff_files.md

   1 # Generate diffs between FreeRTOS source and proofs
   2
   3 ## Requirements
   4
   5   - python3
   6   - ctags 5.8
   7   - diff 3.4+
   8   - [diff2html](https://diff2html.xyz/)
   9
  10 ## Instructions
  11
  12 The following will extract per-function files from the original FreeRTOS source
  13 implementation and the proof directory.
  14
  15
  16 ```
  17 cd scripts
  18 ./generate_diff_files.sh
  19 # will extract to ./FreeRTOS-Kernel/generated and ./queue/generated and ./list/generated
  20 ```
  21
  22 Then use `diff` for a side-by-side comparison.  Note that the `--color=always`
  23 flag needs v3.4+:
  24
  25 ```
  26 diff --color=always --width=$COLUMNS --suppress-common-lines --side-by-side FreeRTOS-Kernel/generated queue/generated | less -r
  27 diff --color=always --width=$COLUMNS --suppress-common-lines --side-by-side FreeRTOS-Kernel/generated list/generated | less -r
  28 ```
  29
  30 Or generate a html report using `diff2html`:
  31
  32 ```
  33 diff -u FreeRTOS-Kernel/generated queue/generated | diff2html -i stdin
  34 diff -u FreeRTOS-Kernel/generated list/generated | diff2html -i stdin
  35 ```
  36
  37 The expectation is that the proofs make minimal changes to the original source
  38 implementation in the form of:
  39
  40   - VeriFast annotations `/*@...@*/` and `//*...`
  41   - Additional comments explaining the proof `/*...*/`
  42   - Flagged changes within `#if[n]def VERIFAST`