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: matthieu.lemerre at cea.fr (Matthieu Lemerre)
  • Date: Wed, 17 Jul 2013 19:20:53 +0200
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F80CBD5C40@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <569C6D7D26484241A530B87F45ADE1F80CBD5C40@AOFRWMBXRSC004.resources.atosorigin.local>
Hello,

DUPRAT Stephane <stephane.duprat at atos.net> writes:

> I deduce that :
>
> -          The tool is able to evaluate a simple element (tab1[5]==5)
> -          An hypothesis introduces by ACSL on a simple element (tab1[2]==2) is propagated in the program
> -          The tool is able to evaluate a set of elements (tab2[6..7]==67)
> -          An hypothesis introduces by ACSL on a set of elements (tab2[2..3]==23) is not propagated in the program
>

Those are all correct.

> The question is for the last item, if there is a way to introduce
> hypothesys on sets of elements ?

The only way to do that at the moment would be to perform some new
developments in the implementation of the reduction strategy in the
logic by the value analysis plugin...

Best regards,

Matthieu