{"push_id":1780770923,"size":4,"distinct_size":4,"ref":"refs/heads/master","head":"6cdf5cbcbede5e276328ac611eac4e76c6ddf413","before":"806a205c8dea5c2fda3647100591fc5d0a051d85","commits":[{"sha":"b980263812be34f0583b09b201cfd6a1b328782a","author":{"name":"Piotr Trojanek","email":"5cdbd7acc4487b43aeff10ffa86dcd9454b78b1c@altran.com"},"message":"Q403-015 deconstruct --dbg-proof-only switch\n\nSwitch --dbg-proof-only was added as a workaround against crashes in flow\nanalysis. However, flow analysis is now much more robust, so this switch is\nrarely useful, yet it is difficult to maintain and use, especially when\ncontracts other than Global are generated. This patch removes this switch.\n\n* common/gnat2why_args.ads\n(Debug_Proof_Only): remove declaration (and all references).\n\n* common/gnat2why_args.adb\n(Prove_Only_Name): remove declaration (and all references).\n\n* gnatprove/configuration.ads\n(Debug_Proof_Only): remove declaration (and all references).\n\n* gnat2why/why/gnat2why-driver.adb\n(GNAT_To_Why): remove IF logic for the --dbg-proof-only switch.\n\n* share/spark/help.txt\nRemove description of the --dbg-proof-only switch.\n\n* testsuite/gnatprove/tests/PA20-065__gnatprove_output/test.out\n* testsuite/gnatprove/tests/PA20-065__gnatprove_help_output/test.out\nUpdate outputs of tests related to the --help switch.\n\n* testsuite/gnatprove/tests/PA30-001__non_spark_comp/test.py\n* testsuite/gnatprove/tests/PA30-001__part_of_spark_mode_off/test.py\nRemove --dbg-proof-only switch (for tests that were already disabled as part\nof the new generated globals; they are not interesting for proof anyway).\n\n* testsuite/gnatprove/tests/PC02-007__record_ddos/test.py\n* testsuite/gnatprove/tests/PC02-007__record_ddos/test.opt\nRemove --dbg-proof-only switch and make the DEAD (it is only meant to\ndemonstrate an excessive memory and CPU usage by flow analysis).\n\nChange-Id: I284081f3d5ce470b066358c944c287dc5c195584","distinct":true,"url":"https://api.github.com/repos/AdaCore/spark2014/commits/b980263812be34f0583b09b201cfd6a1b328782a"},{"sha":"e9ee7ac75261c80d04d6cd5cf10e9a19ab60a471","author":{"name":"Piotr Trojanek","email":"5cdbd7acc4487b43aeff10ffa86dcd9454b78b1c@altran.com"},"message":"OB30-008 deconstruct closure of frontend globals\n\nNew design of the \"generated globals\" unifies handling of globals for\nsubprograms in and out of SPARK. In particular, there is no need to handle\nthem with two graph closures. This patch removes code for the closure that\nhandled frontend globals.\n\n* gnat2why/why/gnat2why-driver.adb\n(Compute_Global_Effects): only call Propagate_Through_Call_Graph in phase 1.\n\n* gnat2why/spark/spark_frame_conditions.ads\n* gnat2why/spark/spark_frame_conditions.adb\n(Propagate_Through_Call_Graph): now only called in phase 1, so no need for\n extra arguments; remove code that depended on those arguments.\n\n(Compute_Strongly_Connected_Components): remove, no longer needed.\n(Count_In_Map):\n\nChange-Id: I518e6a3c21d59f26cbb426badd94097ea21b6ecc","distinct":true,"url":"https://api.github.com/repos/AdaCore/spark2014/commits/e9ee7ac75261c80d04d6cd5cf10e9a19ab60a471"},{"sha":"55ec9e0cb9c1a5ee903de166c607bc4750a4c11a","author":{"name":"Piotr Trojanek","email":"5cdbd7acc4487b43aeff10ffa86dcd9454b78b1c@altran.com"},"message":"refactor repeated iteration over frontend scopes\n\n* gnat2why/spark/spark_frame_conditions.adb\n(Set_Default_To_Empty): refactor to avoid repeated iteration over Scopes.\n\n(no-tn-check)\n\nChange-Id: Ic6fa32011451dbcfaab40a0c8bfec7eeb1739a55","distinct":true,"url":"https://api.github.com/repos/AdaCore/spark2014/commits/55ec9e0cb9c1a5ee903de166c607bc4750a4c11a"},{"sha":"6cdf5cbcbede5e276328ac611eac4e76c6ddf413","author":{"name":"Piotr Trojanek","email":"5cdbd7acc4487b43aeff10ffa86dcd9454b78b1c@altran.com"},"message":"refactor repeated code for reading ALI files\n\n* gnat2why/spark/spark_frame_conditions.adb\n(Load_SPARK_Xrefs): remove duplicated code for conversion from ALI_Id to\n a string filename.\n\n(no-tn-check)\n\nChange-Id: I0ff6108f725de90c8789a2d97505073a671b2442","distinct":true,"url":"https://api.github.com/repos/AdaCore/spark2014/commits/6cdf5cbcbede5e276328ac611eac4e76c6ddf413"}]}
{"actor":{"display_login":"adacore-bot"}}