diff options
Diffstat (limited to 'cfrontend/Cil2Csyntax.ml')
-rw-r--r-- | cfrontend/Cil2Csyntax.ml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml index b8a88de..20a5b7a 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 |