Frama-c not working with static_assert inside a macro

[nsutter]

I am trying to use frama inside my program but I can't use it. My program uses macro with static_assert inside.

If there is the function static_assert(condition, message) (same problem with _Static_assert) inside a maccro I get an error from frama-c (syntax error). Everything is compiling fine with gcc 7.3.0 and I only have a issue with frama-c.

Am I doing something wrong? I've found nothing in the documentation relating this issue.

I use frama-c phosphorus-20170501.

An example is the code below:

#include <assert.h>

#define ADD_ASSERT(MIN, MAX) \
    static_assert(MIN < MAX, "Min should be lower than MAX");

ADD_ASSERT(3, 5)

int main()
{
    return 0;
}

I use the command: frama-c main.c The error message is: [kernel] Frama-c aborted: invalid user input. syntax error at main.c:6 (pointing the line with the maccro)

[nsutter]

Adding to the command line -cpp-command="gcc -E -D 'static_assert(A, B)='" -no-cpp-frama-c-compliant solved the problem (I remove the static_assert during preprocessing)

[maroneze]

static_assert and _Static_assert are C11 features. Frama-C's support is mainly focused on C99 (a few C11 features are occasionally supported).

If all you want is to parse the code, a macro such as #define static_assert(...) (using a variadic notation to allow an arbitrary number of arguments) should allow them to be ignored.

Otherwise, if you also want to check the property defined by the static_assert, a somewhat contrived way to do it would be to use an ACSL lemma:

#define MIN 3
#define MAX 4

//@ lemma min_lt_max: MIN < MAX;

int main() { return 0; }

Then, running the WP plug-in will report on whether the lemma could be proved or not. This is not standard usage and cannot be automatically translated from static_asserts, but in the worst case this may provide a somewhat similar feature.

[maroneze]

By the way, if you are using gcc, you normally don't need to use -cpp-command="gcc -E -D 'static_assert(A, B)='" -no-cpp-frama-c-compliant. Instead, prefer using:

-cpp-extra-args="'-Dstatic_assert(A\,B)='"

(note that the comma had to be escaped)

Or, even better:

-cpp-extra-args="'-Dstatic_assert(...)='"

For complex macros and general parsing issues, I prefer defining all of them in a fc_stubs.h file or similar, and then prepending it to every file during parsing, by using:

-cpp-extra-args="-include fc_stubs.h"

(Using the -include preprocessor option from GCC)

[maroneze]

It seems the issue is no longer active, so I'm closing it. If you have other issues just tell us.

[Tharunsai23]

I am trying to use frama inside my program but I can't use it. My program uses macro with static_assert inside.

If there is the function static_assert(condition, message) (same problem with _Static_assert) inside a maccro I get an error from frama-c (syntax error). Everything is compiling fine with gcc 7.3.0 and I only have a issue with frama-c.

Am I doing something wrong? I've found nothing in the documentation relating this issue.

I use frama-c phosphorus-20170501.

An example is the code below:

include

define ADD_ASSERT(MIN, MAX) \

static_assert(MIN < MAX, "Min should be lower than MAX");

ADD_ASSERT(3, 5)

int main() { return 0; } I use the command: frama-c main.c The error message is: [kernel] Frama-c aborted: invalid user input. syntax error at main.c:6 (pointing the line with the maccro)

[Tharunsai23]

I am trying to use frama inside my program but I can't use it. My program uses macro with static_assert inside.

If there is the function static_assert(condition, message) (same problem with _Static_assert) inside a maccro I get an error from frama-c (syntax error). Everything is compiling fine with gcc 7.3.0 and I only have a issue with frama-c.

Am I doing something wrong? I've found nothing in the documentation relating this issue.

I use frama-c phosphorus-20170501.

An example is the code below:

include

define ADD_ASSERT(MIN, MAX) \

static_assert(MIN < MAX, "Min should be lower than MAX");

ADD_ASSERT(3, 5)

int main() { return 0; } I use the command: frama-c main.c The error message is: [kernel] Frama-c aborted: invalid user input. syntax error at main.c:6 (pointing the line with the maccro)

[maroneze]

Frama-C up to and including 23.1 does not support the C11 _Static_assert keyword, and the error message does not specify it precisely. It simply causes some parsing error that results in a nondescript message. There is no way to make it work reliably with any of these Frama-C versions.

_Static_assert will likely be available on Frama-C 24 (Chromium), to be released later this year (but this is not guaranteed).

Also, this GIthub repository will be archived and future issues should be reported to: https://git.frama-c.com/pub/frama-c/-/issues