From 14cf2c5f1dee4b321005c14c36903f3dafde0f07 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 8 Jan 2021 13:22:44 +0100
Subject: [PATCH] [Kernel] normalize paths in some pretty-printed #include
directives
---
src/kernel_services/ast_printing/cil_printer.ml | 5 ++++-
tests/syntax/anon_enum_libc.c | 2 +-
tests/syntax/oracle/anon_enum_libc.res.oracle | 2 +-
3 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index eeb42506b84..93f7a11edfe 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 3c420cf6e6f..395f5dc1ea3 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 7a8098f266b..163f0857f84 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 ;
--
GitLab