Lines Matching refs:Call
159 Call("reg'PRIMASK",F32,Var("x",CTy"PRIMASK")))
163 Call("rec'PRIMASK",CTy"PRIMASK",Var("x",F32)))
188 Call("reg'PSR",F32,Var("x",CTy"PSR")))
192 Call("rec'PSR",CTy"PSR",Var("x",F32)))
209 Call("reg'CONTROL",FTy 3,Var("x",CTy"CONTROL")))
213 Call("rec'CONTROL",CTy"CONTROL",Var("x",FTy 3)))
237 Call("reg'AIRCR",F32,Var("x",CTy"AIRCR")))
241 Call("rec'AIRCR",CTy"AIRCR",Var("x",F32)))
264 Call("reg'CCR",F32,Var("x",CTy"CCR")))
268 Call("rec'CCR",CTy"CCR",Var("x",F32)))
284 Call("reg'SHPR2",F32,Var("x",CTy"SHPR2")))
288 Call("rec'SHPR2",CTy"SHPR2",Var("x",F32)))
311 Call("reg'SHPR3",F32,Var("x",CTy"SHPR3")))
315 Call("rec'SHPR3",CTy"SHPR3",Var("x",F32)))
343 Call("reg'IPR",F32,Var("x",CTy"IPR")))
347 Call("rec'IPR",CTy"IPR",Var("x",F32)))
429 Apply(Call("LookUpSP",ATy(qTy,CTy"RName"),LU),qVar"state")))],
441 (Call
443 Call("ASSERT",CTy"exception",LS"n >= 0 and n <= 14")),
459 (Call("LookUpSP",ATy(qTy,CTy"RName"),LU),
504 ("SP",qVar"state",Apply(Call("R",ATy(qTy,F32),LW(13,4)),qVar"state"))
511 (Call("write'R",ATy(qTy,qTy),TP[Var("value",F32),LW(13,4)]),
515 ("LR",qVar"state",Apply(Call("R",ATy(qTy,F32),LW(14,4)),qVar"state"))
522 (Call("write'R",ATy(qTy,qTy),TP[Var("value",F32),LW(14,4)]),
526 ("PC",qVar"state",Apply(Call("R",ATy(qTy,F32),LW(15,4)),qVar"state"))
553 (Call
559 (Call
564 (Call
570 (Call
575 (Call
580 (Call
585 (Call
591 (Call
593 Call("ASSERT",CTy"exception",LS"mem: size in {1, 2, 4}")),
662 (Call
664 Call
684 (Call
686 Call
697 EQ(Var("w",BTy"N"),Call("Align",BTy"N",TP[Var("w",BTy"N"),nVar"n"])))
703 ITE(Mop(Not,Call("Aligned",bTy,TP[Var("address",F32),nVar"size"])),
706 (Call
711 (Call
718 (Call
728 ITE(Mop(Not,Call("Aligned",bTy,TP[Var("address",F32),nVar"size"])),
730 (Call
739 (Call
746 (Call
755 (Call
764 (Call
778 (Call("ExternalInterrupt",CTy"ARM_Exception",Var("n",FTy 6)),
788 (Call("MemA",ATy(qTy,PTy(F32,qTy)),TP[Var("v",F32),LN 4]),
798 (Call
805 (Call
809 (Call("write'LR",ATy(qTy,qTy),LX F32),
811 (Call
815 (Call
824 (Call
947 (Call
1039 (Call
1091 (Call
1128 (Call("R",ATy(qTy,F32),LW(0,4)),
1141 (Call
1156 (Call("R",ATy(qTy,F32),LW(1,4)),
1171 (Call
1190 (Call
1209 (Call
1231 (Call
1254 (Call
1279 (Call
1305 (Call
1362 (Call
1392 (Call
1427 (Call
1447 (Call
1450 TP[CC[EX(Call
1470 EX(Call
1504 (Call
1517 (Call
1523 (Call
1535 (Call
1542 (Call("write'R",ATy(qTy,qTy),TP[LX F32,LW(12,4)]),
1552 (Call
1563 (Call("write'PC",ATy(qTy,qTy),Var("v",F32)),
1596 (Call
1598 Call("ExcNumber",FTy 6,Var("e",CTy"ARM_Exception"))),
1599 Apply(Call("PushStack",ATy(qTy,qTy),LU),qVar"state"))),
1608 (Call
1613 (Call
1617 (Call("write'R",ATy(qTy,qTy),TP[Var("v",F32),LW(0,4)]),
1621 (Call
1625 (Call
1630 (Call
1634 (Call
1639 (Call
1644 (Call
1649 (Call
1654 (Call
1659 (Call
1664 (Call
1669 (Call
1675 (Call
1696 (Call
1717 (Call
1739 Call
1753 Call
1764 Call
1782 Call
1792 Call
1808 Call
1874 (Call
1876 Call
1882 Call
1887 (Call
1889 Call
1897 (Call
1907 (Call
1910 Call
1920 (Call
1923 Call
1952 (Call
1955 Call
1984 (Call
1987 Call
2015 (Call
2018 Call
2025 (Call
2030 (Call
2045 (Call
2048 Call
2062 (Call
2065 Call
2076 (Call("Raise",ATy(qTy,qTy),Const("SVCall",CTy"ARM_Exception")),
2083 Apply(Call("write'PC",ATy(qTy,qTy),Var("address",F32)),qVar"state")))
2090 (Call
2104 (Call
2108 (Call
2113 (Call
2123 (Call
2128 (Call
2137 Apply(Call("BXWritePC",ATy(qTy,qTy),Var("address",F32)),qVar"state")))
2144 (Call("BranchWritePC",ATy(qTy,qTy),Var("address",F32)),qVar"state")))
2151 (Call
2168 Call("HighestSetBit",iTy,Var("w",BTy"N")))))
2172 Call("CountLeadingZeroBits",nTy,Mop(Rev,Var("w",BTy"N"))))
2216 (Call
2218 Call("ASSERT",CTy"exception",LS"LSL_C")),
2228 (Call
2243 (Call
2245 Call("ASSERT",CTy"exception",LS"LSR_C")),
2255 (Call
2270 (Call
2272 Call("ASSERT",CTy"exception",LS"ASR_C")),
2282 (Call
2296 (Call
2298 Call("ASSERT",CTy"exception",LS"ROR_C")),
2308 (Call
2324 Call("RRX_C",PTy(BTy"N",bTy),TP[Var("x",BTy"N"),bVar"carry_in"])))
2364 (Call
2369 (Call
2374 (Call
2379 (Call
2383 TP[Call
2395 (Call
2427 Call
2431 Call
2435 Call
2439 Call
2443 Call
2447 Call
2451 Call
2455 Call
2477 (Call
2490 (Call
2492 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state")),
2504 (Call
2511 (Call
2524 (Call
2526 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state")),
2528 (Call
2544 Call
2552 Call
2556 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state")),
2561 (Call
2567 (Call("IncPC",ATy(qTy,qTy),LU),
2594 ITE(Call
2617 Call
2623 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state")),
2627 (Call("ALUWritePC",ATy(qTy,qTy),Var("result",F32)),
2638 (Call
2649 (Call
2662 (Call
2677 (Call
2679 TP[Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
2685 ITE(Call("ArithmeticOpcode",bTy,Var("opc",F4)),
2690 (Call
2695 (Call
2707 (Call
2717 (Call
2730 (Call
2736 (Call
2748 (Call
2750 TP[Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"),
2754 (Call("R",ATy(qTy,F32),Var("m",F4)),
2760 (Call
2770 Bop(Mul,Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"),
2771 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state")),
2774 (Call("write'R",ATy(qTy,qTy),TP[Var("v",F32),Var("d",F4)]),
2786 (Call("IncPC",ATy(qTy,qTy),LU),
2805 (Call("IncPC",ATy(qTy,qTy),LU),
2807 (Call
2809 TP[Call
2813 (Call("R",ATy(qTy,F32),Var("m",F4)),
2825 (Call("IncPC",ATy(qTy,qTy),LU),
2827 (Call
2829 TP[Call
2833 (Call("R",ATy(qTy,F32),Var("m",F4)),
2844 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
2847 (Call("IncPC",ATy(qTy,qTy),LU),
2849 (Call
2865 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
2868 (Call("IncPC",ATy(qTy,qTy),LU),
2870 (Call
2886 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
2889 (Call("IncPC",ATy(qTy,qTy),LU),
2891 (Call
2906 [(Call("register_form",CTy"offset",Var("m",F4)),
2908 (Call
2911 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
2915 (Call("immediate_form",CTy"offset",Var("imm32",F32)),
2919 (Call
2923 (Call("R",ATy(qTy,F32),Var("n",F4)),qVar"s"),
2927 (Call("IncPC",ATy(qTy,qTy),LU),
2929 (Call
2942 (Call
2945 Call
2951 (Call("IncPC",ATy(qTy,qTy),LU),
2953 (Call
2967 [(Call("register_form",CTy"offset",Var("m",F4)),
2969 (Call
2972 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
2976 (Call("immediate_form",CTy"offset",Var("imm32",F32)),
2980 (Call
2984 (Call("R",ATy(qTy,F32),Var("n",F4)),qVar"s"),
2988 (Call("IncPC",ATy(qTy,qTy),LU),
2990 (Call
2992 TP[Call
3007 [(Call("register_form",CTy"offset",Var("m",F4)),
3009 (Call
3012 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
3016 (Call("immediate_form",CTy"offset",Var("imm32",F32)),
3020 (Call
3024 (Call("R",ATy(qTy,F32),Var("n",F4)),qVar"s"),
3028 (Call("IncPC",ATy(qTy,qTy),LU),
3030 (Call
3032 TP[Call
3045 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"),
3046 Let(nVar"bitcount",Call("BitCount",nTy,Var("registers",FTy 9)),
3064 (Call
3095 (Call
3119 (Call
3131 (Call
3148 (Call("IncPC",ATy(qTy,qTy),LU),
3163 (Call
3178 [(Call("register_form",CTy"offset",Var("m",F4)),
3180 (Call
3183 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
3187 (Call("immediate_form",CTy"offset",Var("imm32",F32)),
3191 (Call("IncPC",ATy(qTy,qTy),LU),
3193 (Call
3196 (Call("R",ATy(qTy,F32),Var("t",F4)),qVar"s"),
3199 (Call("R",ATy(qTy,F32),Var("n",F4)),
3211 [(Call("register_form",CTy"offset",Var("m",F4)),
3213 (Call
3216 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
3220 (Call("immediate_form",CTy"offset",Var("imm32",F32)),
3224 (Call("IncPC",ATy(qTy,qTy),LU),
3226 (Call
3229 (Call("R",ATy(qTy,F32),Var("t",F4)),qVar"s"),
3233 (Call("R",ATy(qTy,F32),Var("n",F4)),
3245 [(Call("register_form",CTy"offset",Var("m",F4)),
3247 (Call
3250 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"),
3254 (Call("immediate_form",CTy"offset",Var("imm32",F32)),
3258 (Call("IncPC",ATy(qTy,qTy),LU),
3260 (Call
3263 (Call("R",ATy(qTy,F32),Var("t",F4)),qVar"s"),
3267 (Call("R",ATy(qTy,F32),Var("n",F4)),
3278 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"),
3279 Let(nVar"bitcount",Call("BitCount",nTy,Var("registers",F8)),
3282 (Call("IncPC",ATy(qTy,qTy),LU),
3284 (Call
3316 Call
3322 (Call
3338 (Call
3343 (Call
3379 Let(nVar"bitcount",Call("BitCount",nTy,Var("registers",FTy 9)),
3384 (Call("IncPC",ATy(qTy,qTy),LU),
3386 (Call
3410 (Call
3427 (Call
3465 Apply(Call("CallSupervisor",ATy(qTy,qTy),LU),qVar"state"),
3475 (Call("IncPC",ATy(qTy,qTy),LU),
3477 (Call("CurrentModeIsPrivileged",ATy(qTy,bTy),LU),
3495 (Call("write'R",ATy(qTy,qTy),TP[LW(0,32),Var("d",F4)]),
3499 (Call("IncPC",ATy(qTy,qTy),LU),
3505 (Call
3508 EX(Call
3514 (Call
3521 (Call
3526 (Call
3532 (Call
3535 EX(Call
3542 (Call
3550 (Call
3557 (Call
3567 (Call
3577 (Call
3582 (Call
3585 EX(Call
3591 (Call
3604 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"),
3607 (Call("IncPC",ATy(qTy,qTy),LU),
3614 Call
3620 Call
3627 (Call
3633 (Call
3639 (Call
3646 (Call
3698 (Call("Raise",ATy(qTy,qTy),Const("HardFault",CTy"ARM_Exception")),
3705 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3713 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3721 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3729 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3737 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3745 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3753 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3761 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3769 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"),
3778 [(Call("NoOperation",CTy"instruction",uVar"v48"),
3780 (Call("dfn'NoOperation",ATy(qTy,qTy),uVar"v48"),qVar"state")),
3781 (Call("Undefined",CTy"instruction",Var("v49",F32)),
3783 (Call("dfn'Undefined",ATy(qTy,qTy),Var("v49",F32)),
3785 (Call("Branch",CTy"instruction",Var("v1",CTy"Branch")),
3787 [(Call("BranchExchange",CTy"Branch",Var("v2",F4)),
3789 (Call("dfn'BranchExchange",ATy(qTy,qTy),Var("v2",F4)),
3791 (Call
3794 (Call
3797 (Call("BranchLinkImmediate",CTy"Branch",Var("v4",F32)),
3799 (Call
3802 (Call("BranchTarget",CTy"Branch",Var("v5",F32)),
3804 (Call("dfn'BranchTarget",ATy(qTy,qTy),Var("v5",F32)),
3806 (Call("Data",CTy"instruction",Var("v6",CTy"Data")),
3808 [(Call
3812 (Call
3816 (Call("CompareImmediate",CTy"Data",Var("v8",PTy(F4,F32))),
3818 (Call
3821 (Call("Move",CTy"Data",Var("v9",PTy(F4,F32))),
3823 (Call("dfn'Move",ATy(qTy,qTy),Var("v9",PTy(F4,F32))),
3825 (Call
3829 (Call
3833 (Call
3839 (Call
3845 (Call
3849 (Call
3853 (Call
3857 (Call
3860 (Call("Hint",CTy"instruction",Var("v14",CTy"Hint")),
3862 [(Call("Breakpoint",CTy"Hint",Var("v15",F32)),
3864 (Call("dfn'Breakpoint",ATy(qTy,qTy),Var("v15",F32)),
3866 (Call("DataMemoryBarrier",CTy"Hint",Var("v16",F4)),
3868 (Call
3871 (Call("DataSynchronizationBarrier",CTy"Hint",Var("v17",F4)),
3873 (Call
3876 (Call
3880 (Call
3883 (Call("SendEvent",CTy"Hint",uVar"v19"),
3885 (Call("dfn'SendEvent",ATy(qTy,qTy),uVar"v19"),
3887 (Call("WaitForEvent",CTy"Hint",uVar"v20"),
3889 (Call("dfn'WaitForEvent",ATy(qTy,qTy),uVar"v20"),
3891 (Call("WaitForInterrupt",CTy"Hint",uVar"v21"),
3893 (Call("dfn'WaitForInterrupt",ATy(qTy,qTy),uVar"v21"),
3895 (Call("Yield",CTy"Hint",uVar"v22"),
3897 (Call("dfn'Yield",ATy(qTy,qTy),uVar"v22"),qVar"state"))])),
3898 (Call("Load",CTy"instruction",Var("v23",CTy"Load")),
3900 [(Call
3904 (Call
3908 (Call
3912 (Call
3916 (Call("LoadLiteral",CTy"Load",Var("v26",PTy(F4,F32))),
3918 (Call
3921 (Call
3925 (Call
3928 (Call
3932 (Call
3935 (Call("Media",CTy"instruction",Var("v29",CTy"Media")),
3937 [(Call("ByteReverse",CTy"Media",Var("v30",PTy(F4,F4))),
3939 (Call
3942 (Call
3946 (Call
3949 (Call
3953 (Call
3956 (Call
3959 (Call
3962 (Call
3966 (Call
3969 (Call("Multiply",CTy"instruction",Var("v35",CTy"Multiply")),
3971 [(Call
3975 (Call
3978 (Call("Store",CTy"instruction",Var("v37",CTy"Store")),
3980 [(Call("Push",CTy"Store",Var("v38",FTy 9)),
3982 (Call("dfn'Push",ATy(qTy,qTy),Var("v38",FTy 9)),
3984 (Call
3988 (Call
3991 (Call
3995 (Call
3998 (Call("StoreMultiple",CTy"Store",Var("v41",PTy(F4,F8))),
4000 (Call
4003 (Call
4007 (Call
4010 (Call("System",CTy"instruction",Var("v43",CTy"System")),
4012 [(Call("ChangeProcessorState",CTy"System",bVar"v44"),
4014 (Call("dfn'ChangeProcessorState",ATy(qTy,qTy),bVar"v44"),
4016 (Call
4020 (Call
4023 (Call
4027 (Call
4030 (Call("SupervisorCall",CTy"System",Var("v47",F32)),
4032 (Call("dfn'SupervisorCall",ATy(qTy,qTy),Var("v47",F32)),
4043 (Call("MemA",ATy(qTy,PTy(F16,qTy)),TP[Var("v",F32),LN 2]),
4049 (Call
4052 TP[Call
4055 TP[Call("Thumb",CTy"MachineCode",Var("v0",F16)),qVar"s"]))))
4063 (Call
4065 Call
4069 [(Call("Thumb",CTy"MachineCode",Var("opc",F16)),
4072 (Call
4085 Call("Thumb",CTy"MachineCode",Var("h",F16)),
4094 TP[Call
4096 Call
4126 TP[Call
4128 Call
4154 TP[Call
4156 Call
4177 TP[Call
4179 Call
4202 TP[Call
4204 Call
4208 Call
4213 (Call
4233 TP[Call
4235 Call
4257 Call
4260 Call
4270 Call
4273 Call
4283 Call
4286 Call
4296 Call
4311 TP[Call
4313 Call
4318 Call
4323 (Call
4337 Call
4339 Call
4373 Call
4375 Call("Yield",CTy"Hint",LU))),
4377 Call
4379 Call
4383 Call
4385 Call
4389 Call
4391 Call
4394 Call
4400 Call
4402 Call
4418 Call
4429 Call
4441 Call
4443 Call
4451 Call
4453 Call
4466 Call
4477 Call
4479 Call
4485 Call
4487 Call
4502 TP[Call
4504 Call
4512 Call
4516 (Call
4534 TP[Call
4536 Call
4547 Call
4552 (Call
4565 Call
4579 Call
4581 Call
4591 (Call
4597 Call
4599 Call
4612 Call
4614 Call("Undefined",CTy"instruction",LW(0,32))),
4636 Call
4639 Call
4652 Call
4655 Call
4668 Call
4671 Call
4684 Call
4687 Call
4700 Call
4703 Call
4716 Call
4719 Call
4732 Call
4735 Call
4740 Call
4757 Call
4760 Call
4765 Call
4782 Call
4785 Call
4790 Call
4807 Call
4810 Call
4821 Call
4823 Call
4833 Call
4835 Call
4845 Call
4847 Call
4857 Call
4859 Call
4872 Call
4875 Call
4884 Call
4886 Call
4912 TP[Call
4914 Call
4921 (Call
4942 TP[Call
4944 Call
4959 (Call
4972 TP[Call
4974 Call
4993 TP[Call
4995 Call
5006 TP[Call
5008 Call
5016 TP[Call
5018 Call
5039 Call
5049 Call
5051 Call
5060 Call
5062 Call
5071 Call
5073 Call
5082 Call
5084 Call
5093 Call
5095 Call
5103 Call
5105 Call
5114 Call
5116 Call
5125 Call
5127 Call
5144 Call
5156 Call
5158 Call
5165 Call
5167 Call
5183 Call
5193 Call
5195 Call
5203 Call
5205 Call
5213 TP[Call("Undefined",CTy"instruction",LW(0,32)),
5218 Call
5220 Call
5239 Call
5241 Call
5259 Call
5266 Call
5268 Call
5284 Call
5286 Call
5300 Call
5302 Call
5319 Call
5321 Call
5332 Call("Undefined",CTy"instruction",LW(0,32))),
5340 Call("Thumb2",CTy"MachineCode",Var("h",PTy(F16,F16))),
5374 TP[Call
5376 Call
5393 (Call
5416 Call
5418 Call
5422 Call
5424 Call
5428 Call
5430 Call
5434 Call
5455 TP[Call
5457 Call
5474 (Call
5494 TP[Call
5508 TP[Call
5510 Call
5538 TP[Call("Undefined",CTy"instruction",LW(0,32)),
5540 TP[Call("Undefined",CTy"instruction",LW(0,32)),
5548 [(Call("Thumb",CTy"MachineCode",Var("h",F16)),
5550 (Call
5553 (Call("Thumb2",CTy"MachineCode",Var("hs",PTy(F16,F16))),
5555 (Call
5567 (Call
5571 (Call("Run",ATy(qTy,qTy),Var("v",CTy"instruction")),qVar"s"))))