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

c-parser: session qualified imports for parser tests

This commit is contained in:
Gerwin Klein 2018-06-12 18:30:47 +02:00
parent 5ae795c586
commit f2a8c3e07e
139 changed files with 139 additions and 139 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tools/c-parser/testfiles/ARM/asm_stmt.thy
View File

@ -10,7 +10,7 @@
theory asm_stmt
imports "../../CTranslation"
imports "CParser.CTranslation"
begin

2
tools/c-parser/testfiles/ARM/imports/MachineWords.thy
View File

@ -9,7 +9,7 @@
*)
theory MachineWords
imports "../../../CTranslation"
imports "CParser.CTranslation"
begin
type_synonym machine_word_len = "32"

2
tools/c-parser/testfiles/ARM_HYP/asm_stmt.thy
View File

@ -10,7 +10,7 @@
theory asm_stmt
imports "../../CTranslation"
imports "CParser.CTranslation"
begin

2
tools/c-parser/testfiles/ARM_HYP/imports/MachineWords.thy
View File

@ -9,7 +9,7 @@
*)
theory MachineWords
imports "../../../CTranslation"
imports "CParser.CTranslation"
begin
type_synonym machine_word_len = "32"

2
tools/c-parser/testfiles/X64/imports/MachineWords.thy
View File

@ -9,7 +9,7 @@
*)
theory MachineWords
imports "../../../CTranslation"
imports "CParser.CTranslation"
begin
type_synonym machine_word_len = "64"

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

@ -9,7 +9,7 @@
*)
theory analsignedoverflow
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare [[anal_integer_conversion=true]]

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

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

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

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

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory breakcontinue
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare sep_conj_ac [simp add]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory codetests
imports "../CTranslation"
imports "CParser.CTranslation"
begin
ML {* Context.>> (Context.map_theory (

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

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

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

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

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

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

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

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

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

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

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

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

2
tools/c-parser/testfiles/errors/addrlocal.thy
View File

@ -9,7 +9,7 @@
*)
theory addrlocal
imports "../../CTranslation"
imports "CParser.CTranslation"
begin
install_C_file "addrlocal.c";

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

@ -9,7 +9,7 @@
*)
theory extern_builtin
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare [[allow_underscore_idents=true]]

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

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

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

@ -9,7 +9,7 @@
*)
theory factorial
imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords"
begin
declare hrs_simps [simp add]

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

@ -9,7 +9,7 @@
*)
theory fncall
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare sep_conj_ac [simp add]

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

@ -9,7 +9,7 @@
*)
theory fnptr
imports "../CTranslation"
imports "CParser.CTranslation"
begin
ML {*

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

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

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

@ -9,7 +9,7 @@
*)
theory ghoststate1
imports "../CTranslation"
imports "CParser.CTranslation"
begin
install_C_file "simple_annotated_fn.c" [ghostty="nat \<Rightarrow> nat"]

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

@ -9,7 +9,7 @@
*)
theory ghoststate2
imports "../CTranslation"
imports "CParser.CTranslation"
begin
(*

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

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

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

@ -10,7 +10,7 @@
theory globals_in_record
imports
"../CTranslation"
"CParser.CTranslation"
begin
install_C_file "globals_in_record.c"

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

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

2
tools/c-parser/testfiles/globsall_addressed.thy.broken
View File

@ -8,7 +8,7 @@
* @TAG(NICTA_BSD)
*)
theory globsall_addressed
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare [[globals_all_addressed=true]]

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

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

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

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

2
tools/c-parser/testfiles/includes/test_locality.thy
View File

@ -9,7 +9,7 @@
*)
theory test_locality
imports "../../CTranslation"
imports "CParser.CTranslation"
begin
install_C_file "test_include2.h"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory jiraver150
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare [[use_anonymous_local_variables=true]]

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

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

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory jiraver307
imports "../CTranslation"
imports "CParser.CTranslation"
begin
install_C_file "jira ver307.c"

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

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

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

@ -9,7 +9,7 @@
*)
theory jiraver313
imports "../CTranslation"
imports "CParser.CTranslation"
begin
ML {* Feedback.verbosity_level := 6 *}

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

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

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory jiraver337
imports "../CTranslation"
imports "CParser.CTranslation"
begin

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

@ -9,7 +9,7 @@
*)
theory jiraver344
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare [[allow_underscore_idents=true]]

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory jiraver400
imports "../CTranslation"
imports "CParser.CTranslation"
begin
install_C_file "jiraver400.c" [machinety=bool,roots=[h,indep1]]

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

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

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

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

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory jiraver434
imports "../CTranslation"
imports "CParser.CTranslation"
begin

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory jiraver443
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare [[allow_underscore_idents=true]]

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

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

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

@ -9,7 +9,7 @@
*)
theory jiraver456
imports "../CTranslation"
imports "CParser.CTranslation"
begin

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

@ -9,7 +9,7 @@
*)
theory jiraver464
imports "../CTranslation"
imports "CParser.CTranslation"
begin
(* declare [[calculate_modifies_proofs=false]] *)

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

@ -9,7 +9,7 @@
*)
theory jiraver473
imports "../CTranslation"
imports "CParser.CTranslation"
begin
declare [[munge_info_fname="jiraver473.minfo"]]

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

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

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

@ -11,7 +11,7 @@
theory jiraver550
imports
"../../../lib/CTranslationNICTA"
"../../../lCParser.CTranslationNICTA"
begin
install_C_file "jiraver550.c"

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

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

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

@ -10,7 +10,7 @@
theory jiraver881
imports "../CTranslation"
imports "CParser.CTranslation"
begin

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

@ -9,7 +9,7 @@
*)
theory kmalloc
imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords"
begin
(* no proof here, just testing the parser *)

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

@ -9,7 +9,7 @@
*)
theory list_reverse
imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords"
begin
declare hrs_simps [simp add]

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

@ -9,7 +9,7 @@
*)
theory list_reverse_norm
imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords"
begin
declare sep_conj_ac [simp add]

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

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

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

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

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

@ -10,7 +10,7 @@
theory many_local_vars
imports
"../CTranslation"
"CParser.CTranslation"
begin
(* Avoid memory explosion caused by the C parser generating a huge record

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

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

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

@ -9,7 +9,7 @@
*)
theory modifies_speed
imports "../CTranslation"
imports "CParser.CTranslation"
begin
text {* Speed test for modifies proofs. *}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@ -9,7 +9,7 @@
*)
theory parse_include
imports "../CTranslation"
imports "CParser.CTranslation"
begin
new_C_include_dir "includes"

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

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

Some files were not shown because too many files have changed in this diff Show More