Handling of file specific proof switches?

[Jellix]

Hi there, developer of SPAT here.

For now, this is more of a question than a bug report, so bear with me:

If you look at this issue comment:

[...] a unit is analyzed all at once, so specifying switches for both "rflx-rflx_arithmetic.adb" and "rflx-rflx_arithmetic.ads" is not useful. In that case, only the second set of switches will be used.

So, I naturally assumed that for a single compilation unit it doesn't matter if you specify spec or body file as long as one of them is mentioned, so I opted to prefer the spec file.

Now, I got the other issue comment:

was able to solve that problem by specifying switches for rflx-rflx_arithmetic.adb instead of rflx-rflx_arithmetic.ads. It seems switches should be preferably specified for the body and not the specification.

Which leads to the question: How is gnatprove supposed to handle file specific switches for spec and body file? There seems to be a discrepancy between the somewhat documented and the actual behaviour (given the limited information I have).

[kanigsson]

Hello,

I think Yannick's comment is slightly incorrect, the tool indeed takes into account the switches specified for the body file if it exists (and ignores any switches specified for the spec file in that case). Switches for spec files are taken into account only if there is no body. In my experiments this is consistent with gprbuild's Switches attribute. We will clarify this in the documentation.

[Jellix]

Thank you very much for the clarification.

That confirms the observed behaviour and validates my decision to prefer body files for the Proof_Switches.

[kanigsson]

We have clarified this now in the doc (may take a couple of days to appear online).