Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] introducing hypothesis with ACSL on sets of array elements witk Frama-C/Value

  • Subject: [Frama-c-discuss] introducing hypothesis with ACSL on sets of array elements witk Frama-C/Value
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Thu, 18 Jul 2013 00:03:12 +0200
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F80CBD5FB6@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <569C6D7D26484241A530B87F45ADE1F80CBD5C40@AOFRWMBXRSC004.resources.atosorigin.local> <7fzjtlnlvu.fsf@cea.fr> <569C6D7D26484241A530B87F45ADE1F80CBD5FB6@AOFRWMBXRSC004.resources.atosorigin.local>
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,