diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml index bcc1289f13c6a7a798e68741ed44afb4baa3c948..8cb7318ad076de9ae78f56378cb1b21302047795 100644 --- a/src/kernel_services/ast_data/cil_types.ml +++ b/src/kernel_services/ast_data/cil_types.ml @@ -1884,6 +1884,20 @@ type syntactic_scope = @since 27.0-Cobalt *) +let yaml_dict_to_list = function + | `O l -> + let make_one acc (k,v) = + Result.( + bind acc + (fun l -> + match Yaml.Util.to_string v with + | Ok s -> Ok((k,s) :: l) + | Error (`Msg s) -> + Error (`Msg ("Unexpected value for key " ^ k ^ ": " ^ s)))) + in + List.fold_left make_one (Ok []) l + | _ -> Error (`Msg "Unexpected YAML value instead of dictionary of strings") + (** Definition of a machine model (architecture + compiler). @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *) type mach = { @@ -1948,13 +1962,9 @@ type mach = { rand_max: string; (* expansion of RAND_MAX macro *) mb_cur_max: string; (* expansion of MB_CUR_MAX macro *) nsig: string; (* expansion of non-standard NSIG macro, empty if undefined *) - errno: (string * string) list; (* list of macros defining errors in errno.h*) + (* list of macros defining errors in errno.h*) + errno: (string * string) list [@of_yaml yaml_dict_to_list]; machdep_name: string; (* name of the machdep *) - custom_defs: (string * string) list; (* sequence of key/value for C macros *) -} - -(* -Local Variables: -compile-command: "make -C ../../.." -End: -*) + (* sequence of key/value for C macros *) + custom_defs: (string * string) list [@of_yaml yaml_dict_to_list]; +} [@@deriving yaml] diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index 7e6d6938479de23eab00f7322f5cf7fbe83293f3..43654b5253a0b8e36403cd34691da04a3e886e1f 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -314,86 +314,6 @@ let set_machdep () = let () = Cmdline.run_after_configuring_stage set_machdep -let yaml_dict_to_list = function - | `O l -> - let make_one acc (k,v) = - Result.( - bind acc - (fun l -> - match Yaml.Util.to_string v with - | Ok s -> Ok((k,s) :: l) - | Error (`Msg s) -> - Error (`Msg ("Unexpected value for key " ^ k ^ ": " ^ s)))) - in - List.fold_left make_one (Ok []) l - | _ -> Error (`Msg "Unexpected YAML value instead of dictionary of strings") - -type mach = Cil_types.mach = { - sizeof_short: int; - sizeof_int: int; - sizeof_long: int ; - sizeof_longlong: int; - sizeof_ptr: int; - sizeof_float: int; - sizeof_double: int; - sizeof_longdouble: int; - sizeof_void: int; - sizeof_fun: int; - size_t: string; - ssize_t: string; - wchar_t: string; - ptrdiff_t: string; - intptr_t: string; - uintptr_t: string; - int_fast8_t: string; - int_fast16_t: string; - int_fast32_t: string; - int_fast64_t: string; - uint_fast8_t: string; - uint_fast16_t: string; - uint_fast32_t: string; - uint_fast64_t: string; - wint_t: string; - sig_atomic_t: string; - time_t: string; - alignof_short: int; - alignof_int: int; - alignof_long: int; - alignof_longlong: int; - alignof_ptr: int; - alignof_float: int; - alignof_double: int; - alignof_longdouble: int; - alignof_str: int; - alignof_fun: int; - char_is_unsigned: bool; - little_endian: bool; - alignof_aligned: int; - has__builtin_va_list: bool; - compiler: string; - cpp_arch_flags: string list; - version: string; - weof: string; - wordsize: string; - posix_version: string; - bufsiz: string; - eof: string; - fopen_max: string; - filename_max: string; - host_name_max: string; - tty_name_max: string; - l_tmpnam: string; - path_max: string; - tmp_max: string; - rand_max: string; - mb_cur_max: string; - nsig: string; - errno: (string * string) list [@of_yaml yaml_dict_to_list]; - machdep_name: string; - custom_defs: (string * string) list [@of_yaml yaml_dict_to_list]; -} -[@@deriving yaml] - (* Local to this module. Use Cil.theMachine.theMachine outside *) let get_machdep () = let m = Kernel.Machdep.get () in @@ -404,7 +324,7 @@ let get_machdep () = let res = Result.bind (Yaml_unix.of_file (Fpath.v (file:>string))) - mach_of_yaml + Cil_types.mach_of_yaml in match res with | Ok machdep -> machdep