{"push_id":2963165905,"size":1,"distinct_size":1,"ref":"refs/heads/master","head":"465e791aedda43a8e9becf33019ff0f4e67474ab","before":"eca205f1278f9a3303f4b9cae965aeeffe214b72","commits":[{"sha":"465e791aedda43a8e9becf33019ff0f4e67474ab","author":{"name":"Yannick Moy","email":"87d302d93659e7e602e8a49ff4cf8dd6a60b4efb@adacore.com"},"message":"RA01-014 Suppress wrong explanations across loops\n\nSome wrong explanations are issued by GNATprove on checks inside and after\nloops, when the check involves variables modified in the loop. Avoid the\nsearch for explanation to continue beyond the loop boundary in such cases.\n\n* gnat2why/flow/flow_error_messages.adb\n(Get_Explanation): Stop search at loop boundary when check involves\n variables modified in the loop.\n\n* testsuite/gnatprove/tests/K223-023__search/test.out\n* testsuite/gnatprove/tests/K627-010__stable_marriage/test.out\n* testsuite/gnatprove/tests/KB04-013__expr_action/test.out\n* testsuite/gnatprove/tests/L503-008__iterators/test.out\n* testsuite/gnatprove/tests/LB27-011__overflow_config/test.out\n* testsuite/gnatprove/tests/LB27-011__overflow_pragma/test.out\n* testsuite/gnatprove/tests/LB27-011__overflow_switch/test.out\n* testsuite/gnatprove/tests/M322-040__loopinv/test.out\n* testsuite/gnatprove/tests/N919-012__coq_split/test.out\n* testsuite/gnatprove/tests/O512-022__power_and_sum/test.out\n* testsuite/gnatprove/tests/O512-022__slice_sums/test.out\n* .../tests/O512-022__vscomp2014_partition_functional/test.out\n* testsuite/gnatprove/tests/O722-006__functional_lists/test.out\n* testsuite/gnatprove/tests/P530-020__forall__ce/test.out\n* testsuite/gnatprove/tests/QA11-003__itp_sumrange/test.out\n* testsuite/gnatprove/tests/QA31-008__von_neumann_sqrt/test.out\n* testsuite/gnatprove/tests/QB10-026__counterexample/test.out\n* testsuite/gnatprove/tests/R516-050__functional_lists/test.out\n* testsuite/gnatprove/tests/RA14-002__effect_on_exit_path/test.out\n* testsuite/gnatprove/tests/riposte__arithmetic/test.out\n* testsuite/gnatprove/tests/thumper/test.out\nUpdate outputs.\n\nChange-Id: I898c39f263f567b48f445ecd850d075306fa3930","distinct":true,"url":"https://api.github.com/repos/AdaCore/spark2014/commits/465e791aedda43a8e9becf33019ff0f4e67474ab"}]}
{"actor":{"display_login":"adacore-bot"}}