x64: crefine: added getFaultAddr_ccorres to machine assumptions

2017-10-05 15:55:55 +11:00 · 2017-10-05 15:55:55 +11:00 · 55b5f165b7
parent 72b1edaf96
commit 55b5f165b7
1 changed files with 5 additions and 0 deletions
--- a/proof/crefine/X64/Machine_C.thy
+++ b/proof/crefine/X64/Machine_C.thy
@ -20,6 +20,11 @@ begin

 (* FIXME x64: add all machine operations as required *)
 locale kernel_m = kernel +
+assumes getFaultAddr_ccorres:
+  "ccorres (op =) ret__unsigned_long_' \<top> UNIV []
+           (doMachineOp getFaultAddress)
+           (Call getFaultAddr_'proc)"
+
 assumes resetTimer_ccorres:
  "ccorres dc xfdc \<top> UNIV []
           (doMachineOp resetTimer)