search

AdaCore / ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
63 stars 28 forks source link

Unchecked unions proposal #63

Closed kanigsson closed 3 years ago

kanigsson commented 3 years ago

Proposal at https://github.com/kanigsson/ada-spark-rfcs/blob/master/considered/rfc-unchecked_unions.rst

clairedross commented 3 years ago

I would like to add that the alternative is not costly for formal verification, where it would come for free, but for execution of ghost code. It causes complex issues of interaction with the size attribute for example, as we do not want the presence or absence of ghost code at execution to impact the normal behavior of the program.

CyrilleComar commented 3 years ago

I might have misunderstood the intent but if I understand correctly, I think there is a missing sentence after the second sentence in the second paragraph of "guide level explanation saying; "If the static check succeeds, the execution of the construct is not erroneous even if the discriminant check would fail.". I also think it would make the proposal more standalone of the static check was described here rather than refering to the semantics of address clauses. finally, the comments in the llast line of the example seems incorrect to me since the discriminant check would succeed h=on this line. The problematic line is the one above with the aggregate assignment which where the discuriminant doesn't match the value of the second field. So thisis the line that deserves a comment. By the way, the aggregate would be clearer, and the mismatch more obvious if specified more verbosely as (Flag => false, F2 => 1)

kanigsson commented 3 years ago

Cyrille, I have taken into account your three comments. In particular the last example was incorrect, the intent was to set the flag to True.

yannickmoy commented 3 years ago

After further discussion, it seems all uses of Unchecked_Union can be handled with Unchecked_Conversion, avoiding copies similarly when needed as we can get a reference to the object through an Unchecked_Conversion. So the RFC does not currently solve a big enough problem to warrant further work at this stage. Closing it.