Browse Source

Fix integer input with leading zeros in power-of-two base.

Reading leading '0' characters in integers of base 2, 4, 8, 16, or 32
could result in a NUDS with leading zero digits. This is against the
rules. The result was a misbehaving cl_I down the road.

Thanks to Morgan Deters <mdeters@cs.nyu.edu> of the CVC4 team.
master
Richard Kreckel 12 years ago
parent
commit
4a477b0cc3
  1. 6
      src/integer/conv/cl_I_from_digits.cc

6
src/integer/conv/cl_I_from_digits.cc

@ -28,7 +28,11 @@ static const cl_I digits_to_I_base2 (const char * MSBptr, uintC len, uintD base)
erg_MSDptr = erg_LSDptr; erg_len = 0; erg_MSDptr = erg_LSDptr; erg_len = 0;
var uintD d = 0; // resulting digit var uintD d = 0; // resulting digit
var int ch_where = 0; // position of ch inside d var int ch_where = 0; // position of ch inside d
while (len > 0) {
var uintC min_len = 0; // first non-zero digit
while (min_len < len && *(const uintB *)(MSBptr+min_len) == '0') {
++min_len;
}
while (len > min_len) {
var uintB ch = *(const uintB *)(MSBptr+len-1); // next character var uintB ch = *(const uintB *)(MSBptr+len-1); // next character
if (ch!='.') { // skip decimal point if (ch!='.') { // skip decimal point
// Compute value of ch ('0'-'9','A'-'Z','a'-'z'): // Compute value of ch ('0'-'9','A'-'Z','a'-'z'):

Loading…
Cancel
Save