Skip to content

Commit

Permalink
Update comments
Browse files Browse the repository at this point in the history
  • Loading branch information
andreaslindner committed Nov 5, 2024
1 parent f7db456 commit 5b89dc0
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 3 deletions.
4 changes: 3 additions & 1 deletion examples/arm_cm0/balrob/balrob_fdivScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ open HolKernel Parse boolLib bossLib;
open balrob_supportLib;

open balrob_endsTheory;
open balrob_fsubTheory; (* TODO: remove this line later *)
open balrob_faddTheory; (* TODO: remove this line later *)

val _ = new_theory "balrob_fdiv";

Expand Down Expand Up @@ -101,6 +103,7 @@ val balrob_summary___aeabi_fdiv_c7_thm = save_thm("balrob_summary_" ^ entry_name

(*
(* TODO: uses two jump table encoded in manually extracted cfg! *)
(* TODO: loads constants from memory! *)
val entry_name = "__aeabi_fdiv";
val reqs = get_fun_usage entry_name;
val locs =
Expand All @@ -121,7 +124,6 @@ val symb_exec_thm = birs_summary birs_prog_config
val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
*)


(* ------------------------------------ *)

val _ = print "\n";
Expand Down
6 changes: 4 additions & 2 deletions examples/arm_cm0/balrob/balrob_fmulScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ open HolKernel Parse boolLib bossLib;
open balrob_supportLib;

open balrob_endsTheory;
open balrob_fsubTheory; (* TODO: remove this line later *)
open balrob_faddTheory; (* TODO: remove this line later *)

val _ = new_theory "balrob_fmul";

Expand Down Expand Up @@ -89,7 +91,8 @@ val balrob_summary___aeabi_fmul_c8_thm = save_thm("balrob_summary_" ^ entry_name
(* ------------------------------------ *)

(*
(* TODO: uses one jump table encoded in manually extracted cfg! takes 3 times as much time as sub or div *)
(* TODO: uses one jump table encoded in manually extracted cfg! used to take 3 times as much time as sub or div *)
(* TODO: loads constants from memory! *)
val entry_name = "__aeabi_fmul";
val reqs = get_fun_usage entry_name;
val locs =
Expand All @@ -110,7 +113,6 @@ val symb_exec_thm = birs_summary birs_prog_config
val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
*)


(* ------------------------------------ *)

val _ = print "\n";
Expand Down

0 comments on commit 5b89dc0

Please sign in to comment.