gistfile1.txt

0001010c <f1>:
   1010c:       e92d4800        push    {fp, lr}
   10110:       e28db004        add     fp, sp, #4
   10114:       e24dd008        sub     sp, sp, #8
   10118:       e50b0008        str     r0, [fp, #-8]
   1011c:       e51b3008        ldr     r3, [fp, #-8]
   10120:       e2833001        add     r3, r3, #1
   10124:       e1a00003        mov     r0, r3
   10128:       ebffffea        bl      100d8 <f2>
   1012c:       e1a00000        nop                     ; (mov r0, r0)
   10130:       e24bd004        sub     sp, fp, #4
   10134:       e8bd8800        pop     {fp, pc}


0x1012c:
  
  # 0x1012c 0x1012c: MOV_r_A1(xxx0xxxx.xxxxxxxx.1010OOOO.xxxx0001) Rd 0, Rm 0, S 0, cond 14, imm5 0, type1 0, QuasiMask0 QuasiMask"("4): 0
  # 0x1012c: MOV_r_A1(xxx0xxxx.xxxxxxxx.1010OOOO.xxxx0001) Rd 0, Rm 0, S 0, cond 14, imm5 0, type1 0, QuasiMask0 QuasiMask"("4): 0
  # 0x1012c: {PSTATE_T => 0x0 :: [1]
             ;_PC => 0x10130
             ;_R0 => _R0_0
             ;__AssertionFailure => false
             ;__BranchTaken => false}
  # 0x10130 0x10130: SUB_i_A1(xxxxxxxx.xxxxxxxx.0100xxxx.xxxx0010) Rd 13, Rn 11, S 0, cond 14, imm12 4
  # 0x10130: SUB_i_A1(xxxxxxxx.xxxxxxxx.0100xxxx.xxxx0010) Rd 13, Rn 11, S 0, cond 14, imm12 4
  r2085 := (uext _R11_0 65)
  r2087 := (bv_add r2085 (0xfffffffc :: [65]))
  r2088 := (trunc r2087 32)
  # 0x10130: {PSTATE_T => 0x0 :: [1]
             ;_PC => 0x10134
             ;_R0 => _R0_0
             ;_R13 => r2088
             ;__AssertionFailure => true
             ;__BranchTaken => false
             ;__UndefinedBehavior => false}
  # 0x10134 0x10134: LDM_A1(xxxxxxxx.xxxxxxxx.10x1xxxx.xxxx1000) Rn 13, W 1, cond 14, register_list 34816
  # 0x10134: LDM_A1(xxxxxxxx.xxxxxxxx.10x1xxxx.xxxx1000) Rn 13, W 1, cond 14, register_list 34816
  r2157 := (bv_add r2088 (0x4 :: [32]))
  r2161 := read_mem r2157 (bvle4)
  r2162 := (bv_and r2161 (0x1 :: [32]))
  r2163 := (trunc r2162 1)
  r2164 := (eq r2163 (0x1 :: [1]))
  r2165 := (mux r2164 (0x1 :: [1]) (0x0 :: [1]))
  r2186 := (bv_add r2088 (0x4 :: [32]))
  r2190 := read_mem r2186 (bvle4)
  r2201 := read_mem r2088 (bvle4)
  r2203 := read_mem r2088 (bvle4)
  r2205 := read_mem r2088 (bvle4)
  r2207 := read_mem r2088 (bvle4)
  r2209 := read_mem r2088 (bvle4)
  r2211 := read_mem r2088 (bvle4)
  r2213 := read_mem r2088 (bvle4)
  r2215 := read_mem r2088 (bvle4)
  r2217 := read_mem r2088 (bvle4)
  r2219 := read_mem r2088 (bvle4)
  r2221 := read_mem r2088 (bvle4)
  r2223 := read_mem r2088 (bvle4)
  r2224 := (bv_add r2088 (0x4 :: [32]))
  r2225 := read_mem r2224 (bvle4)
  r2227 := read_mem r2224 (bvle4)
  r2229 := read_mem r2224 (bvle4)
  r2231 := read_mem r2224 (bvle4)
  r2240 := (bv_add r2088 (0x8 :: [32]))
  r2262 := (bv_add r2088 (0xc :: [32]))
  r2266 := read_mem r2262 (bvle4)
  # 0x10134: {PSTATE_T => r2165
             ;_PC => r2190
             ;_R0 => _R0_0
             ;_R11 => r2223
             ;_R13 => r2240
             ;__AssertionFailure => true
             ;__BranchTaken => true
             ;__UnpredictableBehavior => false}
  classify failure
    { PSTATE_IT = 0x0 :: [8]
    , PSTATE_T = r2165
    , PSTATE_nRW = 0x1 :: [1]
    , _PC = r2190
    , _R11 = r2223
    , _R13 = r2240
    , __AssertionFailure = true
    , __BranchTaken = true
    , __PendingInterrupt = false
    , __PendingPhysicalSError = false
    , __Sleeping = false
    , __UndefinedBehavior = false
    , __UnpredictableBehavior = false
    }
    Branch: IP is not an mux:
let r2085 := (uext _R11_0 65)
    r2087 := (bv_add r2085 (0xfffffffc :: [65]))
    r2088 := (trunc r2087 32)
    r2186 := (bv_add r2088 (0x4 :: [32]))
    r2190 := read_mem r2186 (bvle4)
 in r2190