ARM_security_properties/model/arm_decoderScript.sml

83   and i4 n  = ( n + 3  >< n ) ireg : word4
89   let cond = i4 28 and r = i4
120               Miscellaneous (Data_Synchronization_Barrier (i4 0))
122               Miscellaneous (Data_Memory_Barrier (i4 0))
124               Miscellaneous (Instruction_Synchronization_Barrier (i4 0))
145                 (Coprocessor_Transfer_Two b20 (r 16) (r 12) (i4 8) (i4 4) (r 0))
149                    (i4 8) (i8 0))
152                 (Coprocessor_Load b24 (b 23) (b 22) (b 21) (r 16) (r 12) (i4 8)
156                 (Coprocessor_Data_Processing (i4 20) (r 16) (r 12) (i4 8)
160                 (Coprocessor_Transfer (i3 21) (b 20) (r 16) (r 12) (i4 8)
168            StatusAccess (Register_to_Status b22 (i4 16) (r 0))
179              Miscellaneous (Breakpoint (i12 8 @@ i4 0))
183            Miscellaneous (Secure_Monitor_Call (i4 0))
188            DP (i4 21) b20 (r 16) (r 12) (REG (i5 7) (i2 5) (r 0))
190            DP (i4 21) b20 (r 16) (r 12) (SHIFTED (r 8) (i2 5) (r 0))
228              (Mode3_immediate (i4 8 @@ i4 0)))
231              (Mode3_immediate (i4 8 @@ i4 0)))
246                (Mode3_immediate (i4 8 @@ i4 0))))
250                (Mode3_immediate (i4 8 @@ i4 0))))
253              (Mode3_immediate (i4 8 @@ i4 0)))
267            DataProcessing (Move_Halfword b22 (r 12) (i4 16 @@ i12 0))
272              StatusAccess (Immediate_to_Status b22 (i4 16) (i12 0))
276            DP (i4 21) b20 (r 16) (r 12) (IMM (i12 0))
305            DataProcessing (Saturate_16 b22 (i4 16) (r 12) (r 0))
348              (Coprocessor_Transfer_Two b20 (r 16) (r 12) (i4 8) (i4 4) (r 0))
350            Coprocessor (Coprocessor_Store b24 b23 b22 b21 (r 16) (r 12) (i4 8)
353            Coprocessor (Coprocessor_Load b24 b23 b22 b21 (r 16) (r 12) (i4 8)
356            Coprocessor (Coprocessor_Data_Processing (i4 20) (r 16) (r 12)
357              (i4 8) (i3 5) (r 0))
359            Coprocessor (Coprocessor_Transfer (i3 21) b20 (r 16) (r 12) (i4 8)