diff options
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;; |