--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on July 2013 ---
[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



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