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

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