Skip to content

Fixing modules for switching

Alex Loitzlrequested to merge
fixed_modules into master

This commit contains the following major changes

  • Fixing the Module (Π) for switching
  • Adding the necessary definitions/lemmas to the linking module, abstracting over the environment using ghost variables
  • Add a PoC proof of a recursive rec program linking with a spec program
  • Some new Notations
  • Rework of the memmove example -> Motivates a more general treating of external calls (Wip)
  • Auxiliary lemmas

Merge request reports