From 1383f4ceeeedeec8fd3c4da55ed7ad02d9493e94 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Sun, 24 Jun 2018 13:25:00 +0200
Subject: [PATCH] Isabelle2018 autocorres: declare external files

---
 tools/autocorres/Makefile                                      | 1 +
 tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy        | 2 ++
 tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy        | 2 ++
 tools/autocorres/tests/examples/AC_Rename.thy                  | 2 ++
 tools/autocorres/tests/examples/Alloc.thy                      | 2 ++
 tools/autocorres/tests/examples/BinarySearch.thy               | 1 +
 tools/autocorres/tests/examples/CList.thy                      | 1 +
 tools/autocorres/tests/examples/ConditionGuard.thy             | 1 +
 tools/autocorres/tests/examples/FactorialTest.thy              | 2 ++
 tools/autocorres/tests/examples/FibProof.thy                   | 2 ++
 tools/autocorres/tests/examples/FunctionInfoDemo.thy           | 2 ++
 tools/autocorres/tests/examples/HeapWrap.thy                   | 1 +
 tools/autocorres/tests/examples/Incremental.thy                | 1 +
 tools/autocorres/tests/examples/IsPrime.thy                    | 2 ++
 tools/autocorres/tests/examples/Kmalloc.thy                    | 3 ++-
 tools/autocorres/tests/examples/ListRev.thy                    | 1 +
 tools/autocorres/tests/examples/Memcpy.thy                     | 1 +
 tools/autocorres/tests/examples/Memset.thy                     | 1 +
 tools/autocorres/tests/examples/MultByAdd.thy                  | 1 +
 tools/autocorres/tests/examples/Plus.thy                       | 1 +
 tools/autocorres/tests/examples/Quicksort.thy                  | 1 +
 tools/autocorres/tests/examples/SchorrWaite.thy                | 1 +
 tools/autocorres/tests/examples/Simple.thy                     | 2 ++
 tools/autocorres/tests/examples/Str2Long.thy                   | 1 +
 tools/autocorres/tests/examples/Suzuki.thy                     | 1 +
 tools/autocorres/tests/examples/Swap.thy                       | 2 ++
 tools/autocorres/tests/examples/TraceDemo.thy                  | 1 +
 tools/autocorres/tests/examples/WordAbs.thy                    | 1 +
 tools/autocorres/tests/examples/type_strengthen_tricks.thy     | 1 +
 tools/autocorres/tests/failing/dirty_frees.thy                 | 1 +
 tools/autocorres/tests/failing/jira_ver_591.thy                | 1 +
 tools/autocorres/tests/proof-tests/CustomWordAbs.thy           | 1 +
 tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy   | 1 +
 tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy  | 1 +
 tools/autocorres/tests/proof-tests/WordAbsFnCall.thy           | 1 +
 tools/autocorres/tests/proof-tests/array_indirect_update.thy   | 1 +
 tools/autocorres/tests/proof-tests/badnames.thy                | 2 ++
 tools/autocorres/tests/proof-tests/global_array_update.thy     | 1 +
 tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy | 1 +
 tools/autocorres/tests/proof-tests/nested_struct.thy           | 1 +
 tools/autocorres/tests/proof-tests/prototyped_functions.thy    | 1 +
 tools/autocorres/tests/proof-tests/skip_heap_abs.thy           | 1 +
 tools/autocorres/tests/proof-tests/struct.thy                  | 1 +
 tools/autocorres/tests/proof-tests/struct2.thy                 | 1 +
 tools/autocorres/tests/proof-tests/word_abs_cases.thy          | 1 +
 tools/autocorres/tests/proof-tests/word_abs_options.thy        | 1 +
 46 files changed, 58 insertions(+), 1 deletion(-)

diff --git a/tools/autocorres/Makefile b/tools/autocorres/Makefile
index 7d21eefef..6f13d9c14 100644
--- a/tools/autocorres/Makefile
+++ b/tools/autocorres/Makefile
@@ -46,6 +46,7 @@ tests/All.thy: \
 	@echo "Generating '$@' from '$<'..."
 	@printf '(* @LICENSE(NICTA) *)\n\n' > $@
 	@printf 'theory %s\nimports "AutoCorres.AutoCorres"\nbegin\n\n' $(notdir $(basename $<)) > $@
