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] 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>