Add more functions to the analysis

examples/arm_cm0/balrob/balrob_endsScript.sml

@@ -7,8 +7,8 @@ val _ = new_theory "balrob_ends";
 val entry_name = "__clzsi2";
 val reqs = get_fun_usage entry_name;
 val locs =
-  (0x100013b4,
-   0x100013dc);
+  ( 0x100013b4,
+   [0x100013dc]);
 
 val symb_exec_thm = birs_summary birs_prog_config [] reqs locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
@@ -17,17 +17,15 @@ val _ = print "\n";
 val _ = Profile.print_profile_results (Profile.results ());
 
 (* ------------------------------------ *)
-(*
 val entry_name = "__lesf2";
 val reqs = get_fun_usage entry_name;
 val locs =
-  (0x10000a4c,
-   0x10000ad2);
+  ( 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 ();

examples/arm_cm0/balrob/balrob_insttestScript.sml

@@ -13,15 +13,16 @@ val _ = new_theory "balrob_insttest";
 (* insttest *)
 val reqs = (0,63);
 val locs =
-  (0x100012d6,
-   0x100013b4
+  ( 0x100012d6,
+   [0x100012e2]
    (*0x100012e2*)
    (*0x100013b4*));
 
 val symb_exec_thm = birs_summary birs_prog_config [balrob_summary___clzsi2_thm] reqs locs;
 
 Theorem balrob_summary_insttest_thm = symb_exec_thm
 
+(*
 (* now instantiate *)
 val A_thm = balrob_summary_insttest_thm;
 val B_thm = balrob_summary___clzsi2_thm;
@@ -31,6 +32,7 @@ val _ = print "\n";
 val _ = Profile.print_profile_results (Profile.results ());
 
 Theorem balrob_insttest_symb_inst_thm = inst_thm
+*)
 
 val _ = export_theory ();
 

examples/arm_cm0/balrob/balrob_miscScript.sml

@@ -0,0 +1,57 @@
+open HolKernel Parse boolLib bossLib;
+
+open balrob_supportLib;
+
+open balrob_endsTheory;
+
+val _ = new_theory "balrob_misc";
+
+val entry_name = "__aeabi_i2f";
+val reqs = get_fun_usage entry_name;
+val locs =
+  ( 0x100012c8,
+   [0x10001348]);
+
+val symb_exec_thm = birs_summary birs_prog_config [balrob_summary___clzsi2_thm] reqs locs;
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
+
+val _ = print "\n";
+val _ = Profile.print_profile_results (Profile.results ());
+
+(* ------------------------------------ *)
+
+(*
+val entry_name = "__aeabi_fcmplt";
+val reqs = get_fun_usage entry_name;
+val locs =
+  ( 0x1000019c,
+   [0x100001a8,
+    0x100001ac]);
+
+val symb_exec_thm = birs_summary birs_prog_config [balrob_summary___lesf2_thm] reqs locs;
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
+(*
+Uncaught exception: HOL_ERR {message = "birs_symbval_concretizations_oracle_CONV: failed to resolve single jump target, not an equality theorem", origin_function = "RAND_CONV", origin_structure = "Conv"}
+*)
+*)
+
+(* ------------------------------------ *)
+
+(*
+val entry_name = "abs_own";
+val reqs = get_fun_usage entry_name;
+val locs =
+  ( 0x1000140e,
+   [0x10001434]);
+
+val symb_exec_thm = birs_summary birs_prog_config [balrob_summary___lesf2_thm] reqs locs;
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
+(*
+Uncaught exception: HOL_ERR {message = "birs_symbval_concretizations_oracle_CONV: failed to resolve single jump target, not an equality theorem", origin_function = "RAND_CONV", origin_structure = "Conv"}
+*)
+*)
+
+(* ------------------------------------ *)
+
+
+val _ = export_theory ();

examples/arm_cm0/balrob/balrob_supportLib.sml

@@ -300,10 +300,10 @@ fun birs_basic_instantiate (bprog_tm, prog_birenvtyl_def) =
 
 (* ========================================================================================== *)
 
-  fun birs_summary (bprog_tm, prog_birenvtyl_def) sums reqs (init_addr, end_addr) =
+  fun birs_summary (bprog_tm, prog_birenvtyl_def) sums reqs (init_addr, end_addrs) =
     let
       val init_state = birs_basic_init_state prog_birenvtyl_def reqs init_addr;
-      val symb_exec_thm = birs_basic_execute bprog_tm sums [end_addr] init_state;
+      val symb_exec_thm = birs_basic_execute bprog_tm sums end_addrs init_state;
 
       (* need to handle intervals correctly: in symbolic execution driver
            (also need this together with the indirectjump handling and previous summaries) and also before merging *)