From 3ccc93675292bf9a44ac0d7111d3f44981e1f56d Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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
---
 cfrontend/Cil2Csyntax.ml | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'cfrontend')

diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index b8a88deb..20a5b7a6 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -1252,3 +1252,18 @@ let atom_is_readonly a =
   with Not_found ->
     false
 
+let atom_is_small_data a ofs =
+  match Configuration.system with
+  | "linux" ->
+      if !Clflags.option_fsda then begin
+        try
+          let v = Hashtbl.find varinfo_atom a in
+          let sz = Cil.bitsSizeOf v.vtype / 8 in
+          let ofs = camlint_of_coqint ofs in
+          sz <= 8 && ofs >= 0l && ofs < Int32.of_int sz
+        with Not_found ->
+          false
+      end else
+        false
+  | _ ->
+      false
-- 
cgit