From 0648e79b98cc8d79e1942d15dbf05ba7b9eaaa8c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 8 Jun 2013 08:05:41 +0000
Subject: More precise and faster recovery of function name from function or
 fundef value.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 driver/Interp.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'driver/Interp.ml')

diff --git a/driver/Interp.ml b/driver/Interp.ml
index 25c8b30e..662baa24 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -86,13 +86,19 @@ let name_of_fundef prog fd =
   let rec find_name = function
   | [] -> "<unknown function>"
   | (id, Gfun fd') :: rem ->
-      if fd = fd' then extern_atom id else find_name rem
+      if fd == fd' then extern_atom id else find_name rem
   | (id, Gvar v) :: rem ->
       find_name rem
   in find_name prog.prog_defs
 
 let name_of_function prog fn =
-  name_of_fundef prog (Internal fn)
+  let rec find_name = function
+  | [] -> "<unknown function>"
+  | (id, Gfun(Internal fn')) :: rem ->
+      if fn == fn' then extern_atom id else find_name rem
+  | (id, _) :: rem ->
+      find_name rem
+  in find_name prog.prog_defs
 
 let invert_local_variable e b =
   Maps.PTree.fold 
-- 
cgit