diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-19 13:19:35 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-19 13:19:35 +0000 |
| commit | fe115420b17acc722033d0df0dc354c2b841a7ab (patch) | |
| tree | 0118664ccbe182bb0dfc26f5cd4fea09c634e0a1 /checklink | |
| parent | b8633cbc90b45d57d3588491bd6da6a9e7b209f8 (diff) | |
checklink/Check.ml: missing SDA addressing for store instructions.
powerpc/PrintAsm.ml: update Linux output (Csymbol_rel, SDA sections).
test/regression/sections.c: test for SDA and relative addressings.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2571 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Check.ml | 47 |
1 files changed, 46 insertions, 1 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml index cc53f4e..a9a5f02 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -69,7 +69,7 @@ let check_st_bind atom (sym: elf32_sym): s_framework -> s_framework = let name_of_section_Linux: section_name -> string = function | Section_text -> ".text" | Section_data i -> if i then ".data" else "COMM" -| Section_small_data i -> if i then ".sdata" else "COMM" +| Section_small_data i -> if i then ".sdata" else ".sbss" | Section_const -> ".rodata" | Section_small_const -> ".sdata2" | Section_string -> ".rodata" @@ -1936,6 +1936,15 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pstb(rd, Csymbol_sda(ident, ofs), r1) -> + begin match ecode with + | STB(rS, rA, d) :: es -> + OK(fw) + >>= match_iregs rd rS + >>= check_sda ident ofs rA (exts d) + >>= recur_simpl + | _ -> error + end | Pstb(rd, cst, r1) -> begin match ecode with | STB(rS, rA, d) :: es -> @@ -1956,6 +1965,15 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pstfd(rd, Csymbol_sda(ident, ofs), r1) -> + begin match ecode with + | STFD(frS, rA, d) :: es -> + OK(fw) + >>= match_fregs rd frS + >>= check_sda ident ofs rA (exts d) + >>= recur_simpl + | _ -> error + end | Pstfd(rd, cst, r1) | Pstfd_a(rd, cst, r1) -> begin match ecode with | STFD(frS, rA, d) :: es -> @@ -1986,6 +2004,15 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pstfs(rd, Csymbol_sda(ident, ofs), r1) -> + begin match ecode with + | STFS(frS, rA, d) :: es -> + OK(fw) + >>= match_fregs rd frS + >>= check_sda ident ofs rA (exts d) + >>= recur_simpl + | _ -> error + end | Pstfs(rd, cst, r1) -> begin match ecode with | STFS(frS, rA, d) :: es -> @@ -2006,6 +2033,15 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Psth(rd, Csymbol_sda(ident, ofs), r1) -> + begin match ecode with + | STH(rS, rA, d) :: es -> + OK(fw) + >>= match_iregs rd rS + >>= check_sda ident ofs rA (exts d) + >>= recur_simpl + | _ -> error + end | Psth(rd, cst, r1) -> begin match ecode with | STH(rS, rA, d) :: es -> @@ -2036,6 +2072,15 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pstw(rd, Csymbol_sda(ident, ofs), r1) -> + begin match ecode with + | STW(rS, rA, d) :: es -> + OK(fw) + >>= match_iregs rd rS + >>= check_sda ident ofs rA (exts d) + >>= recur_simpl + | _ -> error + end | Pstw(rd, cst, r1) | Pstw_a(rd, cst, r1) -> begin match ecode with | STW(rS, rA, d) :: es -> |