Adpated from a post on the frama-c mailing list:
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, id) \
T id##_max (T x, T y) { \
return (x > y) ? x : y; \
}
DEFINE_MAX_FN(int, int)
DEFINE_MAX_FN(unsigned int, uint)
DEFINE_MAX_FN(int64_t, int64)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, int)
/*@ ensures \result >= x && \result >= y;
ensures \result == x || \result == y;
*/
DEFINE_MAX_FN(unsigned int, uint)
/*@ ensures \result >= x && \result >= y;
ensures \result == x || \result == y;
*/
DEFINE_MAX_FN(int64_t, int64)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, id) \
_Pragma("acsl ensures \\result >= x && \\result >= y") \
_Pragma("acsl ensures \\result == x || \\result == y") \
T id##_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.
@vprevosto responded with:
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; }
That's definitely a problem. I think that allowing people to split annotations across multiple pragmas is important for readability, though.
IMHO perhaps the most natural thing would be to have keywords like lemma apply to a single statement, but also add a begin/end syntax for multi-statement annotations. So, the above example would translate into something like
/*@ lemma foo: \true; */
/*@ requires: \true;
ensures: \true;
*/
int f() { return 0; }However, you changed the code to something like
#pragma acsl begin lemma foo: \true;
#pragma acsl requires: \true;
#pragma acsl ensures: \true;
#pragma acsl end lemma;
You would end up with
/*@ lemma foo: \true
requires: \true;
ensures: \true;
*/
int f() { return 0; }Of course you could also go with end lemma foo, end foo, or even just end.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent