Comment 10 for bug 2063340

there could be something else going on such as linker or C preprocessor tricks.

I wrote a test on a known-good 32-bit arm setup showing that passing 64-bit int seems ok.
Specifically I compiled this C function into the SBCL runtime:
int faketime(int ignore, unsigned int* foo)
{
  printf("Hi in faketime, ptr=%p\n", foo);
  // low part // high part
  foo[0] = 0x669f365d; foo[1] = 0x76543210;
  foo[2] = 0x2f530d4a; foo[3] = 0;
  return 0;
}
and then evaluated:
* (define-alien-type nil
  (struct mock-timespec
          (tv-sec (signed 64))
          (tv-nsec (signed 32))
          (pad (signed 32))))
NIL
* (defun tryit ()
    (with-alien ((ts (struct mock-timespec)))
      (alien-funcall (extern-alien "faketime"
                                   (function int int (* (struct mock-timespec))))
                     0 (addr ts))
      (format t "~x ~x ~x~%"
              (slot ts 'tv-sec)
              (slot ts 'tv-nsec)
              (slot ts 'pad))))
TRYIT
* (tryit)
Hi in faketime, ptr=0xffeda188
76543210669F365D 2F530D4A 0

I'm am the end of the road in terms of being able to help you debug.