projects / ieee754fpu.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 11e3f3e) | patch
Allow the proof driver to check operations with integer output
authorCesar Strauss <cestrauss@gmail.com>
Sun, 17 Jan 2021 17:00:27 +0000 (14:00 -0300)
committerCesar Strauss <cestrauss@gmail.com>
Sun, 17 Jan 2021 17:14:48 +0000 (14:14 -0300)
commitce581d19b45e1ee7b414cec8b470cfc5ac27c6cd
tree3d7f6bcb9e23c11deff637c968587268dbbc0682tree
parent11e3f3eba7a589c61636ca0e4036be4ef294853acommit | diff
Allow the proof driver to check operations with integer output

The "part_out" parameter tells the driver whether the output of the
operation is supposed to be arithmetic or boolean.

Added checks for addition and subtraction, without carry.
src/ieee754/part/formal/proof_partition.py diff | blob | history