+	@printf 'external_file "%s"\n\n' $(notdir $<) >> $@
 	@printf 'install_C_file "%s"\n\n' $(notdir $<) >> $@
 	@printf 'autocorres "%s"\n\n' $(notdir $<) >> $@
 	@printf 'end\n' >> $@
diff --git a/tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy b/tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy
index 1e72f5aa5..a55197eea 100644
--- a/tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy
+++ b/tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy
@@ -13,6 +13,8 @@ imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file  "alloc_lite.c"
+
 (* Parse the input file. *)
 install_C_file  "alloc_lite.c"
 
diff --git a/tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy b/tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy
index d176036f8..85576a680 100644
--- a/tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy
+++ b/tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy
@@ -17,6 +17,8 @@ imports
   "Hoare_Sep_Tactics.Hoare_Sep_Tactics"
 begin
 
+external_file  "alloc_simp.c"
+
 (* Parse the input file. *)
 install_C_file  "alloc_simp.c"
 
diff --git a/tools/autocorres/tests/examples/AC_Rename.thy b/tools/autocorres/tests/examples/AC_Rename.thy
index 297515900..a89b6e7eb 100644
--- a/tools/autocorres/tests/examples/AC_Rename.thy
+++ b/tools/autocorres/tests/examples/AC_Rename.thy
@@ -16,6 +16,8 @@ theory AC_Rename imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "rename.c"
+
 declare [[allow_underscore_idents]]
 install_C_file "rename.c"
 
diff --git a/tools/autocorres/tests/examples/Alloc.thy b/tools/autocorres/tests/examples/Alloc.thy
index 8008c72e8..f3b06660a 100644
--- a/tools/autocorres/tests/examples/Alloc.thy
+++ b/tools/autocorres/tests/examples/Alloc.thy
@@ -13,6 +13,8 @@ imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file  "alloc.c"
+
 (* Parse the input file. *)
 install_C_file  "alloc.c"
 
diff --git a/tools/autocorres/tests/examples/BinarySearch.thy b/tools/autocorres/tests/examples/BinarySearch.thy
index 0d87e1216..d9602deb5 100644
--- a/tools/autocorres/tests/examples/BinarySearch.thy
+++ b/tools/autocorres/tests/examples/BinarySearch.thy
@@ -12,6 +12,7 @@ theory BinarySearch
 imports "AutoCorres.AutoCorres" "../../DataStructures"
 begin
 
+external_file "binary_search.c"
 install_C_file "binary_search.c"
 
 autocorres [ts_rules = nondet, unsigned_word_abs=binary_search] "binary_search.c"
diff --git a/tools/autocorres/tests/examples/CList.thy b/tools/autocorres/tests/examples/CList.thy
index 7ae442f79..08f081149 100644
--- a/tools/autocorres/tests/examples/CList.thy
+++ b/tools/autocorres/tests/examples/CList.thy
@@ -39,6 +39,7 @@ theory CList imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "list.c"
 install_C_file "list.c"
 autocorres "list.c"
 
diff --git a/tools/autocorres/tests/examples/ConditionGuard.thy b/tools/autocorres/tests/examples/ConditionGuard.thy
index 760b0e1b8..1de375494 100644
--- a/tools/autocorres/tests/examples/ConditionGuard.thy
+++ b/tools/autocorres/tests/examples/ConditionGuard.thy
@@ -13,6 +13,7 @@ theory ConditionGuard
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "condition_guard.c"
 install_C_file "condition_guard.c"
 autocorres "condition_guard.c"
 
diff --git a/tools/autocorres/tests/examples/FactorialTest.thy b/tools/autocorres/tests/examples/FactorialTest.thy
index 1e2fc35a3..39adf42be 100644
--- a/tools/autocorres/tests/examples/FactorialTest.thy
+++ b/tools/autocorres/tests/examples/FactorialTest.thy
@@ -17,6 +17,8 @@ imports
   "Lib.OptionMonadWP"
 begin
 
+external_file "factorial.c"
+
 (* Parse the input file. *)
 install_C_file "factorial.c"
 
diff --git a/tools/autocorres/tests/examples/FibProof.thy b/tools/autocorres/tests/examples/FibProof.thy
index 3619bfb99..c587cdaae 100644
--- a/tools/autocorres/tests/examples/FibProof.thy
+++ b/tools/autocorres/tests/examples/FibProof.thy
@@ -23,6 +23,8 @@ imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "factorial.c"
+
 (*
  * The venerable Fibonacci function.
  *)
diff --git a/tools/autocorres/tests/examples/FunctionInfoDemo.thy b/tools/autocorres/tests/examples/FunctionInfoDemo.thy
index 18dda8f13..9e2c6fa05 100644
--- a/tools/autocorres/tests/examples/FunctionInfoDemo.thy
+++ b/tools/autocorres/tests/examples/FunctionInfoDemo.thy
@@ -19,6 +19,8 @@ theory FunctionInfoDemo imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "function_info.c"
+
 text \<open>Process a source file to populate our data structures.\<close>
 install_C_file "function_info.c"
 autocorres "function_info.c"
diff --git a/tools/autocorres/tests/examples/HeapWrap.thy b/tools/autocorres/tests/examples/HeapWrap.thy
index 0c370afb1..ae053f876 100644
--- a/tools/autocorres/tests/examples/HeapWrap.thy
+++ b/tools/autocorres/tests/examples/HeapWrap.thy
@@ -16,6 +16,7 @@ theory HeapWrap
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "heap_wrap.c"
 install_C_file "heap_wrap.c"
 autocorres [heap_abs_syntax] "heap_wrap.c"
 
diff --git a/tools/autocorres/tests/examples/Incremental.thy b/tools/autocorres/tests/examples/Incremental.thy
index 8d0ec6049..023314e08 100644
--- a/tools/autocorres/tests/examples/Incremental.thy
+++ b/tools/autocorres/tests/examples/Incremental.thy
@@ -17,6 +17,7 @@ theory Incremental imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "type_strengthen.c"
 install_C_file "type_strengthen.c"
 
 (* Translate only opt_j *)
diff --git a/tools/autocorres/tests/examples/IsPrime.thy b/tools/autocorres/tests/examples/IsPrime.thy
index ff9cd18e3..e851969a9 100644
--- a/tools/autocorres/tests/examples/IsPrime.thy
+++ b/tools/autocorres/tests/examples/IsPrime.thy
@@ -14,6 +14,8 @@ imports
   "HOL-Computational_Algebra.Primes"
 begin
 
+external_file "is_prime.c"
+
 (* Parse the input file. *)
 install_C_file "is_prime.c"
 
diff --git a/tools/autocorres/tests/examples/Kmalloc.thy b/tools/autocorres/tests/examples/Kmalloc.thy
index cee1ebe3e..d80a7a020 100644
--- a/tools/autocorres/tests/examples/Kmalloc.thy
+++ b/tools/autocorres/tests/examples/Kmalloc.thy
@@ -12,6 +12,8 @@ theory Kmalloc
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "kmalloc.c"
+
 (* No proof here, just testing the parser. *)
 
 consts
@@ -19,7 +21,6 @@ consts
   ptr_retyps :: "nat \<Rightarrow> addr \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc"
 
 install_C_file "kmalloc.c"
-
 autocorres "kmalloc.c"
 
 context kmalloc begin
diff --git a/tools/autocorres/tests/examples/ListRev.thy b/tools/autocorres/tests/examples/ListRev.thy
index acdc6c321..d212b7ea1 100644
--- a/tools/autocorres/tests/examples/ListRev.thy
+++ b/tools/autocorres/tests/examples/ListRev.thy
@@ -12,6 +12,7 @@ theory ListRev
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "list_rev.c"
 install_C_file "list_rev.c"
 
 autocorres [heap_abs_syntax] "list_rev.c"
