m0/model/m0Script.sml

136 val raise'exception_def = Def
146 val rec'PRIMASK_def = Def
151 val reg'PRIMASK_def = Def
157 val write'rec'PRIMASK_def = Def
161 val write'reg'PRIMASK_def = Def
165 val rec'PSR_def = Def
174 val reg'PSR_def = Def
186 val write'rec'PSR_def = Def
190 val write'reg'PSR_def = Def
194 val rec'CONTROL_def = Def
200 val reg'CONTROL_def = Def
207 val write'rec'CONTROL_def = Def
211 val write'reg'CONTROL_def = Def
215 val rec'AIRCR_def = Def
223 val reg'AIRCR_def = Def
235 val write'rec'AIRCR_def = Def
239 val write'reg'AIRCR_def = Def
243 val rec'CCR_def = Def
251 val reg'CCR_def = Def
262 val write'rec'CCR_def = Def
266 val write'reg'CCR_def = Def
270 val rec'SHPR2_def = Def
276 val reg'SHPR2_def = Def
282 val write'rec'SHPR2_def = Def
286 val write'reg'SHPR2_def = Def
290 val rec'SHPR3_def = Def
298 val reg'SHPR3_def = Def
309 val write'rec'SHPR3_def = Def
313 val write'reg'SHPR3_def = Def
317 val rec'IPR_def = Def
329 val reg'IPR_def = Def
341 val write'rec'IPR_def = Def
345 val write'reg'IPR_def = Def
349 val ProcessorID_def = Def ("ProcessorID",AVar uTy,LI 0)
351 val ConditionPassed_def = Def
389 val Raise_def = Def
396 val CurrentModeIsPrivileged_def = Def
406 val LookUpSP_def = Def
413 val R_def = Def
434 val write'R_def = Def
469 val SP_main_def = Def
475 val write'SP_main_def = Def
486 val SP_process_def = Def
492 val write'SP_process_def = Def
503 val SP_def = Def
506 val write'SP_def = Def
514 val LR_def = Def
517 val write'LR_def = Def
525 val PC_def = Def
528 val write'PC_def = Def
539 val mem1_def = Def
546 val mem_def = Def
596 val write'mem_def = Def
668 val BigEndianReverse_def = Def
690 val Align_def = Def
695 val Aligned_def = Def
699 val MemA_def = Def
724 val write'MemA_def = Def
750 val MemU_def = Def
759 val write'MemU_def = Def
769 val ExcNumber_def = Def
781 val TakeReset_def = Def
885 val ExceptionPriority_def = Def
916 val ExecutionPriority_def = Def
1001 val ReturnAddress_def = Def
1005 val PushStack_def = Def
1529 val ExceptionTaken_def = Def
1589 val ExceptionEntry_def = Def
1602 val PopStack_def = Def
1816 val DeActivate_def = Def
1827 val IsOnes_def = Def
1830 val ExceptionActiveBitCount_def = Def
1864 val ExceptionReturn_def = Def
2071 val CallSupervisor_def = Def
2079 val BranchTo_def = Def
2085 val BranchWritePC_def = Def
2095 val BXWritePC_def = Def
2118 val BLXWritePC_def = Def
2133 val LoadWritePC_def = Def
2139 val ALUWritePC_def = Def
2146 val IncPC_def = Def
2159 val HighestSetBit_def = Def
2164 val CountLeadingZeroBits_def = Def
2170 val LowestSetBit_def = Def
2174 val BitCount_def = Def
2192 val SignExtendFrom_def = Def
2197 val Extend_def = Def
2202 val UInt_def = Def
2205 val LSL_C_def = Def
2221 val LSL_def = Def
2233 val LSR_C_def = Def
2248 val LSR_def = Def
2260 val ASR_C_def = Def
2275 val ASR_def = Def
2287 val ROR_C_def = Def
2301 val ROR_def = Def
2313 val RRX_C_def = Def
2321 val RRX_def = Def
2326 val DecodeImmShift_def = Def
2345 val DecodeRegShift_def = Def
2353 val Shift_C_def = Def
2387 val Shift_def = Def
2401 val AddWithCarry_def = Def
2418 val DataProcessingALU_def = Def
2464 val ArithmeticOpcode_def = Def
2471 val dfn'BranchTarget_def = Def
2484 val dfn'BranchExchange_def = Def
2497 val dfn'BranchLinkImmediate_def = Def
2518 val dfn'BranchLinkExchangeRegister_def = Def
2537 val DataProcessing_def = Def
2611 val DataProcessingPC_def = Def
2633 val dfn'Move_def = Def
2644 val dfn'CompareImmediate_def = Def
2655 val dfn'ArithLogicImmediate_def = Def
2669 val doRegister_def = Def
2701 val dfn'Register_def = Def
2712 val dfn'TestCompareRegister_def = Def
2722 val dfn'ShiftImmediate_def = Def
2741 val dfn'ShiftRegister_def = Def
2765 val dfn'Multiply32_def = Def
2799 val dfn'ExtendByte_def = Def
2819 val dfn'ExtendHalfword_def = Def
2839 val dfn'ByteReverse_def = Def
2860 val dfn'ByteReversePackedHalfword_def = Def
2881 val dfn'ByteReverseSignedHalfword_def = Def
2900 val dfn'LoadWord_def = Def
2936 val dfn'LoadLiteral_def = Def
2960 val dfn'LoadByte_def = Def
3000 val dfn'LoadHalf_def = Def
3040 val dfn'LoadMultiple_def = Def
3172 val dfn'StoreWord_def = Def
3205 val dfn'StoreByte_def = Def
3239 val dfn'StoreHalf_def = Def
3273 val dfn'StoreMultiple_def = Def
3374 val dfn'Push_def = Def
3460 val dfn'SupervisorCall_def = Def
3469 val dfn'ChangeProcessorState_def = Def
3489 val dfn'MoveToRegisterFromSpecial_def = Def
3599 val dfn'MoveToSpecialRegister_def = Def
3693 val dfn'Undefined_def = Def
3701 val dfn'NoOperation_def = Def
3709 val dfn'Breakpoint_def = Def
3717 val dfn'DataMemoryBarrier_def = Def
3725 val dfn'DataSynchronizationBarrier_def = Def
3733 val dfn'InstructionSynchronizationBarrier_def = Def
3741 val dfn'SendEvent_def = Def
3749 val dfn'WaitForEvent_def = Def
3757 val dfn'WaitForInterrupt_def = Def
3765 val dfn'Yield_def = Def
3773 val Run_def = Def
4035 val Fetch_def = Def
4057 val DECODE_UNPREDICTABLE_def = Def
4080 val DecodeThumb_def = Def
5335 val DecodeThumb2_def = Def
5543 val Decode_def = Def
5560 val Next_def = Def