https://gcc.gnu.org/bugzilla/show_bug.cgi?id=117760
Matteo Nicoli <matteo.nicoli001 at gmail dot com> changed:
What |Removed |Added
----------------------------------------------------------------------------
CC| |matteo.nicoli001 at gmail dot
com
--- Comment #3 from Matteo Nicoli <matteo.nicoli001 at gmail dot com> ---
Created attachment 62197
--> https://gcc.gnu.org/bugzilla/attachment.cgi?id=62197&action=edit
Formal verification of the properties
Hi Andrew.
I took the liberty of formally verifying the properties using SMTLIB2 language
(file attached that can be executed with Z3).
Are these special properties (used specifically for something), or are they
simply mathematical identities? In the latter case, I could build a script that
of this type of property, (and symbolically verify them) for binary, ternary,
etc. functions in order to obtain a list (as large as desired) of similar
identities.
However, if no one is working on this bug, I'd like to start myself.
