CompCert ARM32 uses IR12 as frame pointer?

[shenghaoyuan]

Hello, In general, ARM32 uses IR11 as the frame pointer register (i.e. FP) [1], but CompCert currently is using IR12 as FP. Considering the following implementation,

  | Pallocframe sz pos =>
      let (m1, stk) := Mem.alloc m 0 sz in
      let sp := (Vptr stk Ptrofs.zero) in
      match Mem.storev Mint32 m1 (Val.offset_ptr sp pos) rs#IR13 with
      | None => Stuck
      | Some m2 => Next (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2
      end

CompCert generates assembly code like (see Asmexpand.ml):

        mov     r12, sp
        sub     sp, sp, #sz
        str     r12, [sp, #pos]

Are there any special reasons to select IR12 instead of IR11 as FP for CompCert? (because IR11 is callee-save?) If so, btw, the comment should be r12 instead of r10

[1] https://developer.arm.com/documentation/100067/0607/armclang-Command-line-Options/-fomit-frame-pointer---fno-omit-frame-pointer