--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on July 2013 ---
Hi St?phane, On Wed, Jul 17, 2013 at 10:14 PM, DUPRAT Stephane <stephane.duprat at atos.net> wrote: > It still remains the solution of introducing these hypothesis by a C function calling f1 and performing some initialization in the context. But it is not an ACSL solution. Sure ! But Matthieu was aiming at an ACSL-only solution. The amount of development needed in Value to reduce by preconditions/assertions of the form 'tab2[2..3]==23' is non-trivial, but also not completely unreasonable. (Say, of similar complexity to previous medium-sized developments that were done to improve the evaluation of the logic in Value.) Notice however that 'tab2[2..3]==23' is in fact translated to '{ tab2[2..3] } == {23}', which really means '{ tab2[2] ; tab2[3] } == {23}'. That is, your equality is actually an equality on sets. Thus you cannot write '0 <= tab2[2..3] <= 10', which is meaningless on sets -- or at least not lifted point-wise on the elements of the set. In this case, you should use universal quantification, for which a very preliminary form of evaluation has appeared in the development version of Value. Unfortunately, no reduction is currently performed either, only evaluation. Reducing by \forall-quantified predicates would be more interesting and more general than reducing by sets equality, and we could in fact easily translate the latter into the former. Unfortunately, it is highly non-trivial if we want to handle predicates more generic than a few hard-coded common cases... HTH,