update references from/to moved crefine, parametrise over L4V_ARCH

2017-03-31 03:32:25 +11:00 · 2017-03-31 03:32:25 +11:00 · c41c7a97ca
parent f00bd94abe
commit c41c7a97ca
23 changed files with 34 additions and 34 deletions
--- a/lib/clib/Corres_C.thy
+++ b/lib/clib/Corres_C.thy
@ -11,7 +11,7 @@
 theory Corres_C
 imports 
 	CCorresLemmas 
-	"../../proof/crefine/SR_lemmas_C"
+	"../../proof/crefine/$L4V_ARCH/SR_lemmas_C"
 begin

 abbreviation
--- a/proof/ROOT
+++ b/proof/ROOT
@ -56,17 +56,17 @@ session AInvs = ASpec +

 session CRefineSyscall = CBaseRefine +
  theories
-    "crefine/Syscall_C"
+    "crefine/$L4V_ARCH/Syscall_C"

 session CRefine = CBaseRefine +
  theories
-    "crefine/Refine_C"
+    "crefine/$L4V_ARCH/Refine_C"

 session CBaseRefine = CSpec +
  theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
-    "crefine/Include_C"
+    "crefine/$L4V_ARCH/Include_C"
  theories
-    "crefine/Include_C"
+    "crefine/$L4V_ARCH/Include_C"


 (*
--- a/proof/crefine/ARM/ADT_C.thy
+++ b/proof/crefine/ARM/ADT_C.thy
@ -11,7 +11,7 @@
 theory ADT_C
 imports
  Schedule_C Retype_C Recycle_C
-  "../invariant-abstract/BCorres2_AI"
+  "../../invariant-abstract/BCorres2_AI"
 begin


--- a/proof/crefine/ARM/AutoCorres_C.thy
+++ b/proof/crefine/ARM/AutoCorres_C.thy
@ -14,10 +14,10 @@ text \<open>
  See AutoCorresTest for example usage.
 \<close>
 theory AutoCorres_C imports
-  "../../tools/autocorres/AutoCorres"
-  "../../tools/autocorres/L4VerifiedLinks"
-  "../../lib/clib/AutoCorresModifiesProofs"
-  "../../lib/clib/Corres_C"
+  "../../../tools/autocorres/AutoCorres"
+  "../../../tools/autocorres/L4VerifiedLinks"
+  "../../../lib/clib/AutoCorresModifiesProofs"
+  "../../../lib/clib/Corres_C"
 begin

 context kernel begin
@ -315,4 +315,4 @@ lemmas [terminates_trivial] =
  terminates.Skip
  terminates.Spec

-end
+end
--- a/proof/crefine/ARM/CLevityCatch.thy
+++ b/proof/crefine/ARM/CLevityCatch.thy
@ -11,8 +11,8 @@
 theory CLevityCatch
 imports
  Include_C
-  "../../lib/LemmaBucket_C"
-  "../../lib/LemmaBucket"
+  "../../../lib/LemmaBucket_C"
+  "../../../lib/LemmaBucket"
 begin

 context begin interpretation Arch . (*FIXME: arch_split*)
--- a/proof/crefine/ARM/CSpaceAcc_C.thy
+++ b/proof/crefine/ARM/CSpaceAcc_C.thy
@ -11,7 +11,7 @@
 (* collects lemmas common to the various CSpace branches *)

 theory CSpaceAcc_C
-imports "../refine/$L4V_ARCH/EmptyFail" "../../lib/clib/Ctac"
+imports "../../refine/$L4V_ARCH/EmptyFail" "../../../lib/clib/Ctac"
 begin

 (* For resolving schematics *) 
--- a/proof/crefine/ARM/CSpace_RAB_C.thy
+++ b/proof/crefine/ARM/CSpace_RAB_C.thy
@ -9,7 +9,7 @@
 *)

 theory CSpace_RAB_C
-imports CSpaceAcc_C "../../lib/clib/MonadicRewrite_C"
+imports CSpaceAcc_C "../../../lib/clib/MonadicRewrite_C"
 begin

 context kernel
--- a/proof/crefine/ARM/DetWP.thy
+++ b/proof/crefine/ARM/DetWP.thy
@ -9,7 +9,7 @@
 *)

 theory DetWP
-imports "../../lib/clib/DetWPLib" Include_C
+imports "../../../lib/clib/DetWPLib" Include_C
 begin

 context begin interpretation Arch . (*FIXME: arch_split*)
--- a/proof/crefine/ARM/Detype_C.thy
+++ b/proof/crefine/ARM/Detype_C.thy
@ -9,7 +9,7 @@
 *)

 theory Detype_C
-imports "../../lib/clib/Ctac" TcbQueue_C
+imports "../../../lib/clib/Ctac" TcbQueue_C
 begin

 lemma typ_clear_region_out:
--- a/proof/crefine/ARM/Fastpath_C.thy
+++ b/proof/crefine/ARM/Fastpath_C.thy
@ -14,8 +14,8 @@ imports
  SyscallArgs_C
  Delete_C
  Syscall_C
-  "../refine/$L4V_ARCH/RAB_FN"
-  "../../lib/clib/MonadicRewrite_C"
+  "../../refine/$L4V_ARCH/RAB_FN"
+  "../../../lib/clib/MonadicRewrite_C"
 begin

 context begin interpretation Arch . (*FIXME: arch_split*)
