4 files changed, 29 insertions, 12 deletions
diff --git a/asmrun/startup.c b/asmrun/startup.c
index 644f48049..c052996e4 100644
--- a/asmrun/startup.c
+++ b/asmrun/startup.c
@@ -24,6 +24,7 @@
 #include "gc_ctrl.h"
 #include "misc.h"
 #include "mlvalues.h"
+#include "osdeps.h"
 #include "printexc.h"
 #include "sys.h"
 #ifdef HAS_UI
@@ -119,7 +120,6 @@ void caml_main(char **argv)
   char * exe_name;
 #ifdef __linux__
   static char proc_self_exe[256];
-  int retcode;
 #endif
   value res;
 
@@ -135,12 +135,8 @@ void caml_main(char **argv)
   init_signals();
   exe_name = argv[0];
 #ifdef __linux__
-  /* Recover executable name from /proc/self/exe, much more reliable */
-  retcode = readlink("/proc/self/exe", proc_self_exe, sizeof(proc_self_exe));
-  if (retcode != -1 && retcode < sizeof(proc_self_exe)) {
-    proc_self_exe[retcode] = 0;
+  if (executable_name(proc_self_exe, sizeof(proc_self_exe)) == 0)
     exe_name = proc_self_exe;
-  }
 #endif
   sys_init(exe_name, argv);
   res = caml_start_program();
diff --git a/byterun/osdeps.h b/byterun/osdeps.h
index cac3e7166..a066547f0 100644
--- a/byterun/osdeps.h
+++ b/byterun/osdeps.h
@@ -50,5 +50,10 @@ extern void * caml_dlsym(void * handle, char * name);
 /* Return an error message describing the most recent dynlink failure. */
 extern char * caml_dlerror(void);
 
+#ifdef __linux__
+/* Recover executable name from /proc/self/exe if possible */
+extern int executable_name(char * name, int name_len);
+#endif
+
 #endif
 
diff --git a/byterun/startup.c b/byterun/startup.c
index 942791d4d..dd1229560 100644
--- a/byterun/startup.c
+++ b/byterun/startup.c
@@ -322,7 +322,6 @@ CAMLexport void caml_main(char **argv)
   char * exe_name;
 #ifdef __linux__
   static char proc_self_exe[256];
-  int retcode;
 #endif
 
   /* Machine-dependent initialization of the floating-point hardware
@@ -339,12 +338,8 @@ CAMLexport void caml_main(char **argv)
   pos = 0;
   exe_name = argv[0];
 #ifdef __linux__
-  /* Recover executable name from /proc/self/exe, much more reliable */
-  retcode = readlink("/proc/self/exe", proc_self_exe, sizeof(proc_self_exe));
-  if (retcode != -1 && retcode < sizeof(proc_self_exe)) {
-    proc_self_exe[retcode] = 0;
+  if (executable_name(proc_self_exe, sizeof(proc_self_exe)) == 0)
     exe_name = proc_self_exe;
-  }
 #endif
   fd = attempt_open(&exe_name, &trail, 0);
   if (fd < 0) {
diff --git a/byterun/unix.c b/byterun/unix.c
index 465b68409..6fbf0922e 100644
--- a/byterun/unix.c
+++ b/byterun/unix.c
@@ -254,3 +254,24 @@ void aligned_munmap (char * addr, asize_t size)
 }
 
 #endif
+
+/* Recover executable name from /proc/self/exe if possible */
+
+#ifdef __linux__
+
+int executable_name(char * name, int name_len)
+{
+  int retcode;
+  struct stat st;
+
+  retcode = readlink("/proc/self/exe", name, name_len);
+  if (retcode == -1 || retcode >= name_len) return -1;
+  name[retcode] = 0;
+  /* Make sure that the contents of /proc/self/exe is a regular file.
+     (Old Linux kernels return an inode number instead.) */
+  if (stat(name, &st) != 0) return -1;
+  if (! S_ISREG(st.st_mode)) return -1;
+  return 0;
+}
+
+#endif