diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index fc906631..b40d444a 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -154,6 +154,10 @@ Extract Constant Compopts.va_strict => "fun _ -> false". Extract Constant Compopts.all_loads_nontrap => "fun _ -> !Clflags.option_all_loads_nontrap". +Extract Constant Compopts.profile_arcs => +"fun _ -> !Clflags.option_profile_arcs". +Extract Constant Compopts.branch_probabilities => + "fun _ -> !Clflags.option_fbranch_probabilities". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". @@ -164,9 +168,17 @@ Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". Extract Constant Compiler.time => "Timing.time_coq". Extract Constant Compopts.time => "Timing.time_coq". - (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) +(* Profiling *) +Extract Constant AST.profiling_id => "Digest.t". +Extract Constant AST.profiling_id_eq => "Digest.equal". +Extract Constant Profiling.function_id => "Profilingaux.function_id". +Extract Constant Profiling.branch_id => "Profilingaux.branch_id". +Extract Constant ProfilingExploit.function_id => "Profilingaux.function_id". +Extract Constant ProfilingExploit.branch_id => "Profilingaux.branch_id". +Extract Constant ProfilingExploit.condition_oracle => "Profilingaux.condition_oracle". + (* Cabs *) Extract Constant Cabs.loc => "{ lineno : int; |