diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-01 16:51:47 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-01 16:51:47 +0000 |
| commit | 3ccc93675292bf9a44ac0d7111d3f44981e1f56d (patch) | |
| tree | 2879f37d1625e035f21134bc2307fce427531ce4 /extraction | |
| parent | 033aa0555a209fa3e825b1eeb8a5fc00ff8163e3 (diff) | |
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
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 3 |
1 files changed, 3 insertions, 0 deletions
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". |