summaryrefslogtreecommitdiff
path: root/cfrontend/Cil2Csyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cil2Csyntax.ml')
-rw-r--r--cfrontend/Cil2Csyntax.ml18
1 files changed, 8 insertions, 10 deletions
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index 20a5b7a..16daa14 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