--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] Assert clause not proved




Le 08/10/2013 07:40, Guillaume Melquiond a ?crit :
> On 04/10/2013 15:50, Rovedy Aparecida Busquim e Silva wrote:
> 
>> The attached source code is a simplified version of the program we are
>> trying to prove.
>> Basically, M and L are struct type variables.
>>
>> L.M1 is equal to 0.0 and we tried to state this in the requires clause
>> with the BOUND define. Is it correct?
> 
> I don't see anything wrong with the specification. In fact, if you
> replace field M.x1 by some float variable Mx1, it will go through.
> 
>> We want to prove that M.x1 and result variable are equal to 0.0 too,
>> but the assert clauses are not proved. What is wrong?
> 
> Gappa can prove the arithmetic properties, but it does not support field
> accesses. SMT solvers support them, but they cannot cope with the
> arithmetic. Thus you are stuck, since none of the tools is powerful enough.

This analysis is unfortunately correct, but fortunately the conclusion
is too pessimistic.

This is indeed an issue that I realized before on float arrays, and I
implemented a solution in Jessie so that Gappa can prove the goals.
Unfortunately the same treatment should have been done to structs, but
wasn't.

Still, there is a workaround, but using temporary scalar variables to
help the provers. A solution is attached. It is heavy but I have no
simpler solution to propose. In an ideal world there should exists a SMT
solver able to handle the theory of floats natively. (This may happen in
the future !)

- Claude


-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |

-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: siteZero.c
Type: text/x-csrc
Taille: 451 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131008/4da217fd/attachment.c>