Isabelle2018 autocorres: declare external files
This commit is contained in:
parent
efe8d89a99
commit
1383f4ceee
|
@ -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' >> $@
|
||||
|
|
|
@ -13,6 +13,8 @@ imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "alloc_lite.c"
|
||||
|
||||
(* Parse the input file. *)
|
||||
install_C_file "alloc_lite.c"
|
||||
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -16,6 +16,8 @@ theory AC_Rename imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "rename.c"
|
||||
|
||||
declare [[allow_underscore_idents]]
|
||||
install_C_file "rename.c"
|
||||
|
||||
|
|
|
@ -13,6 +13,8 @@ imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "alloc.c"
|
||||
|
||||
(* Parse the input file. *)
|
||||
install_C_file "alloc.c"
|
||||
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -39,6 +39,7 @@ theory CList imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "list.c"
|
||||
install_C_file "list.c"
|
||||
autocorres "list.c"
|
||||
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -17,6 +17,8 @@ imports
|
|||
"Lib.OptionMonadWP"
|
||||
begin
|
||||
|
||||
external_file "factorial.c"
|
||||
|
||||
(* Parse the input file. *)
|
||||
install_C_file "factorial.c"
|
||||
|
||||
|
|
|
@ -23,6 +23,8 @@ imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "factorial.c"
|
||||
|
||||
(*
|
||||
* The venerable Fibonacci function.
|
||||
*)
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -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 *)
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -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 *)
|
||||
|
|
|
@ -12,6 +12,7 @@ theory Memset
|
|||
imports "AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "memset.c"
|
||||
install_C_file "memset.c"
|
||||
|
||||
autocorres [
|
||||
|
|
|
@ -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. *)
|
||||
|
|
|
@ -13,6 +13,7 @@ imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "plus.c"
|
||||
install_C_file "plus.c"
|
||||
|
||||
autocorres [ ts_force nondet = plus2 ] "plus.c"
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -13,6 +13,8 @@ imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "simple.c"
|
||||
|
||||
(* Parse the input file. *)
|
||||
install_C_file "simple.c"
|
||||
|
||||
|
|
|
@ -14,6 +14,7 @@ imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "str2long.c"
|
||||
install_C_file "str2long.c"
|
||||
autocorres "str2long.c"
|
||||
|
||||
|
|
|
@ -18,6 +18,7 @@ imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "suzuki.c"
|
||||
install_C_file "suzuki.c"
|
||||
autocorres [heap_abs_syntax] "suzuki.c"
|
||||
|
||||
|
|
|
@ -13,6 +13,8 @@ imports
|
|||
"AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "swap.c"
|
||||
|
||||
(* Parse the input file. *)
|
||||
install_C_file "swap.c"
|
||||
|
||||
|
|
|
@ -17,6 +17,7 @@
|
|||
|
||||
theory TraceDemo imports "AutoCorres.AutoCorres" begin
|
||||
|
||||
external_file "trace_demo.c"
|
||||
install_C_file "trace_demo.c"
|
||||
|
||||
autocorres [
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -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 *)
|
||||
|
|
|
@ -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]:
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -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 [
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -12,6 +12,7 @@ theory struct
|
|||
imports "AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "struct.c"
|
||||
install_C_file "struct.c"
|
||||
|
||||
end
|
||||
|
|
|
@ -12,6 +12,7 @@ theory struct2
|
|||
imports "AutoCorres.AutoCorres"
|
||||
begin
|
||||
|
||||
external_file "struct2.c"
|
||||
install_C_file "struct2.c"
|
||||
|
||||
autocorres [keep_going] "struct2.c"
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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 [
|
||||
|
|
Loading…
Reference in New Issue