From 4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a Mon Sep 17 00:00:00 2001 From: Richard Kreckel Date: Sat, 6 Oct 2012 22:44:34 +0200 Subject: [PATCH] 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 of the CVC4 team. --- src/integer/conv/cl_I_from_digits.cc | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/integer/conv/cl_I_from_digits.cc b/src/integer/conv/cl_I_from_digits.cc index 1046204..9bf2f18 100644 --- 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; var uintD d = 0; // resulting digit 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 if (ch!='.') { // skip decimal point // Compute value of ch ('0'-'9','A'-'Z','a'-'z'):