Lines Matching refs:fp
167 saved_regs_list = [isR 0; isR 1; isR 2; isR 3; isR 4; isR 5; isR 6; isR 7; isR 8; isR fp; isR ip; isR lr]`;
172 MSUB R11 R12 (MC 1w)] (* sub fp ip 1 *)
286 fp | saved sp |
287 | saved fp |
642 (* We need to keep track of how sp,fp and ip are changed. *)
643 (* Note that r0-r8,fp,ip and lr are also pushed into the stack *)
857 run_cfl (BLK [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]) st)`,
880 run_cfl (BLK ((MSUB R13 R13 (MC (n2w k))) :: (APPEND (push_list l) [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]))) st)`,
895 [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++
915 `MSUB R13 R13 (MC (n2w k))::push_list (MAP conv_exp caller_i) ++ [MPUSH 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++
917 MSUB R13 R13 (MC (n2w k))::(push_list (MAP conv_exp caller_i) ++ [MPUSH 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]])
1058 [MSUB R13 R11 (MC 11w)] ++ (* sub sp fp 12 *)
1059 [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++
1203 (run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) (regs,mem) =
1263 let st' = run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st in
1305 ((run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l')) st) ''
1309 Q.ABBREV_TAC `st1 = run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st` THEN
1353 ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++
1404 Q.ABBREV_TAC `st1 = run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st` THEN
1437 (st '' isM (w2n x - 1) = st0 '' isR fp) /\ (st '' isM (w2n x - 2) = st0 '' isR 8) /\
1460 let st' = run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]))) st in
1473 `(st '' isM (w2n x) = st0 '' isR ip) /\ (st '' isM (w2n x - 1) = st0 '' isR fp)` by
1487 let st' = run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l'))) st in
1524 ((run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l'))) st) ''
1528 `w2n (read (run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st) FP) = w2n(read st0 FP)`
1572 ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list (MAP conv_exp caller_o))))
1616 ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list (MAP conv_exp caller_o)))) st
1680 [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN
1706 [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN
1734 [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN
1901 (* The values fp,ip and sp are recovered after the function call; *)