--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on May 2017 ---
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