Isabelle2018 c-parser: declare external files

2018-06-24 13:15:33 +02:00 · 2018-06-24 13:15:33 +02:00 · 4dc3ffb1ba
parent 86bad831e2
commit 4dc3ffb1ba
131 changed files with 191 additions and 50 deletions
--- a/tools/c-parser/testfiles/ARM/asm_stmt.thy
+++ b/tools/c-parser/testfiles/ARM/asm_stmt.thy
@ -19,6 +19,7 @@ declare [[populate_globals=true]]
 typedecl machine_state
 typedecl cghost_state

+external_file "asm_stmt.c"
 install_C_file "asm_stmt.c"
  [machinety=machine_state, ghostty=cghost_state]

--- a/tools/c-parser/testfiles/ARM_HYP/asm_stmt.thy
+++ b/tools/c-parser/testfiles/ARM_HYP/asm_stmt.thy
@ -19,6 +19,7 @@ declare [[populate_globals=true]]
 typedecl machine_state
 typedecl cghost_state

+external_file "asm_stmt.c"
 install_C_file "asm_stmt.c"
  [machinety=machine_state, ghostty=cghost_state]

--- a/tools/c-parser/testfiles/analsignedoverflow.thy
+++ b/tools/c-parser/testfiles/analsignedoverflow.thy
@ -12,6 +12,8 @@ theory analsignedoverflow
 imports "CParser.CTranslation"
 begin

+external_file "analsignedoverflow.c"
+
 declare [[anal_integer_conversion=true]]
 install_C_file "analsignedoverflow.c"

--- a/tools/c-parser/testfiles/array_of_ptr.thy
+++ b/tools/c-parser/testfiles/array_of_ptr.thy
@ -12,6 +12,7 @@ theory array_of_ptr
 imports "CParser.CTranslation"
 begin

+external_file "array_of_ptr.c"
 install_C_file "array_of_ptr.c"

 print_locale array_of_ptr_global_addresses
--- a/tools/c-parser/testfiles/arrays.thy
+++ b/tools/c-parser/testfiles/arrays.thy
@ -12,6 +12,7 @@ theory arrays
 imports "CParser.CTranslation"
 begin

+external_file "arrays.c"
 install_C_file "arrays.c"

 context arrays_global_addresses
--- a/tools/c-parser/testfiles/basic_char.thy
+++ b/tools/c-parser/testfiles/basic_char.thy
@ -12,6 +12,7 @@ theory basic_char
 imports "CParser.CTranslation"
 begin

+external_file "basic_char.c"
 install_C_file "basic_char.c"

 context basic_char
--- a/tools/c-parser/testfiles/bigstruct.thy
+++ b/tools/c-parser/testfiles/bigstruct.thy
@ -12,6 +12,7 @@ theory bigstruct
 imports "CParser.CTranslation"
 begin

+external_file "bigstruct.c"
 install_C_file "bigstruct.c"

 end
--- a/tools/c-parser/testfiles/breakcontinue.thy
+++ b/tools/c-parser/testfiles/breakcontinue.thy
@ -13,6 +13,8 @@ imports "CParser.CTranslation"
 begin

 declare sep_conj_ac [simp add]
+
+external_file "breakcontinue.c"
 install_C_file "breakcontinue.c"

 context breakcontinue_global_addresses
--- a/tools/c-parser/testfiles/bug20060707.thy
+++ b/tools/c-parser/testfiles/bug20060707.thy
@ -12,6 +12,7 @@ theory bug20060707
 imports "CParser.CTranslation"
 begin

+external_file "bug20060707.c"
 install_C_file "bug20060707.c"

  print_locale bug20060707_global_addresses
--- a/tools/c-parser/testfiles/bug_mvt20110302.thy
+++ b/tools/c-parser/testfiles/bug_mvt20110302.thy
@ -12,6 +12,7 @@ theory bug_mvt20110302
 imports "CParser.CTranslation"
 begin

+external_file "bug_mvt20110302.c"
 install_C_file "bug_mvt20110302.c"

 context bug_mvt20110302
--- a/tools/c-parser/testfiles/bugzilla180.thy
+++ b/tools/c-parser/testfiles/bugzilla180.thy
@ -12,6 +12,7 @@ theory bugzilla180
 imports "CParser.CTranslation"
 begin

+external_file "bugzilla180.c"
 install_C_file "bugzilla180.c"

 context "bugzilla180"
--- a/tools/c-parser/testfiles/bugzilla181.thy
+++ b/tools/c-parser/testfiles/bugzilla181.thy
@ -12,6 +12,7 @@ theory bugzilla181
 imports "CParser.CTranslation"
 begin

