kth-step / HolBA

Binary analysis in HOL
Other
33 stars 20 forks source link

Additional opens in bir_m0_extrasScript #165

Closed didriklundberg closed 4 months ago

didriklundberg commented 4 months ago

Fixes the issues with Cortex-M0-lifting. The problem was that R_name from m0_stepTheory was treated as a free variable when the theory in question wasn't opened. Since this happened in a forward proof, it wasn't discovered during regular compilation.