From b0ce8c573c18c73d7a1c79d26381f25622b0c09a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 14 Jan 2020 18:43:56 +0100
Subject: [PATCH] [kernel] use appropriate (non-absolute) file name in assert.h
---
share/libc/assert.h | 6 +-----
src/kernel_internals/typing/cabs2cil.ml | 4 ++++
.../syntax/oracle/assert_location.res.oracle | 20 +++++++++++++++++++
3 files changed, 25 insertions(+), 5 deletions(-)
create mode 100644 tests/syntax/oracle/assert_location.res.oracle
diff --git a/share/libc/assert.h b/share/libc/assert.h
index 8d81f757525..807927b994c 100644
--- a/share/libc/assert.h
+++ b/share/libc/assert.h
@@ -42,12 +42,8 @@ __POP_FC_STDLIB
#ifdef NDEBUG
#define assert(ignore) ((void)0)
#else
-#ifndef __FC_ASSERT_FILE__
+#ifndef __FRAMAC__
#define __FC_FILENAME__ __FILE__
-#else
-#define str(a) # a
-#define xstr(a) str(a)
-#define __FC_FILENAME__ xstr(__FC_ASSERT_FILE__)
#endif
#define assert(e) (__FC_assert((e) != 0,__FC_FILENAME__,__LINE__,#e))
#endif
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f3b479e9c07..b55d8da40fe 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5636,6 +5636,10 @@ and doExp local_env
let res = new_exp ~loc (Const(CStr "exp_nothing")) in
finishExp [] (unspecified_chunk empty) res (typeOf res)
(* Do the potential lvalues first *)
+ | A.VARIABLE "__FC_FILENAME__" ->
+ let f = Filepath.Normalized.to_pretty_string (fst loc).pos_path in
+ let res = new_exp ~loc (Const(CStr f)) in
+ finishExp [] (unspecified_chunk empty) res (typeOf res)
| A.VARIABLE n -> begin
if is_stdlib_function_macro n then begin
(* These must be macros. They can be implemented with a function
diff --git a/tests/syntax/oracle/assert_location.res.oracle b/tests/syntax/oracle/assert_location.res.oracle
new file mode 100644
index 00000000000..330495a75d0
--- /dev/null
+++ b/tests/syntax/oracle/assert_location.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/syntax/assert_location.c (with preprocessing)
+/* Generated by Frama-C */
+#include "assert.h"
+void h(void)
+{
+ __FC_assert("I\'m in assert_location.h" != (char const *)0,
+ "tests/syntax/assert_location.h",4,
+ "\"I\'m in assert_location.h\"");
+ return;
+}
+
+void c(void)
+{
+ __FC_assert("I\'m in assert_location.c" != (char const *)0,
+ "tests/syntax/assert_location.c",4,
+ "\"I\'m in assert_location.c\"");
+ return;
+}
+
+
--
GitLab