diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-02 10:42:56 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-02 10:42:56 +0000 |
commit | 5d84e6862562eb14fe489c297864e660ace12418 (patch) | |
tree | bbe3828bd4da0eec12a91c788e13051d00a4e7cd /cfrontend | |
parent | 3ccc93675292bf9a44ac0d7111d3f44981e1f56d (diff) | |
download | compcert-5d84e6862562eb14fe489c297864e660ace12418.tar.gz compcert-5d84e6862562eb14fe489c297864e660ace12418.zip |
Simplified the treatment of the PowerPC small data area; now more specific to the Diab toolchain.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1165 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cil2Csyntax.ml | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml index 20a5b7a6..16daa141 100644 --- a/cfrontend/Cil2Csyntax.ml +++ b/cfrontend/Cil2Csyntax.ml @@ -1254,16 +1254,14 @@ let atom_is_readonly a = 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 + | "diab" -> + 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 | _ -> false |