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

lib+proof+tools: move LemmaBucket_C into CParser 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-01-24 14:55:01 +11:00
parent cb34fc3c4c
commit 2d2cadb86b
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
12 changed files with 14 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
lib/ROOT
View File

@ -85,7 +85,6 @@ session CLib (lib) in clib = CParser +
Simpl_Rewrite Simpl_Rewrite
MonadicRewrite_C MonadicRewrite_C
CTranslationNICTA CTranslationNICTA
LemmaBucket_C
SIMPL_Lemmas SIMPL_Lemmas
SimplRewrite SimplRewrite
BitFieldProofsLib BitFieldProofsLib

6
lib/clib/Corres_UL_C.thy
View File

@ -11,9 +11,9 @@
theory Corres_UL_C theory Corres_UL_C
imports imports
"LemmaBucket_C" CParser.LemmaBucket_C
"Lib.LemmaBucket" Lib.LemmaBucket
"SIMPL_Lemmas" SIMPL_Lemmas
begin begin
declare word_neq_0_conv [simp del] declare word_neq_0_conv [simp del]

2
lib/test/ShowTypes_Test.thy
View File

@ -7,7 +7,7 @@
theory ShowTypes_Test theory ShowTypes_Test
imports imports
Lib.ShowTypes Lib.ShowTypes
CLib.LemmaBucket_C CParser.LemmaBucket_C
CParser.CTranslation CParser.CTranslation
begin begin

2
proof/crefine/ARM/CLevityCatch.thy
View File

@ -8,7 +8,7 @@ theory CLevityCatch
imports imports
"CBaseRefine.Include_C" "CBaseRefine.Include_C"
ArchMove_C ArchMove_C
"CLib.LemmaBucket_C" "CParser.LemmaBucket_C"
"Lib.LemmaBucket" "Lib.LemmaBucket"
begin begin

2
proof/crefine/ARM_HYP/CLevityCatch.thy
View File

@ -8,7 +8,7 @@ theory CLevityCatch
imports imports
"CBaseRefine.Include_C" "CBaseRefine.Include_C"
ArchMove_C ArchMove_C
"CLib.LemmaBucket_C" "CParser.LemmaBucket_C"
"Lib.LemmaBucket" "Lib.LemmaBucket"
begin begin

2
proof/crefine/RISCV64/CLevityCatch.thy
View File

@ -8,7 +8,7 @@ theory CLevityCatch
imports imports
"CBaseRefine.Include_C" "CBaseRefine.Include_C"
ArchMove_C ArchMove_C
"CLib.LemmaBucket_C" "CParser.LemmaBucket_C"
"Lib.LemmaBucket" "Lib.LemmaBucket"
begin begin

2
proof/crefine/X64/CLevityCatch.thy
View File

@ -8,7 +8,7 @@ theory CLevityCatch
imports imports
"CBaseRefine.Include_C" "CBaseRefine.Include_C"
ArchMove_C ArchMove_C
"CLib.LemmaBucket_C" "CParser.LemmaBucket_C"
"Lib.LemmaBucket" "Lib.LemmaBucket"
begin begin

2
tools/asmrefine/FieldAccessors.thy
View File

@ -7,7 +7,7 @@
theory FieldAccessors theory FieldAccessors
imports imports
Lib.Lib Lib.Lib
CLib.LemmaBucket_C CParser.LemmaBucket_C
begin begin
lemma h_val_mono: lemma h_val_mono:

2
tools/asmrefine/GraphRefine.thy
View File

@ -10,7 +10,7 @@ imports
TailrecPre TailrecPre
GraphLangLemmas GraphLangLemmas
Lib.Lib Lib.Lib
"CLib.LemmaBucket_C" "CParser.LemmaBucket_C"
ExtraSpecs ExtraSpecs
begin begin

2
tools/autocorres/HeapLift.thy
View File

@ -11,7 +11,7 @@ imports
L2Defs L2Defs
ExecConcrete ExecConcrete
AbstractArrays AbstractArrays
"CLib.LemmaBucket_C" "CParser.LemmaBucket_C"
begin begin
definition "L2Tcorres st A C = corresXF st (\<lambda>r _. r) (\<lambda>r _. r) \<top> A C" definition "L2Tcorres st A C = corresXF st (\<lambda>r _. r) (\<lambda>r _. r) \<top> A C"

2
lib/clib/LemmaBucket_C.thy → tools/c-parser/LemmaBucket_C.thy
View File

@ -7,7 +7,7 @@
theory LemmaBucket_C theory LemmaBucket_C
imports imports
Basics.CLib Basics.CLib
CParser.TypHeapLib TypHeapLib
begin begin
lemma Ptr_not_null_pointer_not_zero: "(Ptr p \<noteq> NULL)=(p\<noteq>0)" lemma Ptr_not_null_pointer_not_zero: "(Ptr p \<noteq> NULL)=(p\<noteq>0)"

3
tools/c-parser/ROOT
View File

@ -16,9 +16,10 @@ session CParser = "Simpl-VCG" +
sessions sessions
"HOL-Library" "HOL-Library"
"ML_Utils" "ML_Utils"
"Basics"
directories directories
"umm_heap" "umm_heap"
"umm_heap/$L4V_ARCH" "umm_heap/$L4V_ARCH"
theories theories
"CTranslation" "CTranslation"
"TypHeapLib" "LemmaBucket_C"