diff --git a/tools/autocorres/tests/examples/Memcpy.thy b/tools/autocorres/tests/examples/Memcpy.thy
index 9cac2934b..6e0659d6e 100644
--- a/tools/autocorres/tests/examples/Memcpy.thy
+++ b/tools/autocorres/tests/examples/Memcpy.thy
@@ -44,6 +44,7 @@ lemma ptr_contained:"\<lbrakk> c_guard (x::('a::c_type) ptr); size_of TYPE('a) =
   apply (clarsimp simp: nat_less_iff of_nat_nat)
   done
 
+external_file "memcpy.c"
 install_C_file "memcpy.c"
 
 (* FIXME: MOVE *)
diff --git a/tools/autocorres/tests/examples/Memset.thy b/tools/autocorres/tests/examples/Memset.thy
index fb1fa57b9..5f229910a 100644
--- a/tools/autocorres/tests/examples/Memset.thy
+++ b/tools/autocorres/tests/examples/Memset.thy
@@ -12,6 +12,7 @@ theory Memset
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "memset.c"
 install_C_file "memset.c"
 
 autocorres [
diff --git a/tools/autocorres/tests/examples/MultByAdd.thy b/tools/autocorres/tests/examples/MultByAdd.thy
index 0b68c14cc..cd7d813c3 100644
--- a/tools/autocorres/tests/examples/MultByAdd.thy
+++ b/tools/autocorres/tests/examples/MultByAdd.thy
@@ -14,6 +14,7 @@ imports
 begin
 
 (* Parse the input file. *)
+external_file "mult_by_add.c"
 install_C_file "mult_by_add.c"
 
 (* Abstract the input file. *)
diff --git a/tools/autocorres/tests/examples/Plus.thy b/tools/autocorres/tests/examples/Plus.thy
index 2733d17e4..c82570989 100644
--- a/tools/autocorres/tests/examples/Plus.thy
+++ b/tools/autocorres/tests/examples/Plus.thy
@@ -13,6 +13,7 @@ imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "plus.c"
 install_C_file "plus.c"
 
 autocorres [ ts_force nondet = plus2 ] "plus.c"
diff --git a/tools/autocorres/tests/examples/Quicksort.thy b/tools/autocorres/tests/examples/Quicksort.thy
index 56513155d..1b5dbb509 100644
--- a/tools/autocorres/tests/examples/Quicksort.thy
+++ b/tools/autocorres/tests/examples/Quicksort.thy
@@ -22,6 +22,7 @@ declare validNF_whileLoopE_inv_measure_twosteps [wp]
 
 declare creturn_def [vcg_simp]
 
+external_file "quicksort.c"
 install_C_file "quicksort.c"
 autocorres "quicksort.c"
 
diff --git a/tools/autocorres/tests/examples/SchorrWaite.thy b/tools/autocorres/tests/examples/SchorrWaite.thy
index 95fce8ada..ac630ddc0 100644
--- a/tools/autocorres/tests/examples/SchorrWaite.thy
+++ b/tools/autocorres/tests/examples/SchorrWaite.thy
@@ -53,6 +53,7 @@ begin
 
 declare fun_upd_apply[simp del]
 
+external_file "schorr_waite.c"
 install_C_file "schorr_waite.c"
 autocorres [heap_abs_syntax] "schorr_waite.c"
 
diff --git a/tools/autocorres/tests/examples/Simple.thy b/tools/autocorres/tests/examples/Simple.thy
index 151a11e14..2c80330ba 100644
--- a/tools/autocorres/tests/examples/Simple.thy
+++ b/tools/autocorres/tests/examples/Simple.thy
@@ -13,6 +13,8 @@ imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "simple.c"
+
 (* Parse the input file. *)
 install_C_file "simple.c"
 
diff --git a/tools/autocorres/tests/examples/Str2Long.thy b/tools/autocorres/tests/examples/Str2Long.thy
index 3e2194250..99d46fa94 100644
--- a/tools/autocorres/tests/examples/Str2Long.thy
+++ b/tools/autocorres/tests/examples/Str2Long.thy
@@ -14,6 +14,7 @@ imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "str2long.c"
 install_C_file "str2long.c"
 autocorres "str2long.c"
 
diff --git a/tools/autocorres/tests/examples/Suzuki.thy b/tools/autocorres/tests/examples/Suzuki.thy
index 2552bbdac..c3c747bbd 100644
--- a/tools/autocorres/tests/examples/Suzuki.thy
+++ b/tools/autocorres/tests/examples/Suzuki.thy
@@ -18,6 +18,7 @@ imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "suzuki.c"
 install_C_file "suzuki.c"
 autocorres [heap_abs_syntax] "suzuki.c"
 
diff --git a/tools/autocorres/tests/examples/Swap.thy b/tools/autocorres/tests/examples/Swap.thy
index 24d74f871..74b153c24 100644
--- a/tools/autocorres/tests/examples/Swap.thy
+++ b/tools/autocorres/tests/examples/Swap.thy
@@ -13,6 +13,8 @@ imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file  "swap.c"
+
 (* Parse the input file. *)
 install_C_file  "swap.c"
 
diff --git a/tools/autocorres/tests/examples/TraceDemo.thy b/tools/autocorres/tests/examples/TraceDemo.thy
index dfabaf2b6..fcbbd3b78 100644
--- a/tools/autocorres/tests/examples/TraceDemo.thy
+++ b/tools/autocorres/tests/examples/TraceDemo.thy
@@ -17,6 +17,7 @@
 
 theory TraceDemo imports "AutoCorres.AutoCorres" begin
 
+external_file "trace_demo.c"
 install_C_file "trace_demo.c"
 
 autocorres [
diff --git a/tools/autocorres/tests/examples/WordAbs.thy b/tools/autocorres/tests/examples/WordAbs.thy
index bc34af768..bb00b471b 100644
--- a/tools/autocorres/tests/examples/WordAbs.thy
+++ b/tools/autocorres/tests/examples/WordAbs.thy
@@ -12,6 +12,7 @@ theory WordAbs
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "word_abs.c"
 install_C_file "word_abs.c"
 autocorres [unsigned_word_abs = f] "word_abs.c"
 
diff --git a/tools/autocorres/tests/examples/type_strengthen_tricks.thy b/tools/autocorres/tests/examples/type_strengthen_tricks.thy
index 9d9945d6a..490741eb1 100644
--- a/tools/autocorres/tests/examples/type_strengthen_tricks.thy
+++ b/tools/autocorres/tests/examples/type_strengthen_tricks.thy
@@ -16,6 +16,7 @@ theory type_strengthen_tricks imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "type_strengthen.c"
 install_C_file "type_strengthen.c"
 
 (* We can configure the type strengthen rules individually.
diff --git a/tools/autocorres/tests/failing/dirty_frees.thy b/tools/autocorres/tests/failing/dirty_frees.thy
index 3add58316..a8bad0853 100644
--- a/tools/autocorres/tests/failing/dirty_frees.thy
+++ b/tools/autocorres/tests/failing/dirty_frees.thy
@@ -13,6 +13,7 @@
  *)
 theory dirty_frees imports "AutoCorres.AutoCorres" begin
 
+external_file "dirty_frees.c"
 install_C_file "dirty_frees.c"
 
 autocorres [scope = f1 f2, function_name_suffix = ""] "dirty_frees.c"
diff --git a/tools/autocorres/tests/failing/jira_ver_591.thy b/tools/autocorres/tests/failing/jira_ver_591.thy
index 8c9470054..0134f2348 100644
--- a/tools/autocorres/tests/failing/jira_ver_591.thy
+++ b/tools/autocorres/tests/failing/jira_ver_591.thy
@@ -13,6 +13,7 @@
  *)
 theory jira_ver_591 imports "AutoCorres.AutoCorres" begin
 
+external_file "jira_ver_591.c"
 install_C_file "jira_ver_591.c"
 
 (* This fails *)
diff --git a/tools/autocorres/tests/proof-tests/CustomWordAbs.thy b/tools/autocorres/tests/proof-tests/CustomWordAbs.thy
index 912868a56..d5e265fff 100644
--- a/tools/autocorres/tests/proof-tests/CustomWordAbs.thy
+++ b/tools/autocorres/tests/proof-tests/CustomWordAbs.thy
@@ -12,6 +12,7 @@ theory CustomWordAbs
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "custom_word_abs.c"
 install_C_file "custom_word_abs.c"
 
 lemma [word_abs]:
diff --git a/tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy b/tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy
index f1425b818..679ccdd23 100644
--- a/tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy
+++ b/tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy
@@ -15,6 +15,7 @@ theory Test_Spec_Translation
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "test_spec_translation.c"
 install_C_file "test_spec_translation.c"
 
 autocorres [ts_rules = nondet] "test_spec_translation.c"
diff --git a/tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy b/tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy
index b24e3aa70..b678a9284 100644
--- a/tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy
+++ b/tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy
@@ -12,6 +12,7 @@ theory WhileLoopVarsPreserved imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "while_loop_vars_preserved.c"
 install_C_file "while_loop_vars_preserved.c"
 
 autocorres [ts_force nondet = loop] "while_loop_vars_preserved.c"
diff --git a/tools/autocorres/tests/proof-tests/WordAbsFnCall.thy b/tools/autocorres/tests/proof-tests/WordAbsFnCall.thy
index 3e5d594c0..ae912fb0c 100644
--- a/tools/autocorres/tests/proof-tests/WordAbsFnCall.thy
+++ b/tools/autocorres/tests/proof-tests/WordAbsFnCall.thy
@@ -12,6 +12,7 @@ theory WordAbsFnCall imports
   "AutoCorres.AutoCorres"
 begin
 
+external_file "word_abs_fn_call.c"
 install_C_file "word_abs_fn_call.c"
 
 (* Test interaction of abstracted/non-abstracted functions calling the
diff --git a/tools/autocorres/tests/proof-tests/array_indirect_update.thy b/tools/autocorres/tests/proof-tests/array_indirect_update.thy
index cc08d8f5e..03efc4c04 100644
--- a/tools/autocorres/tests/proof-tests/array_indirect_update.thy
+++ b/tools/autocorres/tests/proof-tests/array_indirect_update.thy
@@ -15,6 +15,7 @@
  *)
 theory array_indirect_update imports "AutoCorres.AutoCorres" begin
 
+external_file "array_indirect_update.c"
 install_C_file "array_indirect_update.c"
 autocorres "array_indirect_update.c"
 
diff --git a/tools/autocorres/tests/proof-tests/badnames.thy b/tools/autocorres/tests/proof-tests/badnames.thy
index b0e8dbf6a..948304672 100644
--- a/tools/autocorres/tests/proof-tests/badnames.thy
+++ b/tools/autocorres/tests/proof-tests/badnames.thy
@@ -13,6 +13,8 @@
  *)
 theory badnames imports "AutoCorres.AutoCorres" begin
 
