diff options
Diffstat (limited to 'cfrontend/Cil2Csyntax.ml')
-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 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 |