• Stefan Krah's avatar
    The divmod function for large numbers now has an ACL2 proof. Related changes: · 3c23a87e
    Stefan Krah yazdı
      1) Rename _mpd_qbarrett_divmod into _mpd_base_ndivmod: The function is
         only marginally related to either Barrett's algorithm or to the version
         in Hasselstrom's paper.
    
      2) In places where the proof assumes exact operations, use new versions of
         add/sub/multiply that set NaN/Invalid_operation if this condition is
         not met. According to the proof this cannot happen, so this should be
         regarded as an extra safety net.
    
      3) Raise Division_impossible for operands with a number of digits greater
         than MPD_MAX_PREC. This facilitates the audit of the function and can
         practically only occur in the 32-bit version under conditions where
         a MemoryError is already imminent.
    
      4) Use _mpd_qmul() in places where the result can exceed MPD_MAX_PREC in
         a well defined manner.
    
      5) Test for mpd_isspecial(qq) in a place where the addition of one
         can theoretically trigger a Malloc_error.
    
      6) Remove redundant code in _mpd_qdivmod().
    
      7) Add many comments.
    3c23a87e
Adı
Son kayıt (commit)
Son güncelleme
Doc Loading commit data...
Grammar Loading commit data...
Include Loading commit data...
Lib Loading commit data...
Mac Loading commit data...
Misc Loading commit data...
Modules Loading commit data...
Objects Loading commit data...
PC Loading commit data...
PCbuild Loading commit data...
Parser Loading commit data...
Python Loading commit data...
Tools Loading commit data...
.bzrignore Loading commit data...
.gitignore Loading commit data...
.hgeol Loading commit data...
.hgignore Loading commit data...
.hgtags Loading commit data...
LICENSE Loading commit data...
Makefile.pre.in Loading commit data...
README Loading commit data...
config.guess Loading commit data...
config.sub Loading commit data...
configure Loading commit data...
configure.ac Loading commit data...
install-sh Loading commit data...
pyconfig.h.in Loading commit data...
setup.py Loading commit data...