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.

diff --git a/src/integer/conv/cl_I_from_digits.cc b/src/integer/conv/cl_I_from_digits.cc
index 1046204a2ab9ede3437e09114b907b2db30f5540..9bf2f183963d3caa910a74c378f6f2d376dd41f4 100644 (file)
--- a/src/integer/conv/cl_I_from_digits.cc
+++ b/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;\r
        var uintD d = 0;  // resulting digit\r
        var int ch_where = 0;  // position of ch inside d\r
-       while (len > 0) {\r
+       var uintC min_len = 0;  // first non-zero digit\r
+       while (min_len < len && *(const uintB *)(MSBptr+min_len) == '0') {\r
+           ++min_len;\r
+       }\r
+       while (len > min_len) {\r
                var uintB ch = *(const uintB *)(MSBptr+len-1); // next character\r
                if (ch!='.') { // skip decimal point\r
                        // Compute value of ch ('0'-'9','A'-'Z','a'-'z'):\r