+external_file "bugzilla181.c"
 install_C_file "bugzilla181.c"

 end
--- a/tools/c-parser/testfiles/bugzilla182.thy
+++ b/tools/c-parser/testfiles/bugzilla182.thy
@ -12,6 +12,7 @@ theory bugzilla182
 imports "CParser.CTranslation"
 begin

+external_file "bugzilla182.c"
 install_C_file "bugzilla182.c"

 end
--- a/tools/c-parser/testfiles/builtins.thy
+++ b/tools/c-parser/testfiles/builtins.thy
@ -12,6 +12,7 @@ theory builtins
 imports "CParser.CTranslation"
 begin

+external_file "builtins.c"
 install_C_file "builtins.c"

 context builtins
--- a/tools/c-parser/testfiles/charlit.thy
+++ b/tools/c-parser/testfiles/charlit.thy
@ -12,6 +12,7 @@ theory charlit
 imports "CParser.CTranslation"
 begin

+external_file "charlit.c"
 install_C_file "charlit.c"

 context charlit
--- a/tools/c-parser/testfiles/dc_20081211.thy
+++ b/tools/c-parser/testfiles/dc_20081211.thy
@ -12,6 +12,7 @@ theory dc_20081211
 imports "CParser.CTranslation"
 begin

+external_file "dc_20081211.c"
 install_C_file "dc_20081211.c"

 declare [[show_types]]
--- a/tools/c-parser/testfiles/dc_embbug.thy
+++ b/tools/c-parser/testfiles/dc_embbug.thy
@ -12,6 +12,7 @@ theory dc_embbug
 imports "CParser.CTranslation"
 begin

+external_file "dc_embbug.c"
 install_C_file "dc_embbug.c"

 thm dc_embbug_global_addresses.f_body_def
--- a/tools/c-parser/testfiles/decl_only.thy
+++ b/tools/c-parser/testfiles/decl_only.thy
@ -12,6 +12,7 @@ theory decl_only
 imports "CParser.CTranslation"
 begin

+external_file "decl_only.c"
 install_C_file "decl_only.c"

 print_locale decl_only_global_addresses
--- a/tools/c-parser/testfiles/dont_translate.thy
+++ b/tools/c-parser/testfiles/dont_translate.thy
@ -12,6 +12,7 @@ theory dont_translate
 imports "CParser.CTranslation"
 begin

+external_file "dont_translate.c"
 install_C_file "dont_translate.c"

 context dont_translate
--- a/tools/c-parser/testfiles/dupthms.thy
+++ b/tools/c-parser/testfiles/dupthms.thy
@ -12,6 +12,7 @@ theory dupthms
 imports "CParser.CTranslation"
 begin

+external_file "dupthms.c"
 install_C_file "dupthms.c"

 end
--- a/tools/c-parser/testfiles/emptystmt.thy
+++ b/tools/c-parser/testfiles/emptystmt.thy
@ -12,6 +12,7 @@ theory emptystmt
 imports "CParser.CTranslation"
 begin

+external_file "emptystmt.c"
 install_C_file "emptystmt.c"

 context emptystmt
--- a/tools/c-parser/testfiles/errors/addrlocal.thy
+++ b/tools/c-parser/testfiles/errors/addrlocal.thy
@ -12,6 +12,7 @@ theory addrlocal
 imports "CParser.CTranslation"
 begin

+external_file "addrlocal.c";
 install_C_file "addrlocal.c";

 end
--- a/tools/c-parser/testfiles/extern_builtin.thy
+++ b/tools/c-parser/testfiles/extern_builtin.thy
@ -14,6 +14,7 @@ begin

 declare [[allow_underscore_idents=true]]

+external_file "extern_builtin.c"
 install_C_file "extern_builtin.c"

 end
--- a/tools/c-parser/testfiles/extern_dups.thy
+++ b/tools/c-parser/testfiles/extern_dups.thy
@ -12,6 +12,7 @@ theory extern_dups
 imports "CParser.CTranslation"
 begin

+external_file "extern_dups.c"
 install_C_file "extern_dups.c"

 print_locale extern_dups_global_addresses
--- a/tools/c-parser/testfiles/factorial.thy
+++ b/tools/c-parser/testfiles/factorial.thy
@ -98,6 +98,7 @@ lemma sep_fac_list_points:
    apply simp+
  done

+external_file "factorial.c"
 install_C_file memsafe "factorial.c"

 thm factorial_global_addresses.factorial_body_def
--- a/tools/c-parser/testfiles/fncall.thy
+++ b/tools/c-parser/testfiles/fncall.thy
@ -26,6 +26,7 @@ val ast = IsarInstall.get_Csyntax @{theory} "fncall.c"

 *}

+external_file "fncall.c"
 install_C_file "fncall.c"

 context fncall
--- a/tools/c-parser/testfiles/fnptr.thy
+++ b/tools/c-parser/testfiles/fnptr.thy
@ -16,6 +16,7 @@ ML {*
  IsarInstall.install_C_file ((((NONE,NONE),NONE),"fnptr.c"),NONE) @{theory}
 *}

+external_file "fnptr.c"
 install_C_file "fnptr.c"

 context fnptr_global_addresses
--- a/tools/c-parser/testfiles/gcc_attribs.thy
+++ b/tools/c-parser/testfiles/gcc_attribs.thy
@ -12,6 +12,7 @@ theory gcc_attribs
 imports "CParser.CTranslation"
 begin

+external_file "gcc_attribs.c"
 install_C_file "gcc_attribs.c"

 context gcc_attribs
--- a/tools/c-parser/testfiles/ghoststate1.thy
+++ b/tools/c-parser/testfiles/ghoststate1.thy
@ -12,6 +12,7 @@ theory ghoststate1
 imports "CParser.CTranslation"
 begin

+external_file "simple_annotated_fn.c"
 install_C_file "simple_annotated_fn.c" [ghostty="nat \<Rightarrow> nat"]

 (* demonstrates existence of ghost'state global variable of appropriate type *)
--- a/tools/c-parser/testfiles/ghoststate2.thy
+++ b/tools/c-parser/testfiles/ghoststate2.thy
@ -23,6 +23,7 @@ IsarInstall.install_C_file ((((NONE, NONE), NONE), "ghoststate2.c"),
 *}
 *)

+external_file "ghoststate2.c"
 install_C_file "ghoststate2.c" [ghostty="nat"]

 context ghoststate2
--- a/tools/c-parser/testfiles/globals_fn.thy
+++ b/tools/c-parser/testfiles/globals_fn.thy
@ -12,6 +12,7 @@ theory globals_fn
 imports "CParser.CTranslation"
 begin

+external_file "globals_fn.c"
 install_C_file "globals_fn.c"

 print_locale globals_fn_global_addresses
--- a/tools/c-parser/testfiles/globals_in_record.thy
+++ b/tools/c-parser/testfiles/globals_in_record.thy
@ -13,6 +13,7 @@ imports
  "CParser.CTranslation"
 begin

+external_file "globals_in_record.c"
 install_C_file "globals_in_record.c"

 context globals_in_record begin
--- a/tools/c-parser/testfiles/globinits.thy
+++ b/tools/c-parser/testfiles/globinits.thy
@ -12,6 +12,7 @@ theory globinits
 imports "CParser.CTranslation"
 begin

+external_file "globinits.c"
 install_C_file "globinits.c"

 context globinits
--- a/tools/c-parser/testfiles/guard_while.thy
+++ b/tools/c-parser/testfiles/guard_while.thy
@ -12,6 +12,7 @@ theory guard_while
 imports "CParser.CTranslation"
 begin

+external_file "guard_while.c"
 install_C_file "guard_while.c"

 print_locale guard_while_global_addresses
--- a/tools/c-parser/testfiles/hexliteral.thy
+++ b/tools/c-parser/testfiles/hexliteral.thy
@ -12,6 +12,7 @@ theory hexliteral
 imports "CParser.CTranslation"
 begin

+external_file "hexliteral.c"
 install_C_file "hexliteral.c"

 thm hexliteral_global_addresses.f_body_def
--- a/tools/c-parser/testfiles/includes/test_locality.thy
+++ b/tools/c-parser/testfiles/includes/test_locality.thy
@ -12,6 +12,7 @@ theory test_locality
 imports "CParser.CTranslation"
 begin

+external_file "test_include2.h"
 install_C_file "test_include2.h"

 end;
--- a/tools/c-parser/testfiles/initialised_decls.thy
+++ b/tools/c-parser/testfiles/initialised_decls.thy
@ -12,6 +12,7 @@ theory initialised_decls
 imports "CParser.CTranslation"
 begin

+external_file "initialised_decls.c"
 install_C_file "initialised_decls.c"

 context initialised_decls_global_addresses
--- a/tools/c-parser/testfiles/inner_fncalls.thy
+++ b/tools/c-parser/testfiles/inner_fncalls.thy
@ -12,6 +12,7 @@ theory inner_fncalls
 imports "CParser.CTranslation"
 begin

+external_file "inner_fncalls.c"
 install_C_file "inner_fncalls.c"

 print_locale inner_fncalls_global_addresses
--- a/tools/c-parser/testfiles/int_promotion.thy
+++ b/tools/c-parser/testfiles/int_promotion.thy
@ -12,6 +12,7 @@ theory int_promotion
 imports "CParser.CTranslation"
 begin

