adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

riscv crefine: resolve FIXME 

the definition of objBits is in Haskell, so has to use pteBits instead of
pte_bits (not in scope)

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-06-08 17:56:02 +08:00
parent 65ae80c5ad
commit c14b2bb69a
1 changed files with 0 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
proof/crefine/RISCV64/Arch_C.thy
View File

@ -29,7 +29,6 @@ lemma objBits_InvalidPTE:
"objBits RISCV64_H.InvalidPTE = word_size_bits"
by (simp add: objBits_simps archObjSize_def word_size_bits_def bit_simps)
(* FIXME RISCV: should this be the real objBits_InvalidPTE? *)
lemma objBits_InvalidPTE_pte_bits:
"objBits RISCV64_H.InvalidPTE = pte_bits"
by (simp add: objBits_InvalidPTE bit_simps)