Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Pragma-based ACSL syntax
  • From: evan at coeus-group.com (Evan Nemerson)
  • Date: Thu, 11 May 2017 16:08:35 -0700
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