+external_file "int_promotion.c"
 install_C_file "int_promotion.c"

  context int_promotion
--- a/tools/c-parser/testfiles/isa2014.thy
+++ b/tools/c-parser/testfiles/isa2014.thy
@ -12,9 +12,10 @@ theory isa2014
  imports "CParser.CTranslation"
 begin

-  install_C_file "isa2014.c"
+external_file "isa2014.c"
+install_C_file "isa2014.c"

-  print_locale isa2014_global_addresses
+print_locale isa2014_global_addresses

 context isa2014
 begin
--- a/tools/c-parser/testfiles/jiraver039.thy
+++ b/tools/c-parser/testfiles/jiraver039.thy
@ -12,6 +12,7 @@ theory jiraver039
 imports "CParser.CTranslation"
 begin

+external_file "jiraver039.c"
 install_C_file "jiraver039.c"

 context jiraver039
--- a/tools/c-parser/testfiles/jiraver092.thy
+++ b/tools/c-parser/testfiles/jiraver092.thy
@ -12,6 +12,7 @@ theory jiraver092
 imports "CParser.CTranslation"
 begin

+external_file "jiraver092.c"
 install_C_file "jiraver092.c"

 context jiraver092
--- a/tools/c-parser/testfiles/jiraver105.thy
+++ b/tools/c-parser/testfiles/jiraver105.thy
@ -12,6 +12,7 @@ theory jiraver105
 imports "CParser.CTranslation"
 begin

+external_file "jiraver105.c"
 install_C_file "jiraver105.c"

 end
--- a/tools/c-parser/testfiles/jiraver110.thy
+++ b/tools/c-parser/testfiles/jiraver110.thy
@ -12,6 +12,7 @@ theory jiraver110
 imports "CParser.CTranslation"
 begin

+external_file "jiraver110.c"
 install_C_file "jiraver110.c"

 context jiraver110
--- a/tools/c-parser/testfiles/jiraver150.thy
+++ b/tools/c-parser/testfiles/jiraver150.thy
@ -12,6 +12,8 @@ theory jiraver150
 imports "CParser.CTranslation"
 begin

+external_file "jiraver150.c"
+
 declare [[use_anonymous_local_variables=true]]
  install_C_file "jiraver150.c"

--- a/tools/c-parser/testfiles/jiraver224.thy
+++ b/tools/c-parser/testfiles/jiraver224.thy
@ -12,6 +12,7 @@ theory jiraver224
 imports "CParser.CTranslation"
 begin

+external_file "jiraver224.c"
 install_C_file "jiraver224.c"

 context jiraver224
--- a/tools/c-parser/testfiles/jiraver253.thy
+++ b/tools/c-parser/testfiles/jiraver253.thy
@ -12,6 +12,7 @@ theory jiraver253
 imports "CParser.CTranslation"
 begin

+external_file "jiraver253.c"
 install_C_file "jiraver253.c"

 context jiraver253
--- a/tools/c-parser/testfiles/jiraver254.thy
+++ b/tools/c-parser/testfiles/jiraver254.thy
@ -12,6 +12,7 @@ theory jiraver254
 imports "CParser.CTranslation"
 begin

+external_file "jiraver254.c"
 install_C_file "jiraver254.c"

 context jiraver254
--- a/tools/c-parser/testfiles/jiraver307.thy
+++ b/tools/c-parser/testfiles/jiraver307.thy
@ -12,6 +12,7 @@ theory jiraver307
  imports "CParser.CTranslation"
 begin

+external_file "jira ver307.c"
 install_C_file "jira ver307.c"

 context "jira ver307"
--- a/tools/c-parser/testfiles/jiraver310.thy
+++ b/tools/c-parser/testfiles/jiraver310.thy
@ -12,20 +12,21 @@ theory jiraver310
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver310.c"
+external_file "jiraver310.c"
+install_C_file "jiraver310.c"

-  context jiraver310
-  begin
+context jiraver310
+begin

-    thm f_body_def
-    thm g_body_def
+  thm f_body_def
+  thm g_body_def

-    lemma "g_body = X"
-    apply (simp add: g_body_def)
-    oops
+  lemma "g_body = X"
+  apply (simp add: g_body_def)
+  oops

-    thm h_body_def
+  thm h_body_def

-  end (* context *)
+end (* context *)

 end (* theory *)
--- a/tools/c-parser/testfiles/jiraver313.thy
+++ b/tools/c-parser/testfiles/jiraver313.thy
@ -16,6 +16,7 @@ ML {* Feedback.verbosity_level := 6 *}

 declare [[calculate_modifies_proofs = false ]]

