--- layout: fc_discuss_archives title: Message 8 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



Hello,

2017-05-12 1:08 GMT+02:00 Evan Nemerson <evan at coeus-group.com>:
> I'm wondering if anyone has given any consideration to rendering ACSL
> using pragmas instead of embedded in comments?
>

No. there is some bitrotten mechanism in
src/kernel_internals/typing/translate_lightweight.ml that once seeked
to hijack Microsoft's __declspec annotations to provide "lightweight"
annotations. Basically, attaching `__declspec(p)` to a parameter x
(respectively to the function itself) would generate `requires p(x)`
(respectively `ensures p(\result)`). It's been unmaintained for years,
though, and porting the code so that it can be used against current
versions of Frama-C will probably require significant work.


>   #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;

> 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.
>

I see your point. This might indeed be worth considering, even though
I think that some clarifications are needed on what exactly can go
after an acsl pragma. In particular, you seem to want to be able to
split a single annotation into several pragmas, which implies an
obvious question: how do we merge them? In particular, we should take
care of easily distinguishing global annotations from function
contracts, as in:

_Pragma("acsl lemma foo: \\true;")
_Pragma("acsl requires \\true;")
_Pragma("acsl ensures \\true;")
int f() { return 0; }

May I suggest to open an issue on
https://github.com/acsl-language/acsl ? It is supposed to be the new
home for discussions on ACSL itself (although we could have advertised
it a bit more, I admit).

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile