diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 17:02:45 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 17:02:45 +0200 |
| commit | c3f5f3dbd088091e3fab9f357b01693932d148f8 (patch) | |
| tree | fee361b1e1cc616a1b9c412ae5cec7c9467dcf32 /extraction | |
| parent | 96165dbec88ab4c951d99e64e51f5c55a1244137 (diff) | |
| download | compcert-kvx-c3f5f3dbd088091e3fab9f357b01693932d148f8.tar.gz compcert-kvx-c3f5f3dbd088091e3fab9f357b01693932d148f8.zip | |
reloading and exploiting seems to work
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 72c19385..eb811f6c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -138,7 +138,9 @@ Extract Constant Compopts.va_strict => Extract Constant Compopts.all_loads_nontrap => "fun _ -> !Clflags.option_all_loads_nontrap". Extract Constant Compopts.profile_arcs => - "fun _ -> !Clflags.option_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". @@ -156,6 +158,9 @@ 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 => |