--- a/proof/crefine/ARM/Include_C.thy
+++ b/proof/crefine/ARM/Include_C.thy
@ -10,8 +10,8 @@

 theory Include_C
 imports
-  "../../spec/cspec/KernelInc_C"
-  "../refine/$L4V_ARCH/Refine"
+  "../../../spec/cspec/$L4V_ARCH/KernelInc_C"
+  "../../refine/$L4V_ARCH/Refine"
 begin

 end
--- a/proof/crefine/ARM/Invoke_C.thy
+++ b/proof/crefine/ARM/Invoke_C.thy
@ -9,7 +9,7 @@
 *)

 theory Invoke_C
-imports Recycle_C "../../lib/clib/MonadicRewrite_C"
+imports Recycle_C "../../../lib/clib/MonadicRewrite_C"
 begin

 context kernel_m
--- a/proof/crefine/ARM/IsolatedThreadAction.thy
+++ b/proof/crefine/ARM/IsolatedThreadAction.thy
@ -9,7 +9,7 @@
 *)

 theory IsolatedThreadAction
-imports "../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
+imports "../../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
 begin

 datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word"
--- a/proof/crefine/ARM/Machine_C.thy
+++ b/proof/crefine/ARM/Machine_C.thy
@ -15,7 +15,7 @@
 *)

 theory Machine_C
-imports "../../lib/clib/Ctac"
+imports "../../../lib/clib/Ctac"
 begin

 locale kernel_m = kernel +
--- a/proof/crefine/ARM/Move.thy
+++ b/proof/crefine/ARM/Move.thy
@ -11,7 +11,7 @@
 (* things that should be moved into first refinement *)

 theory Move
-imports "../refine/$L4V_ARCH/Refine"
+imports "../../refine/$L4V_ARCH/Refine"
 begin

 lemma finaliseCap_Reply:
--- a/proof/crefine/ARM/PSpace_C.thy
+++ b/proof/crefine/ARM/PSpace_C.thy
@ -9,7 +9,7 @@
 *)

 theory PSpace_C
-imports "../../lib/clib/Ctac"
+imports "../../../lib/clib/Ctac"
 begin

 context kernel begin
--- a/proof/crefine/ARM/Refine_C.thy
+++ b/proof/crefine/ARM/Refine_C.thy
@ -11,7 +11,7 @@
 chapter "Toplevel Refinement Statement"

 theory Refine_C
-imports Init_C Fastpath_C "../../lib/clib/CToCRefine"
+imports Init_C Fastpath_C "../../../lib/clib/CToCRefine"
 begin

 context begin interpretation Arch . (*FIXME: arch_split*)
--- a/proof/crefine/ARM/Refine_nondet_C.thy
+++ b/proof/crefine/ARM/Refine_nondet_C.thy
@ -13,7 +13,7 @@ header "Toplevel Refinement Statement for nondeterministic specification"
 theory Refine_nondet_C (* FIXME: broken *)
 imports
  Refine_C
-  "../invariant-abstract/BCorres2_AI"
+  "../../invariant-abstract/BCorres2_AI"
 begin

 definition (in state_rel)
--- a/proof/crefine/ARM/SR_lemmas_C.thy
+++ b/proof/crefine/ARM/SR_lemmas_C.thy
@ -11,7 +11,7 @@
 theory SR_lemmas_C
 imports
  StateRelation_C
-  "../refine/$L4V_ARCH/Invariants_H"
+  "../../refine/$L4V_ARCH/Invariants_H"
 begin

 context begin interpretation Arch . (*FIXME: arch_split*)
--- a/proof/crefine/ARM/TcbAcc_C.thy
+++ b/proof/crefine/ARM/TcbAcc_C.thy
@ -9,7 +9,7 @@
 *)

 theory TcbAcc_C
-imports "../../lib/clib/Ctac"
+imports "../../../lib/clib/Ctac"
 begin

 context kernel
--- a/proof/crefine/ARM/Wellformed_C.thy
+++ b/proof/crefine/ARM/Wellformed_C.thy
@ -13,9 +13,9 @@

 theory Wellformed_C
 imports
-  "../../lib/CTranslationNICTA"
+  "../../../lib/CTranslationNICTA"
  CLevityCatch
-  "../../spec/cspec/Substitute"
+  "../../../spec/cspec/Substitute"
 begin

 context begin interpretation Arch . (*FIXME: arch_split*)
--- a/proof/infoflow/ADT_IF_Refine_C.thy
+++ b/proof/infoflow/ADT_IF_Refine_C.thy
@ -10,7 +10,7 @@

 theory ADT_IF_Refine_C
 imports    
-    "ADT_IF_Refine" "../crefine/Refine_C"
+    "ADT_IF_Refine" "../crefine/$L4V_ARCH/Refine_C"
 begin

 context begin interpretation Arch . (*FIXME: arch_split*)
--- a/tools/autocorres/TestSEL4.thy
+++ b/tools/autocorres/TestSEL4.thy
@ -11,7 +11,7 @@
 theory TestSEL4
 imports
  AutoCorres
-  "../../spec/cspec/KernelInc_C"
+  "../../spec/cspec/$L4V_ARCH/KernelInc_C"
 begin

 (*