diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 12:36:24 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 12:36:24 +0200 |
| commit | 3c30567c452f030267d0fb09465adf8d7b44a90d (patch) | |
| tree | 59d1eb891066a97580d83b60cdb160030d5ae114 /backend/Profilingaux.ml | |
| parent | 1972df30827022dcb39110cddf9032eaa3dc61b9 (diff) | |
| download | compcert-kvx-3c30567c452f030267d0fb09465adf8d7b44a90d.tar.gz compcert-kvx-3c30567c452f030267d0fb09465adf8d7b44a90d.zip | |
installed Profiling (not finished)
Diffstat (limited to 'backend/Profilingaux.ml')
| -rw-r--r-- | backend/Profilingaux.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml new file mode 100644 index 00000000..ad963a48 --- /dev/null +++ b/backend/Profilingaux.ml @@ -0,0 +1,8 @@ +open Camlcoq +open RTL + +let function_id (f : coq_function) : Z.t = + Z.of_uint 0;; + +let branch_id (f_id : Z.t) (node : P.t) = + Z.of_uint 0;; |