We agreed that it is safer for volatile variables (or state abstractions) with
Async_Writers to be explicitly initialized (or imported), despite SPARK RM
7.1.2(14) didn't require them to be initialized.
[changelog]
* docs/lrm/source/packages.rst
(External State): Remove rule 7.1.2(14); renumber subsequent rules.
* src/flow/flow-control_flow_graph-utility.adb
(Make_Variable_Attribute): Remove implementation of the mentioned rule.
* testsuite/gnatprove/tests/932__flow_async_import/test.out
New check on a volatile variable with no explicit initialization.
Switch --no-generated-global was bypassing global generation by forcing
generated globals to be null where no explicit contract was present. However,
this behavior was impossible to implement precisely and now this switch causes
a warning where an explicit non-null Global or Refined_Global could be written.
[changelog]
* docs/ug/en/source/how_to_write_subprogram_contracts.rst
(Generation of Dependency Contracts): Adjust switch description.
* src/flow/flow-analysis-sanity.adb
(Check_Illegal_Writes_And_All_Variables_Known): Deconstruct GG bypass.
* src/flow/flow-analysis.adb
(Check_Required_Contracts): New check that emit warnings; body.
* src/flow/flow-analysis.ads
(Check_Required_Contracts): Likewise; spec.
* src/flow/flow.adb
(Check_Contracts): Plug new check into analysis.
* src/flow/flow_error_messages.adb
Adapt WITH clauses.
* src/flow/flow_error_messages.ads
(Error_Msg_Flow): Add precondition that was useful when special-casing missing
Refined_Global on imported subprograms.
* src/flow/flow_generated_globals-partial.adb
(Generate_Contracts): Deconstruct GG bypass in phase 1.
* src/flow/flow_generated_globals-phase_2.adb
(Resolve_Globals): Deconstruct GG bypass in phase 2.
* src/flow/flow_utility.adb
(Get_Globals): Deconstruct GG bypass in Get_Globals.
* src/flow/flow_utility.ads
(Get_Globals): Remove comment about GG bypass.
* src/spark/gnat2why_opts-reading.ads
(Flow_Generate_Contracts): Update flag description.
* testsuite/gnatprove/tests/346__flow_no_generated_global/
Add dedicated tests: units P and Q are based on the original reproducer and the
issue discussion; unit R shows different warnings for states with null and
non-null refinements; unit T is for an imported subprogram (this was found when
enabling switch on the entire testsuite).
* testsuite/gnatprove/tests/QB22-037__flow_no_gg/test.out
* testsuite/gnatprove/tests/R524-009__flow_no_global_generation_switch/test.out
* testsuite/gnatprove/tests/R717-025__flow_container/test.out
Update outputs.