+external_file "badnames.c"
+
 declare [[allow_underscore_idents]]
 install_C_file "badnames.c"
 autocorres "badnames.c"
diff --git a/tools/autocorres/tests/proof-tests/global_array_update.thy b/tools/autocorres/tests/proof-tests/global_array_update.thy
index 50be1eb54..5cd66d564 100644
--- a/tools/autocorres/tests/proof-tests/global_array_update.thy
+++ b/tools/autocorres/tests/proof-tests/global_array_update.thy
@@ -10,6 +10,7 @@
 
 theory global_array_update imports "AutoCorres.AutoCorres" begin
 
+external_file "global_array_update.c"
 install_C_file "global_array_update.c"
 autocorres "global_array_update.c"
 
diff --git a/tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy b/tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy
index 6612c00ce..fa128471a 100644
--- a/tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy
+++ b/tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy
@@ -16,6 +16,7 @@ theory heap_lift_force_prevent
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "heap_lift_force_prevent.c"
 install_C_file "heap_lift_force_prevent.c"
 
 autocorres [
diff --git a/tools/autocorres/tests/proof-tests/nested_struct.thy b/tools/autocorres/tests/proof-tests/nested_struct.thy
index 567d982a2..bf8e25f20 100644
--- a/tools/autocorres/tests/proof-tests/nested_struct.thy
+++ b/tools/autocorres/tests/proof-tests/nested_struct.thy
@@ -14,6 +14,7 @@
  *)
 theory nested_struct imports "AutoCorres.AutoCorres" begin
 
