diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-18 12:34:43 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-18 12:34:43 +0000 |
| commit | 71a8a9586078c0132aa326a8c7968d38fe25a78d (patch) | |
| tree | 391a3726e1152e499bfb1e52e9d29cbdb342a40a /powerpc/extractionMachdep.v | |
| parent | 940ebe1a61a4e2ce9a564520339f6499a767dcc8 (diff) | |
| download | compcert-kvx-71a8a9586078c0132aa326a8c7968d38fe25a78d.tar.gz compcert-kvx-71a8a9586078c0132aa326a8c7968d38fe25a78d.zip | |
powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.
powerpc/Asmgen*: simplify the code generated for far-data relative
accesses, so that the only occurrences of Csymbol_rel_{low,high}
are in the pattern
Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...)
checklink/Check.ml: check the pattern above.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/extractionMachdep.v')
| -rw-r--r-- | powerpc/extractionMachdep.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index 352d3b54..b448e3d2 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -13,8 +13,8 @@ (* Additional extraction directives specific to the PowerPC port *) (* Asm *) -Extract Constant Asm.low_half => "fun _ -> assert false". -Extract Constant Asm.high_half => "fun _ -> assert false". +Extract Constant Asm.low_half => "fun _ _ _ -> assert false". +Extract Constant Asm.high_half => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_is_small_data => "C2C.atom_is_small_data". Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data". |