+external_file "jiraver313.c"
 install_C_file memsafe "jiraver313.c"

 ML {*
--- a/tools/c-parser/testfiles/jiraver315.thy
+++ b/tools/c-parser/testfiles/jiraver315.thy
@ -12,6 +12,7 @@ theory jiraver315
  imports "CParser.CTranslation"
 begin

+external_file "jiraver315.c"
 install_C_file "jiraver315.c"

 context jiraver315
--- a/tools/c-parser/testfiles/jiraver332.thy
+++ b/tools/c-parser/testfiles/jiraver332.thy
@ -12,13 +12,14 @@ theory jiraver332
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver332.c"
+external_file "jiraver332.c"
+install_C_file "jiraver332.c"

-  context jiraver332
-  begin
+context jiraver332
+begin

-    thm f_body_def
-
-  end
+  thm f_body_def
+
+end

 end
--- a/tools/c-parser/testfiles/jiraver336.thy
+++ b/tools/c-parser/testfiles/jiraver336.thy
@ -12,7 +12,8 @@ theory jiraver336
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver336.c"
+external_file "jiraver336.c"
+install_C_file "jiraver336.c"

 context jiraver336
 begin
--- a/tools/c-parser/testfiles/jiraver337.thy
+++ b/tools/c-parser/testfiles/jiraver337.thy
@ -12,13 +12,14 @@ theory jiraver337
  imports "CParser.CTranslation"
 begin

+declare [[cpp_path=""]]

-  declare [[cpp_path=""]]
-  install_C_file "jiraver337.c"
+external_file "jiraver337.c"
+install_C_file "jiraver337.c"

-  context jiraver337
-  begin
-    thm f_body_def
-  end (* context *)
+context jiraver337
+begin
+  thm f_body_def
+end (* context *)

 end
--- a/tools/c-parser/testfiles/jiraver344.thy
+++ b/tools/c-parser/testfiles/jiraver344.thy
@ -12,8 +12,9 @@ theory jiraver344
  imports "CParser.CTranslation"
 begin

+external_file "jiraver344.c"
+
 declare [[allow_underscore_idents=true]]
 install_C_file "jiraver344.c"

-
 end
--- a/tools/c-parser/testfiles/jiraver345.thy
+++ b/tools/c-parser/testfiles/jiraver345.thy
@ -12,7 +12,8 @@ theory jiraver345
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver345.c"
+external_file "jiraver345.c"
+install_C_file "jiraver345.c"

 context jiraver345
 begin
--- a/tools/c-parser/testfiles/jiraver384.thy
+++ b/tools/c-parser/testfiles/jiraver384.thy
@ -12,6 +12,7 @@ theory jiraver384
  imports "CParser.CTranslation"
 begin

+  external_file "jiraver384.c"
  install_C_file "jiraver384.c"

  context jiraver384
--- a/tools/c-parser/testfiles/jiraver400.thy
+++ b/tools/c-parser/testfiles/jiraver400.thy
@ -12,7 +12,8 @@ theory jiraver400
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver400.c" [machinety=bool,roots=[h,indep1]]
+external_file "jiraver400.c"
+install_C_file "jiraver400.c" [machinety=bool,roots=[h,indep1]]

 context jiraver400
 begin
--- a/tools/c-parser/testfiles/jiraver422.thy
+++ b/tools/c-parser/testfiles/jiraver422.thy
@ -12,13 +12,14 @@ theory jiraver422
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver422.c"
+external_file "jiraver422.c"
+install_C_file "jiraver422.c"

-  context jiraver422
-  begin
+context jiraver422
+begin

-    thm qux_body_def
-
-  end
+  thm qux_body_def
+
+end

 end
--- a/tools/c-parser/testfiles/jiraver426.thy
+++ b/tools/c-parser/testfiles/jiraver426.thy
@ -12,6 +12,7 @@ theory jiraver426
  imports "CParser.CTranslation"
 begin

+external_file "jiraver426.c"
 install_C_file "jiraver426.c"

 context jiraver426
--- a/tools/c-parser/testfiles/jiraver429.thy
+++ b/tools/c-parser/testfiles/jiraver429.thy
@ -12,6 +12,7 @@ theory jiraver429
  imports "CParser.CTranslation"
 begin

+external_file "jiraver429.c"
  install_C_file "jiraver429.c"

  context jiraver429
--- a/tools/c-parser/testfiles/jiraver432.thy
+++ b/tools/c-parser/testfiles/jiraver432.thy
@ -12,6 +12,7 @@ theory jiraver432
  imports "CParser.CTranslation"
 begin

+external_file "jiraver432.c"
 install_C_file "jiraver432.c"

 thm AnonStruct1'_size
--- a/tools/c-parser/testfiles/jiraver434.thy
+++ b/tools/c-parser/testfiles/jiraver434.thy
@ -13,6 +13,7 @@ theory jiraver434

 begin

+external_file "jiraver434.c"
 install_C_file "jiraver434.c"

 context jiraver434
--- a/tools/c-parser/testfiles/jiraver439.thy
+++ b/tools/c-parser/testfiles/jiraver439.thy
@ -12,7 +12,8 @@ theory jiraver439
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver439.c"
+external_file "jiraver439.c"
+install_C_file "jiraver439.c"

 context jiraver439
 begin
--- a/tools/c-parser/testfiles/jiraver440.thy
+++ b/tools/c-parser/testfiles/jiraver440.thy
@ -12,18 +12,19 @@ theory jiraver440
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver440.c"
+external_file "jiraver440.c"
+install_C_file "jiraver440.c"

-  context jiraver440
-  begin
+context jiraver440
+begin

-  thm f_body_def
-  thm g_body_def
+thm f_body_def
+thm g_body_def

-  lemma "f_body = g_body"
-  by (simp add: f_body_def g_body_def)
+lemma "f_body = g_body"
+by (simp add: f_body_def g_body_def)


-  end
-
+end
+
 end
--- a/tools/c-parser/testfiles/jiraver443.thy
+++ b/tools/c-parser/testfiles/jiraver443.thy
@ -12,6 +12,8 @@ theory jiraver443
  imports "CParser.CTranslation"
 begin

+  external_file "jiraver443.c"
+
  declare [[allow_underscore_idents=true]]
  (* 3014 lines, with  78 globals:  works ;
     3498 lines, with  96 globals:  works ;
--- a/tools/c-parser/testfiles/jiraver443a.thy
+++ b/tools/c-parser/testfiles/jiraver443a.thy
@ -12,7 +12,8 @@ theory jiraver443a
  imports "CParser.CTranslation"
 begin

-  install_C_file "jiraver443a.c"
+external_file "jiraver443a.c"
+install_C_file "jiraver443a.c"

 context jiraver443a
 begin
--- a/tools/c-parser/testfiles/jiraver456.thy
+++ b/tools/c-parser/testfiles/jiraver456.thy
@ -13,6 +13,7 @@ theory jiraver456

 begin

+external_file "jiraver456.c"
 install_C_file "jiraver456.c"

 context jiraver456
--- a/tools/c-parser/testfiles/jiraver464.thy
+++ b/tools/c-parser/testfiles/jiraver464.thy
@ -13,6 +13,8 @@ theory jiraver464
 begin

 (* declare [[calculate_modifies_proofs=false]] *)
+
+external_file "jiraver464.c"
 install_C_file "jiraver464.c"

 print_locale f_spec
--- a/tools/c-parser/testfiles/jiraver473.thy
+++ b/tools/c-parser/testfiles/jiraver473.thy
@ -12,7 +12,9 @@ theory jiraver473
  imports "CParser.CTranslation"
 begin

-  declare [[munge_info_fname="jiraver473.minfo"]]
-  install_C_file "jiraver473.c"
+declare [[munge_info_fname="jiraver473.minfo"]]
+
+external_file "jiraver473.c"
+install_C_file "jiraver473.c"

 end
--- a/tools/c-parser/testfiles/jiraver54.thy
+++ b/tools/c-parser/testfiles/jiraver54.thy
@ -12,6 +12,7 @@ theory jiraver54
 imports "CParser.CTranslation"
 begin

+external_file "jiraver54.c"
 install_C_file "jiraver54.c"

 context jiraver54
--- a/tools/c-parser/testfiles/jiraver550.thy
+++ b/tools/c-parser/testfiles/jiraver550.thy
@ -14,6 +14,7 @@ imports
  "CParser.CTranslation"
 begin

+external_file "jiraver550.c"
 install_C_file "jiraver550.c"


--- a/tools/c-parser/testfiles/jiraver808.thy
+++ b/tools/c-parser/testfiles/jiraver808.thy
@ -12,7 +12,8 @@ theory jiraver808
  imports "CParser.CTranslation"
 begin

- install_C_file "jiraver808.c"
+external_file "jiraver808.c"
+install_C_file "jiraver808.c"

 context jiraver808
 begin
--- a/tools/c-parser/testfiles/jiraver881.thy
+++ b/tools/c-parser/testfiles/jiraver881.thy
@ -14,6 +14,7 @@ imports "CParser.CTranslation"

 begin

+external_file "jiraver881.c"
 install_C_file "jiraver881.c"

 context jiraver881 begin
--- a/tools/c-parser/testfiles/kmalloc.thy
+++ b/tools/c-parser/testfiles/kmalloc.thy
@ -18,6 +18,7 @@ consts
  KMC :: word32
  ptr_retyps :: "nat \<Rightarrow> machine_word \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc"

+external_file "kmalloc.c"
 install_C_file "kmalloc.c"

 context kmalloc begin
--- a/tools/c-parser/testfiles/list_reverse.thy
+++ b/tools/c-parser/testfiles/list_reverse.thy
@ -29,6 +29,7 @@ lemma list_empty [simp]:
 declare sep_conj_com [simp del]
 declare sep_conj_left_com [simp del]

+external_file "list_reverse.c"
 install_C_file memsafe "list_reverse.c"

 thm list_reverse_global_addresses.reverse_body_def
--- a/tools/c-parser/testfiles/list_reverse_norm.thy
+++ b/tools/c-parser/testfiles/list_reverse_norm.thy
@ -84,6 +84,7 @@ lemma list_heap_update_ignore [simp]:

 declare typ_simps [simp]

+external_file "list_reverse_norm.c"
 install_C_file "list_reverse_norm.c"

 lemma (in list_reverse_norm_global_addresses) reverse_correct:
--- a/tools/c-parser/testfiles/locvarfncall.thy
+++ b/tools/c-parser/testfiles/locvarfncall.thy
@ -12,6 +12,7 @@ theory locvarfncall
 imports "CParser.CTranslation"
 begin

+external_file "locvarfncall.c"
 install_C_file "locvarfncall.c"

 context "locvarfncall"
--- a/tools/c-parser/testfiles/longlong.thy
+++ b/tools/c-parser/testfiles/longlong.thy
@ -12,6 +12,7 @@ theory longlong
 imports "CParser.CTranslation"
 begin

+external_file "longlong.c"
 install_C_file "longlong.c"

 ML {* NameGeneration.return_var_name (Absyn.Signed Absyn.LongLong) *}
--- a/tools/c-parser/testfiles/many_local_vars.thy
+++ b/tools/c-parser/testfiles/many_local_vars.thy
@ -17,6 +17,7 @@ begin
 * containing local variables. *)
 declare [[record_codegen = false]]

+external_file "many_local_vars.c"
 install_C_file "many_local_vars.c"

 context "many_local_vars_global_addresses" begin
--- a/tools/c-parser/testfiles/modifies_assumptions.thy
+++ b/tools/c-parser/testfiles/modifies_assumptions.thy
@ -12,6 +12,7 @@ theory modifies_assumptions
 imports "CParser.CTranslation"
 begin

+external_file "modifies_assumptions.c"
 install_C_file "modifies_assumptions.c"

 context modifies_assumptions
--- a/tools/c-parser/testfiles/multi_deref.thy
+++ b/tools/c-parser/testfiles/multi_deref.thy
@ -12,6 +12,7 @@ theory multi_deref
 imports "CParser.CTranslation"
 begin

+external_file "multi_deref.c"
 install_C_file "multi_deref.c"

 context multi_deref_global_addresses begin
--- a/tools/c-parser/testfiles/multidim_arrays.thy
+++ b/tools/c-parser/testfiles/multidim_arrays.thy
@ -12,6 +12,7 @@ theory multidim_arrays
 imports "CParser.CTranslation"
 begin

+external_file "multidim_arrays.c"
 install_C_file "multidim_arrays.c"

 context multidim_arrays
--- a/tools/c-parser/testfiles/mutrec_modifies.thy
+++ b/tools/c-parser/testfiles/mutrec_modifies.thy
@ -12,6 +12,7 @@ theory mutrec_modifies
 imports "CParser.CTranslation"
 begin

+external_file "mutrec_modifies.c"
 install_C_file "mutrec_modifies.c"

 context mutrec_modifies
--- a/tools/c-parser/testfiles/parse_addr.thy
+++ b/tools/c-parser/testfiles/parse_addr.thy
@ -12,6 +12,7 @@ theory parse_addr
 imports "CParser.CTranslation"
 begin

+external_file "parse_addr.c"
 install_C_file "parse_addr.c"

 context parse_addr_global_addresses
--- a/tools/c-parser/testfiles/parse_c99block.thy
+++ b/tools/c-parser/testfiles/parse_c99block.thy
@ -12,6 +12,7 @@ theory parse_c99block
 imports "CParser.CTranslation"
 begin

+external_file "parse_c99block.c"
 install_C_file "parse_c99block.c"

 thm parse_c99block_global_addresses.f_body_def
--- a/tools/c-parser/testfiles/parse_complit.thy
+++ b/tools/c-parser/testfiles/parse_complit.thy
@ -12,6 +12,7 @@ theory parse_complit
 imports "CParser.CTranslation"
 begin

+external_file "parse_complit.c"
 install_C_file "parse_complit.c"

 context parse_complit_global_addresses
--- a/tools/c-parser/testfiles/parse_dowhile.thy
+++ b/tools/c-parser/testfiles/parse_dowhile.thy
@ -12,6 +12,7 @@ theory parse_dowhile
 imports "CParser.CTranslation"
 begin

+external_file "parse_dowhile.c"
 install_C_file "parse_dowhile.c"

 print_locale parse_dowhile_global_addresses
--- a/tools/c-parser/testfiles/parse_enum.thy
+++ b/tools/c-parser/testfiles/parse_enum.thy
@ -12,6 +12,7 @@ theory parse_enum
 imports "CParser.CTranslation"
 begin

+external_file "parse_enum.c"
 install_C_file "parse_enum.c"

 print_locale parse_enum_global_addresses
--- a/tools/c-parser/testfiles/parse_fncall.thy
+++ b/tools/c-parser/testfiles/parse_fncall.thy
@ -12,6 +12,7 @@ theory parse_fncall
 imports "CParser.CTranslation"
 begin

+external_file "parse_fncall.c"
 install_C_file "parse_fncall.c"

 print_locale parse_fncall_global_addresses
--- a/tools/c-parser/testfiles/parse_forloop.thy
+++ b/tools/c-parser/testfiles/parse_forloop.thy
@ -12,6 +12,7 @@ theory parse_forloop
 imports "CParser.CTranslation"
 begin

+external_file "parse_forloop.c"
 install_C_file "parse_forloop.c"

 print_locale parse_forloop_global_addresses
--- a/tools/c-parser/testfiles/parse_include.thy
+++ b/tools/c-parser/testfiles/parse_include.thy
@ -12,6 +12,9 @@ theory parse_include
 imports "CParser.CTranslation"
 begin

+external_file "includes/test_include2.h"
+external_file "parse_include.c"
+
 new_C_include_dir "includes"

 install_C_file "parse_include.c"
--- a/tools/c-parser/testfiles/parse_protos.thy
+++ b/tools/c-parser/testfiles/parse_protos.thy
@ -12,6 +12,7 @@ theory parse_protos
 imports "CParser.CTranslation"
 begin

+external_file "parse_protos.c"
 install_C_file "parse_protos.c"

 context parse_protos_global_addresses
--- a/tools/c-parser/testfiles/parse_retfncall.thy
+++ b/tools/c-parser/testfiles/parse_retfncall.thy
@ -12,6 +12,7 @@ theory parse_retfncall
 imports "CParser.CTranslation"
 begin

+external_file "parse_retfncall.c"
 install_C_file "parse_retfncall.c"

 print_locale parse_retfncall_global_addresses
--- a/tools/c-parser/testfiles/parse_sizeof.thy
+++ b/tools/c-parser/testfiles/parse_sizeof.thy
@ -12,6 +12,7 @@ theory parse_sizeof
 imports "CParser.CTranslation"
 begin

+external_file "parse_sizeof.c"
 install_C_file "parse_sizeof.c"

 print_locale parse_sizeof_global_addresses
--- a/tools/c-parser/testfiles/parse_someops.thy
+++ b/tools/c-parser/testfiles/parse_someops.thy
@ -12,6 +12,7 @@ theory parse_someops
 imports "CParser.CTranslation"
 begin

+external_file "parse_someops.c"
 install_C_file "parse_someops.c"

 print_locale parse_someops_global_addresses
--- a/tools/c-parser/testfiles/parse_struct.thy
+++ b/tools/c-parser/testfiles/parse_struct.thy
@ -12,6 +12,7 @@ theory parse_struct
 imports "CParser.CTranslation"
 begin

+external_file "parse_struct.c"
 install_C_file "parse_struct.c"

 (* mem_type instances proved automatically.  If you remove the additional
--- a/tools/c-parser/testfiles/parse_struct_array.thy
+++ b/tools/c-parser/testfiles/parse_struct_array.thy
@ -12,6 +12,7 @@ theory parse_struct_array
 imports "CParser.CTranslation"
 begin

+external_file "parse_struct_array.c"
 install_C_file "parse_struct_array.c"

 term "globk2_'"
--- a/tools/c-parser/testfiles/parse_switch.thy
+++ b/tools/c-parser/testfiles/parse_switch.thy
@ -12,6 +12,7 @@ theory parse_switch
 imports "CParser.CTranslation"
 begin

+external_file "parse_switch.c"
 install_C_file "parse_switch.c"

 context parse_switch_global_addresses
--- a/Show More
+++ b/Show More