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

c-parser: update to Isabelle2020 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-03-21 15:18:18 +08:00 committed by Gerwin Klein
parent f15fbf1e4b
commit 18428256f0
5 changed files with 8 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
tools/c-parser/Makefile
View File

@ -53,9 +53,9 @@ CParser: c-parser-deps
# then build it using Isabelle.
#
cparser_test: c-parser-deps testfiles/$(L4V_ARCH)/ROOT .FORCE
$(ISABELLE) build -d $(L4V_ROOT_DIR) -d testfiles/$(L4V_ARCH) -b -v CParserTest
$(ISABELLE) build -d $(L4V_ROOT_DIR) -d testfiles/$(L4V_ARCH) -v CParserTest
testfiles/$(L4V_ARCH)/ROOT: testfiles testfiles/*.c testfiles/*.thy ../../misc/scripts/gen_isabelle_root.py
python3 ../../misc/scripts/gen_isabelle_root.py -i testfiles -i testfiles/$(L4V_ARCH) -o testfiles/$(L4V_ARCH)/ROOT -s CParserTest -b CParser
python3 ../../misc/scripts/gen_isabelle_root.py -i testfiles -i testfiles/$(L4V_ARCH) -o testfiles/$(L4V_ARCH)/ROOT -s CParserTest -b CParser --dir ".." --dir "imports"
all_tests_$(L4V_ARCH).thy: testfiles testfiles/*.c ../../misc/scripts/gen_isabelle_root.py
python3 ../../misc/scripts/gen_isabelle_root.py -T -o $@ -b CParser -i testfiles -i testfiles/$(L4V_ARCH)

3
tools/c-parser/ROOT
View File

@ -17,5 +17,8 @@ session CParser = "Simpl-VCG" +
"HOL-Library"
"HOL-Word"
"Lib"
directories
"umm_heap"
"umm_heap/$L4V_ARCH"
theories
"CTranslation"

2
tools/c-parser/standalone-parser/basics.sml
View File

@ -80,6 +80,8 @@ infix mem
structure Library =
struct
type 'a ord = 'a * 'a -> order
val int_ord = Int.compare
val fast_string_ord = String.compare

2
tools/c-parser/testfiles/attributes.thy
View File

@ -5,7 +5,7 @@
*)
theory attributes
imports "../CTranslation"
imports "CParser.CTranslation"
begin
install_C_file "attributes.c"

4
tools/c-parser/umm_heap/TypHeap.thy
View File

@ -854,12 +854,8 @@ proof -
apply(subgoal_tac "k = 0")
prefer 2
apply(rule ccontr, simp)
apply(drule order_le_imp_less_or_eq[where x=t])
apply clarsimp
apply(simp add: typ_slice_0_prefix)
apply simp
apply(drule order_le_imp_less_or_eq[where x=t])
apply clarsimp
(* given by the fd_tag_consistent condition *)
apply(drule typ_slice_True_prefix)
apply(clarsimp simp: field_of_def)