+external_file "nested_struct.c"
 install_C_file "nested_struct.c"
 (* Nested struct translation currently only works for packed_type types. *)
 instance s1_C :: array_outer_packed by intro_classes auto
diff --git a/tools/autocorres/tests/proof-tests/prototyped_functions.thy b/tools/autocorres/tests/proof-tests/prototyped_functions.thy
index ce08668f0..1e438d577 100644
--- a/tools/autocorres/tests/proof-tests/prototyped_functions.thy
+++ b/tools/autocorres/tests/proof-tests/prototyped_functions.thy
@@ -12,6 +12,7 @@ theory prototyped_functions
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "prototyped_functions.c"
 install_C_file "prototyped_functions.c"
 
 autocorres [ts_force option = moo4] "prototyped_functions.c"
diff --git a/tools/autocorres/tests/proof-tests/skip_heap_abs.thy b/tools/autocorres/tests/proof-tests/skip_heap_abs.thy
index 66ae4d978..aa1d60819 100644
--- a/tools/autocorres/tests/proof-tests/skip_heap_abs.thy
+++ b/tools/autocorres/tests/proof-tests/skip_heap_abs.thy
@@ -13,6 +13,7 @@
  *)
 theory skip_heap_abs imports "AutoCorres.AutoCorres" begin
 
