diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index eeb42506b8447ad5f3219707f6508d69ddc0ba5f..93f7a11edfe9e87b21528fedf243d23d61b58396 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/src/kernel_services/ast_printing/cil_printer.ml @@ -131,7 +131,10 @@ let print_global g = let print_std_includes fmt globs = if not (Kernel.PrintLibc.get ()) then begin let extract_file acc = function - | AStr s -> Datatype.String.Set.add s acc + | AStr s -> + (* These strings are filepaths, so we normalize and prettify them *) + let s = Filepath.Normalized.(to_pretty_string (of_string s)) in + Datatype.String.Set.add s acc | _ -> Kernel.warning "Unexpected attribute parameter for fc_stdlib"; acc in let add_file acc g = diff --git a/tests/syntax/anon_enum_libc.c b/tests/syntax/anon_enum_libc.c index 3c420cf6e6fe62b7f6becb62555d2708a710c471..395f5dc1ea3bdedb2a14f7a463bc8cbe03f09871 100644 --- a/tests/syntax/anon_enum_libc.c +++ b/tests/syntax/anon_enum_libc.c @@ -1,5 +1,5 @@ /* run.config -FILTER: sed -e 's|#include *"\([^/]*[/]\)*\([^/]*\)"|#include "PTESTS_DIR/\2"|' + OPT: -cpp-extra-args="-I @PTEST_DIR@" -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -ocode="" @PTEST_DIR@/result/@PTEST_NAME@.c -print */ diff --git a/tests/syntax/oracle/anon_enum_libc.res.oracle b/tests/syntax/oracle/anon_enum_libc.res.oracle index 7a8098f266bdd68a621604cce083c1cd2619aaa8..163f0857f8473958e0d7acb027c5e4eae18f20e2 100644 --- a/tests/syntax/oracle/anon_enum_libc.res.oracle +++ b/tests/syntax/oracle/anon_enum_libc.res.oracle @@ -1,7 +1,7 @@ [kernel] Parsing tests/syntax/anon_enum_libc.c (with preprocessing) [kernel] Parsing tests/syntax/result/anon_enum_libc.c (with preprocessing) /* Generated by Frama-C */ -#include "PTESTS_DIR/anon_enum_libc.h" +#include "tests/syntax/anon_enum_libc.h" struct __anonstruct_s1_1 { int x ; float y ;