mirror of
https://github.com/AdaCore/spark2014.git
synced 2026-02-12 12:39:11 -08:00
2469257c82
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.