Merge pull request #1183 from romainbrenguier/bugfix/character-digit#851

Adapt convert_digit_char for the case without radix argument

Author: romainbrenguier

regression/strings/CharacterGetNumericValue/test.class

@@ -0,0 +1,9 @@
+CORE
+test.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test.java line 8 .* SUCCESS$
+assertion at file test.java line 10 .* FAILURE$
+--
+^warning: ignoring

regression/strings/CharacterGetNumericValue/test.desc

@@ -0,0 +1,12 @@
+public class test
+{
+
+    public static void main(String[] args)
+    {
+        char c = 'a';
+        if(args.length>1)
+            assert Character.getNumericValue(c) == 10;
+        else
+            assert Character.getNumericValue(c) != 10;
+    }
+}

regression/strings/CharacterGetNumericValue/test.java

@@ -126,15 +126,22 @@ codet character_refine_preprocesst::convert_compare(conversion_inputt &target)
 
 
 /// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.digit:(CI)I
+/// the java method Character.digit:(CI)I. The function call has one character
+/// argument and an optional integer radix argument. If the radix is not given
+/// it is set to 36 by default.
 /// \param target: a position in a goto program
+/// \return code assigning the result of the Character.digit function to the
+///         left-hand-side of the given target
 codet character_refine_preprocesst::convert_digit_char(
   conversion_inputt &target)
 {
   const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==2);
+  const std::size_t nb_args=function_call.arguments().size();
+  PRECONDITION(nb_args==1 || nb_args==2);
   const exprt &arg=function_call.arguments()[0];
-  const exprt &radix=function_call.arguments()[1];
+  // If there is no radix argument we set it to 36 which is the maximum possible
+  const exprt &radix=
+    nb_args>1?function_call.arguments()[1]:from_integer(36, arg.type());
   const exprt &result=function_call.lhs();
   const typet &type=result.type();