From 3ccc93675292bf9a44ac0d7111d3f44981e1f56d Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 1 Nov 2009 16:51:47 +0000 Subject: Preliminary support for small data area in PowerPC port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 4eb107b..f8a159b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -72,6 +72,9 @@ Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". (* Asm *) Extract Constant Asm.low_half => "fun _ -> assert false". Extract Constant Asm.high_half => "fun _ -> assert false". +Extract Constant Asm.symbol_is_small_data => "Cil2Csyntax.atom_is_small_data". +Extract Constant Asm.small_data_area_base => "fun _ -> assert false". +Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false". (* Suppression of stupidly big equality functions *) Extract Constant Op.eq_operation => "fun (x: operation) (y: operation) -> x = y". -- cgit v1.2.3