diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index fd438e7de134a87f511ac4711e676947853f92ed..24d8d26e36fc42e6af21e74e0925beaf910a755c 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -5936,6 +5936,11 @@ let getCompField cinfo fieldName = (fun fi -> fi.fname = fieldName) (Option.value ~default:[] cinfo.cfields) +let getCompType typ = + match unrollTypeSkel typ with + | TComp(comp,_) -> comp + | _ -> raise Not_found + let sameSizeInt ?(machdep=false) (ik1 : ikind) (ik2 : ikind) = if machdep then bytesSizeOfInt ik1 == bytesSizeOfInt ik2 else diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index 2e07fd682872d525bc099358fcd556ab91934839..83a9b53210a943b23d890b72c2337b6548c27b8b 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -658,6 +658,8 @@ val lenOfArray64: exp option -> Integer.t (** Return a named fieldinfo in compinfo, or raise Not_found *) val getCompField: compinfo -> string -> fieldinfo +(** Return the compinfo of the typ, or raise Not_found *) +val getCompType: typ -> compinfo (** A datatype to be used in conjunction with [existsType] *) type existsAction =