Proof of the generic unit to array operations (vector/matrix), only at silver level, for runtime errors that come from the generic part of the unit. This does not prove e.g. absence of overflows in an instantiation related to arithmetic operations passed as formal generic subprogram parameters.
Justify 2 checks with pragma Annotate as False_Positive (related to
absence of aliasing) and 3 checks as Intentional (possible overflow and
explicit exception).
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-ngcoar.adb: Add pragma to ignore assertions in
instance.
* libgnat/a-ngrear.adb: Likewise.
* libgnat/s-gearop.adb: Prove implementation is free of runtime
errors.
* libgnat/s-gearop.ads: Add contracts to protect against runtime
errors in the generic part.
patch.diff.gz
Description: application/gzip
