Add second function summary (both run in 10 mins)

kth-step · Oct 18, 2024 · f69c34e · f69c34e
1 parent c673e5b
commit f69c34e
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 6 deletions.
diff --git a/examples/arm_cm0/balrob/balrob_endsScript.sml b/examples/arm_cm0/balrob/balrob_endsScript.sml
@@ -11,7 +11,18 @@ val locs =
    0x100013dc);
 
 val symb_exec_thm = birs_summary birs_prog_config reqs locs;
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
 
-Theorem balrob_clzsi2_symb_exec_thm = symb_exec_thm
+(* ------------------------------------ *)
+val entry_name = "__lesf2";
+val reqs = get_fun_usage entry_name;
+val locs =
+  (0x10000a4c,
+   0x10000ad2);
+
+val symb_exec_thm = birs_summary birs_prog_config reqs locs;
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
+
+(* ------------------------------------ *)
 
 val _ = export_theory ();
diff --git a/examples/arm_cm0/balrob/balrob_insttestScript.sml b/examples/arm_cm0/balrob/balrob_insttestScript.sml
@@ -10,20 +10,20 @@ open balrob_endsTheory;
 
 val _ = new_theory "balrob_insttest";
 
-(* instantiation test *)
+(* insttest *)
 val reqs = (0,63);
 val locs =
   (0x100012d6,
    0x100013b4);
 
 val symb_exec_thm = birs_summary birs_prog_config reqs locs;
 
-Theorem balrob_insttest_symb_exec_thm = symb_exec_thm
+Theorem balrob_summary_insttest_thm = symb_exec_thm
 
 
 (* now instantiate *)
-val A_thm = balrob_insttest_symb_exec_thm;
-val B_thm = balrob_clzsi2_symb_exec_thm;
+val A_thm = balrob_summary_insttest_thm;
+val B_thm = balrob_summary___clzsi2_thm;
 val inst_thm = birs_basic_instantiate birs_prog_config A_thm B_thm;
 
 Theorem balrob_insttest_symb_inst_thm = inst_thm

diff --git a/examples/arm_cm0/balrob/balrob_symb_transfScript.sml b/examples/arm_cm0/balrob/balrob_symb_transfScript.sml
@@ -15,7 +15,7 @@ open balrob_endsTheory;
 val _ = new_theory "balrob_symb_transf";
 
 
-val balrob_exec_thm = balrob_clzsi2_symb_exec_thm;
+val balrob_exec_thm = balrob_summary___clzsi2_thm;
 
 (**)
 val bprog_envtyl_tm = (fst o dest_eq o concl) balrob_birenvtyl_def;