diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml index 144bb0d584ce4a8f61d9195bd7e4960bd2af9055..a30ae3abc13942f68e214f7130af5d1de15e01fc 100644 --- a/src/kernel_services/ast_printing/cil_types_debug.ml +++ b/src/kernel_services/ast_printing/cil_types_debug.ml @@ -607,7 +607,8 @@ and pp_location fmt (pos_start,pos_end) = p fmt "(%a,%a)" pp_filepath_position pos_start pp_filepath_position pos_end and pp_if_loc_known prefix suffix fmt loc = - if print_locations && loc <> Cil_datatype.Location.unknown + if print_locations && + not (Filepath.Normalized.is_unknown (fst loc).Filepath.pos_path) then Format.fprintf fmt "%s%a%s" prefix pp_location loc suffix else ()