--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Strange results when verifying bitshifts using frama-c v19.1 with z3



Thank you for the detailed answer.
I will do manual smoke tests for now then

// Nauck

On Mon, Jan 13, 2020 at 12:14 PM Loïc Correnson <loic.correnson at cea.fr>
wrote:

> > How do I know if I get another false positive again?
>
> The Frama-C/WP simplifiers are checked with an extensive base of test
> cases, build from community  feedback and industrial test cases.
> Bitwise operations have been widely exercised during the last 5 years, but
> they are the more complex Frama-C simplifiers we have ever developed.
> Hence, we might still find some (hopefully rare) bugs in them.
>
> We are working on two directions to improve this situation:
>
> 1. Smoke tests: this is an automated way of trying to prove (!P) instead
> of P in order to detect specification inconsistencies or bugs.
> 2. Formally verified simplifiers: use only simplification routines that
> have been proved with Why-3 and Coq or SMT solvers.
>
> We hope to release (1) during 2020 ; (2) is an on-going, long-term
> research work and we have an opened PhD position on this subject.
>
> Regards,
>         L.
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200116/a783e63d/attachment.html>