search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

Fix list of clauses accepting \old and \result #40

Closed maroneze closed 6 years ago

maroneze commented 6 years ago

As noticed by @bobot in discussion with industrial partners.

bobot commented 6 years ago

Could we add that in assigns clauses \result not in a direct \at(e,Post) is forbidden (and enforced by the typer)? In fact we could enforce the same thing in ensures (just the \at(e,Post) is implicitely at toplevel).

vprevosto commented 6 years ago

@bobot at first glance, your comment seems quite in line with what I said yesterday in the discussion initiated by @yakobowski above. Are there some points I forgot to mention?

bobot commented 6 years ago

@vprevosto I just wanted to explicit what was implicit in your message. I should have said that I agreed with you.

maroneze commented 6 years ago

I tried rewording it to take into account your remarks:

vprevosto commented 6 years ago

no mention of frees;

But didn't we say that frees ought to refer to \at(\result,Post) in a way similar to what assigns does?