[CN] multiple incompatible specs for a function are silently accepted

[peterohanley]

This succeeds silently, I think it should give an error for this case and a warning for duplicate specs at all.

void f (int *res);
/*@ spec f(pointer res);
    requires take x = Block<int>(res);
    ensures take out = Owned<int>(res);
@*/
/*@ spec f(pointer res);
    requires take x = Owned<int>(res);
    ensures take out = Owned<int>(res);
@*/

void g(void)
{
   int x;
   f(&x);
}

It seems that it uses the first spec. To avoid tricky questions about what a compatible spec is just warning when another is encountered should work

[septract]

I agree that there should be a warning. But I think that it would be fine to allow multiple specs, if we had some mechanism in the language to select between them at the callsite. There's always a danger that the user will assume incorrect specs, of course.

to nitpick, these particular specs for f() are compatible with each other. It's just that the first one is stronger in that it allows the memory at res to be uninitialized.

[peterohanley]

Are you thinking of multiple specs as overloading? I was thinking of them as refinement or something. I will make another issue about it, it has to do with mentioning a static global variable that the function needs. It needs to have a spec to be called elsewhere but that spec cannot mention the variable because it isn't in scope. That specific case doesn't really make sense but it was when I added the second spec that I learned I had already added a spec for the function at its declaration.

[cp526]

We've also come across situations where it would have been handy to be able to give multiple specifications to the same function (in our case the pKVM buddy allocator's list manipulating functions); Frama-C supports something like that.

One possible route in CN would be to support function specifications with top-level if-then-else's that "switch" between different specifications based on the inputs (possibly even in a nested way). Then at the callsite it has to be provable that the if-then-else branching is uniquely determined, and everything else could work the same way.

[PeterSewell]

Frama-C has "named behaviours" (p27 of https://frama-c.com/download/frama-c-acsl-implementation.pdf) - it'd be interesting to know how much they use them.

On Sat, 6 Jul 2024 at 09:09, Christopher Pulte @.***> wrote:

We've also come across situations where it would have been handy to be able to give multiple specifications to the same function (in our case the pKVM buddy allocator's list manipulating functions); Frama-C supports something like that.

One possible route in CN would be to support function specifications with top-level if-then-else's that "switch" between different specifications based on the inputs (possibly even in a nested way). Then at the callsite it has to be provable that the if-then-else branching is uniquely determined, and everything else could work the same way.

— Reply to this email directly, view it on GitHub https://github.com/rems-project/cerberus/issues/362#issuecomment-2211701721, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZUP53DTEA7SCOCPDPLZK6Q35AVCNFSM6AAAAABKKB6GGKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMJRG4YDCNZSGE . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[septract]

From a CN design PoV, I suppose we should at least warn / crash when specs are overridden, rather than just deciding arbitrarily which one to use. So I think this is a bug as of now, even though in the future we might want multiple named specs for the same function.

[peterohanley]

BTW there is already a warning if a spec is written after the declaration and then also on the definition.