diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-06-08 08:05:41 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-06-08 08:05:41 +0000 |
commit | 0648e79b98cc8d79e1942d15dbf05ba7b9eaaa8c (patch) | |
tree | 758bdee8deb36aae7fa8ba46dd339a4f4b1a7f32 /driver | |
parent | 7c9b3828ab1d29ef50cb2c7756eadfb190804476 (diff) | |
download | compcert-0648e79b98cc8d79e1942d15dbf05ba7b9eaaa8c.tar.gz compcert-0648e79b98cc8d79e1942d15dbf05ba7b9eaaa8c.zip |
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
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Interp.ml | 10 |
1 files changed, 8 insertions, 2 deletions
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 |