diff --git a/share/libc/assert.h b/share/libc/assert.h index 8d81f75752504f1902b89d3d1c5e14830714e8dd..807927b994c23871ef75e63a985044dd860d8986 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 f3b479e9c0745c243ba404dee8ce6e8acd4e4c8b..b55d8da40fe1f6e1c46c989d4490baee51b665e5 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 0000000000000000000000000000000000000000..330495a75d028e011333663a694d7bcaa435c18f --- /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; +} + +