--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on May 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Pragma-based ACSL syntax



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