Suggested configuration is incomplete

[heisenbugltd]

Suggested configuration is incomplete

[Jellix]

Thanks for the report.

I think I understand the underlying issue. From the looks of it, the crudely implemented logic to figure out the proper source file name is especially broken when the .spark file references an entity from a generic unit: In such a case the name of the generic unit wins and as you can have multiple instantiations, they will be referenced more than once, forgetting about the actual name of the instantiation.

[Jellix]

Ok, I just released v1.1.2 which should fix the issue according to what I could test without my machine constantly crashing due to overheating. :)

[treiher]

Many thanks for your work. Unfortunately, I'm still not able to successfully prove the project with the suggested configuration. To narrow the problem down I reused the example used in #50. The suggested configuration for this example with version 1.1.2 is:

package Prove is
   for Proof_Switches ("rflx-rflx_arithmetic.ads") use ("--prover=CVC4", "--steps=90761", "--timeout=22");
end Prove;

Using that configuration leads to multiple failing checks:

$ gnatprove -Ptest
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
rflx-rflx_arithmetic.adb:11:13: medium: divide by zero might fail [possible explanation: precondition of subprogram at rflx-rflx_arithmetic.ads:16 should mention Value]
rflx-rflx_arithmetic.adb:21:08: medium: postcondition might fail, cannot prove X / Pow2 (K) < Pow2 (J - K)
rflx-rflx_arithmetic.adb:21:10: medium: divide by zero might fail
rflx-rflx_arithmetic.adb:36:14: medium: postcondition might fail, cannot prove X * Pow2 (K) <= Pow2 (J + K) - Pow2 (K) (e.g. when J = 0 and K = 0 and X = 4611686018427387904)
rflx-rflx_arithmetic.adb:36:16: medium: overflow check might fail (e.g. when K = 0 and X = 12797496590450976783)
rflx-rflx_arithmetic.adb:36:43: medium: overflow check might fail
rflx-rflx_arithmetic.adb:37:16: medium: overflow check might fail (e.g. when K = 0 and X = 12797496590450976783)
rflx-rflx_arithmetic.adb:37:50: medium: overflow check might fail
rflx-rflx_arithmetic.adb:46:38: medium: divide by zero might fail
rflx-rflx_arithmetic.adb:54:38: medium: overflow check might fail (e.g. when Length = 0 and Result = 12797496590450976783 and Value = 12797496590450976783)
rflx-rflx_arithmetic.ads:20:08: medium: postcondition might fail, cannot prove Mod_Pow2'Result < 2**Exp
rflx-rflx_arithmetic.ads:30:08: medium: postcondition might fail, cannot prove Right_Shift'Result < 2**(Value_Size - Length)
rflx-rflx_arithmetic.ads:42:11: medium: postcondition might fail, cannot prove Left_Shift'Result <= Pow2 (Value_Size + Length) - Pow2 (Length) (e.g. when Left_Shift'Result = 0 and Length = 0)
rflx-rflx_arithmetic.ads:45:57: medium: overflow check might fail

I 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.

[Jellix]

Interesting, considering that certain representatives of the tool chain developers said that it only considers a single unit.

So from what I understood, it shouldn't matter, which file is specified as long as there's one (and preferably only one). With that assumption, I obviously opted for the spec.

Well, at least that one is easy enough to fix.

[Jellix]

Alright, fixed in v1.1.3, which now prefers the bodies instead of specs.