--- layout: fc_discuss_archives title: Message 106 from Frama-C-discuss on October 2008 ---
Thank you, Yannick and Pascal, for your answers and hints. But ... would it be possible to keep that idea of a command-line option that will stress the end-users to specify mandatory "terminates ..." clauses either for functions containing loops, or for recursive functions, or for backward goto/label in functions (I promise there is no backward-goto in my code! but ... who knows in the world!!!). Best regards, Dillon Pascal Cuoq a ?crit : > > On Oct 23, 2008, at 2:28 PM, Yannick Moy wrote: >> It is still to be decided whether we define an option to force >> termination checking, or if this should be the default, with an >> option to switch back to the current behavior. > ... > > Partial correctness results can be expressed by adding > a "terminates false;" clause to the contract every function in the > program. > It would be bad style if the meaning of contracts > changed according to command-line options. > ...