{"push_id":2546974998,"size":1,"distinct_size":1,"ref":"refs/heads/master","head":"01c38cfa8fc59498f3675c019f8ae0081dacb4a2","before":"003a2c114dc331996d16fdc218d3e5cda41dfabd","commits":[{"sha":"01c38cfa8fc59498f3675c019f8ae0081dacb4a2","author":{"name":"Piotr Trojanek","email":"cf728c1c31506c7219195290995225cd6fff6281@altran.com"},"message":"Q515-015 remove warnings about ineffective writes for assertions\n\nThis patch fixes suspicious suppression about ineffective writes to ghost\nvariables.\n\nThis removes spurious warnings about ineffective assignment, e.g.:\n\n   X := Some_Expression; --  here the \"effect\" is to compute something for\n                         --  an assertion expression\n   pragma Assert (X);\n\nor compound ineffective statements, e.g.:\n\n   for K in 1 .. 10 loop\n      pragma Loop_Invariant (X >= K);\n      if Y > K then      --  here is a more complicated, but similar effect,\n         exit;           --  i.e. computing something for a Loop_Invariant\n      end if;\n      exit when Z > K;\n   end loop;\n\n   if Some_expression then --  again, here the computation is meant for the\n      pragma Assert (X);   --  assertion expression; that is its \"effect\"\n   end if;\n\nand about ineffective initialization like this:\n\n   declare\n      X := Some_Expression;\n   begin\n      pragma Assert (X);\n   end;\n\nand finally about ineffective entry barriers like this:\n\n   entry E\n      when X  --  this is neither an output nor an assertion, but a warning\n              --  that this \"statement has no effect\" is clearly spurious\n   is\n      ...\n\nWe also get some new warnings, both genuine and spurious (see below).\n\n* testsuite/gnatprove/tests/JC17-017__exit/test.out\n* testsuite/gnatprove/tests/K315-020__nested/test.out\n* testsuite/gnatprove/tests/K412-014__param/test.out\n* testsuite/gnatprove/tests/K412-014__pointer/test.out\n* testsuite/gnatprove/tests/KA21-006__funcs/test.out\n* testsuite/gnatprove/tests/KB29-037__subtype/test.out\n* testsuite/gnatprove/tests/L305-015__actions/test.out\n* testsuite/gnatprove/tests/L608-022__minmax/test.out\n* testsuite/gnatprove/tests/L719-025__hashed_sets_equal/test.out\n* testsuite/gnatprove/tests/L719-025__ordered_sets_equal/test.out\n* testsuite/gnatprove/tests/LC17-035__update_big_test/test.out\n* testsuite/gnatprove/tests/M318-009__flow_quantified_expressions/test.out\n* testsuite/gnatprove/tests/M426-006__flow_bug_nested_subprogram_pragmas/\n* testsuite/gnatprove/tests/M426-014__flow_tick_old_and_loop_entry/test.out\n* testsuite/gnatprove/tests/M716-042__constants/test.out\n* testsuite/gnatprove/tests/MB14-026__old/test.out\n* testsuite/gnatprove/tests/N624-020__perm_occ/test.out\n* testsuite/gnatprove/tests/O219-034__flow_global_checks/test.out\n* testsuite/gnatprove/tests/O319-012__null_records/test.out\n* testsuite/gnatprove/tests/O403-005__private_attributes/test.out\n* testsuite/gnatprove/tests/O512-022__fibonacci/test.out\n* testsuite/gnatprove/tests/O512-022__prefix_sum/test.out\n* testsuite/gnatprove/tests/O522-028__loop_entry_update/test.out\n* testsuite/gnatprove/tests/O715-033__level0/test.out\n* testsuite/gnatprove/tests/O715-033__level1/test.out\n* testsuite/gnatprove/tests/O715-033__level2/test.out\n* testsuite/gnatprove/tests/O715-033__level3/test.out\n* testsuite/gnatprove/tests/O724-003__iterable/test.out\n* testsuite/gnatprove/tests/O827-017__dispatching_procedures/test.out\n* testsuite/gnatprove/tests/O831-003__do333_mode_logic_qgen/test.out\n* testsuite/gnatprove/tests/O910-017__modular_strlit/test.out\n* testsuite/gnatprove/tests/OB12-011__polluting_abstract_state/test.out\n* testsuite/gnatprove/tests/P108-010__flow_incorrect_depends_of_po/test.out\n* testsuite/gnatprove/tests/P519-021__x86_basicmath_small/test.out\n* testsuite/gnatprove/tests/P519-021__x86_basicmath_small_no_loop_fn/\n* testsuite/gnatprove/tests/P519-021__x86_memcpy/test.out\n* testsuite/gnatprove/tests/P602-004__entry_range_check/test.out\n* testsuite/gnatprove/tests/P608-008__claim_on_entry_body/test.out\n* testsuite/gnatprove/tests/P608-023__assumption_spark_off/test.out\n* testsuite/gnatprove/tests/P615-019__bronze/test.out\n* testsuite/gnatprove/tests/P715-019__flow_subprogram_termination/test.out\n* testsuite/gnatprove/tests/P916-028__er_pure_barriers/test.out\n* testsuite/gnatprove/tests/Q106-016__address_aliasing/test.out\n* testsuite/gnatprove/tests/Q918-039__flow_ghost/test.out\n* testsuite/gnatprove/tests/RM_MS__external_variables_output_append_tail/\n* testsuite/gnatprove/tests/TU__loop_related_legal/test.out\n* testsuite/gnatprove/tests/prime_numbers/test.out\n* testsuite/gnatprove/tests/proofinuse__ce/test.out\n* testsuite/gnatprove/tests/tagged_stacks/test.out\n* testsuite/gnatprove/tests/trajectory_computation/test.out\nRemove spurious warnings.\n\n* testsuite/gnatprove/tests/red_black_trees/test.out\n* testsuite/gnatprove/tests/adacore_u/test.out\nNew warnings; genuine.\n\n* testsuite/gnatprove/tests/N624-020__perm_rem/test.out\nNew warnings; spurious; to be investigated separately.\n\nChange-Id: I12d3fc50094a6e6fc16ef842c85374d37b3ca04f","distinct":true,"url":"https://api.github.com/repos/AdaCore/spark2014/commits/01c38cfa8fc59498f3675c019f8ae0081dacb4a2"}]}
{"actor":{"display_login":"adacore-bot"}}