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

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 ->