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