--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on April 2012 ---
Hi Sylvain, On Mon, Apr 16, 2012 at 10:34 AM, sylvain nahas <sylvain.nahas at googlemail.com> wrote: >> If you want to avoid those warnings, position your disjunction _before_ your >> ? ? ? ?/*@ assert ( in_int8 < 0 ) || ( in_int8 >= 0 ); */ >> ? ? ? ?uint8 out_uint8 = abs8(in_int8); > > So a "requires" in a contract hasn't the same effect? Good remark. I focused on the assertion at the beginning of abs8, and forgot about your precondition. The answer is two-fold. Disjunction in 'requires' are used to propagate states separately, provided there is enough slevel at the beginning of the function to split the disjunction (it is the case here). You can check that by adding a Frama_C_show_each(val) just before your assert: you will get two different lines in the log. However, the body of the function is not analyzed N times, just 1 time with N different states. There are subtle differences between these two possibilities, including which behaviors are active. Here positive_or_zero is active only in the case "val >= 0', and conversely, but we cannot easily keep track of this information. By adding a disjunction before the call, things are different: the function is analyzed twice. >From a general standpoint, Value has a certain latitude on what to do on behaviors and preconditions, as many approaches are correct (sound), but not equivalent in terms of precision and computation time. In your example, the 'requires' is useful, but should not be given the 'assumes', 'disjoint' and 'complete' clauses, since those contain all the needed information. For Oxygen, I would like to implement alternative strategies such as automatic split, at least for complete and disjoint behaviors. HTH, -- Boris