--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on May 2017 ---
I'm wondering if anyone has given any consideration to rendering ACSL using pragmas instead of embedded in comments? Using the first example from the tutorial:  /*@ ensures \result >= x && \result >= y;       ensures \result == x || \result == y;  */  int max (int x, int y) {     return (x > y) ? x : y;  } A pragma-based version might look something like:  #pragma acsl ensures \result >= x && \result >= y;  #pragma acsl ensures \result == x || \result == y;  int max (int x, int y) {     return (x > y) ? x : y;  } One major advantage of the pragma syntax is integration with the preprocessor.  For example, let's say I use a macro to define several variants of a function:  #define DEFINE_MAX_FN(T) \     T max (T x, T y) { \       return (x > y) ? x : y; \     }  DEFINE_MAX_FN(int)  DEFINE_MAX_FN(unsigned int)  DEFINE_MAX_FN(int64_t) I realize that (ab)using the preprocessor like this is often considered to be something of an anti-pattern, but there are times where the benefits from code reuse vastly outweigh the decreased readability.  I know several of my own projects would have been impractical without this feature. As far as I know, with ACSL there is no good way to annotate the different versions; I would need to add a comment for each one:  /*@ ensures \result >= x && \result >= y;       ensures \result == x || \result == y;  */  DEFINE_MAX_FN(int)  /*@ ensures \result >= x && \result >= y;       ensures \result == x || \result == y;  */  DEFINE_MAX_FN(unsigned int)  /*@ ensures \result >= x && \result >= y;       ensures \result == x || \result == y;  */  DEFINE_MAX_FN(int64_t) Which is especially onerous if the macro is considered to be part of the user-facing API and not just an implementation detail.  This is pretty common for things like test harnesses and data structure implementations. With a pragma-based implementation the annotations could be moved into the macro:  #define DEFINE_MAX_FN(T) \     _Pragma("acsl ensures \\result >= x && \\result >= y") \     _Pragma("acsl ensures \\result == x || \\result == y") \     T max (T x, T y) { \       return (x > y) ? x : y;     } Just to give a bit of context, I'm interested in adding (partial) ACSL support to C compilers; not for full formal verification, but to help the compilers provide better compile-time warnings and errors. I think the pragma-based syntax would also be more attractive for compilers as it would likely be easier to hook in to existing mechanisms in place to handle things like OpenMP, Cilk++, and compiler-specific directives.  It's also seems a bit more palatable since the pragma mechanism is part of the C99 and C11 standards. -Evan