+external_file "skip_heap_abs.c"
 install_C_file "skip_heap_abs.c"
 autocorres [skip_heap_abs] "skip_heap_abs.c"
 
diff --git a/tools/autocorres/tests/proof-tests/struct.thy b/tools/autocorres/tests/proof-tests/struct.thy
index 8c58ccae8..d9425fbec 100644
--- a/tools/autocorres/tests/proof-tests/struct.thy
+++ b/tools/autocorres/tests/proof-tests/struct.thy
@@ -12,6 +12,7 @@ theory struct
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "struct.c"
 install_C_file "struct.c"
 
 end
diff --git a/tools/autocorres/tests/proof-tests/struct2.thy b/tools/autocorres/tests/proof-tests/struct2.thy
index 0b7da16b6..05e6cdb7e 100644
--- a/tools/autocorres/tests/proof-tests/struct2.thy
+++ b/tools/autocorres/tests/proof-tests/struct2.thy
@@ -12,6 +12,7 @@ theory struct2
 imports "AutoCorres.AutoCorres"
 begin
 
+external_file "struct2.c"
 install_C_file "struct2.c"
 
 autocorres [keep_going] "struct2.c"
diff --git a/tools/autocorres/tests/proof-tests/word_abs_cases.thy b/tools/autocorres/tests/proof-tests/word_abs_cases.thy
index 46e03d0f4..c711368de 100644
--- a/tools/autocorres/tests/proof-tests/word_abs_cases.thy
+++ b/tools/autocorres/tests/proof-tests/word_abs_cases.thy
@@ -63,6 +63,7 @@ lemma [unfolded INT_MIN_def INT_MAX_def, simplified, L2flow]:
   "simp_expr (INT_MIN \<le> b \<and> b \<le> INT_MAX \<and> b \<noteq> 0) (a smod b \<le> INT_MAX) True"
   by (simp add: simp_expr_def INT_MIN_MAX_smod)
 
+external_file "word_abs_cases.c"
 install_C_file "word_abs_cases.c"
 autocorres [
   unsigned_word_abs = callee_flat_u_abs
diff --git a/tools/autocorres/tests/proof-tests/word_abs_options.thy b/tools/autocorres/tests/proof-tests/word_abs_options.thy
index b53951259..54e1640a2 100644
--- a/tools/autocorres/tests/proof-tests/word_abs_options.thy
+++ b/tools/autocorres/tests/proof-tests/word_abs_options.thy
@@ -10,6 +10,7 @@
 
 theory word_abs_options imports "AutoCorres.AutoCorres" begin
 
+external_file "word_abs_options.c"
 install_C_file "word_abs_options.c"
 
 autocorres [