-- Andrei Paskevich (2014-02-10) > > > Yes, I think, we will have to create debug flags to silence different types > of warnings, and that, before the next release.
Or have a more clever warning which does not warn on "while True" loops. This is what we strive to do in our compiler: produce warnings that detect as many potential issues, as you try to do here, but avoid pinpointing situations that the user knows about. For example, when we implemented in GNAT the warning about suspicious postconditions that only talk about the pre-state, we did not warn about postconditions of "True" or "False", that are either generated or put on purpose (for test, for documentation), and do not correspond to an error. > That said, once we go seriously into module cloning / refinement, these > annotations will become important, since, for one, it won't be possible to > instantiate an abstract terminating function (that is, any "val" without an > explicit "diverges" clause) with a potentially diverging implementation. And > this is no more the question of usability but of correctness. sure, but that's a different issue from the warning above. -- Yannick Moy, Senior Software Engineer, AdaCore _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
