strtol must not overflow

regression/cbmc-library/strtol-02/test.desc

@@ -1,8 +1,11 @@
 CORE
 main.c
-
+--signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Even with --signed-overflow-check enabled, verification should succeed here as
+strtol reports overflow condition with errno set to ERANGE.

src/ansi-c/library/stdlib.c

@@ -353,16 +353,23 @@ inline long strtol(const char *nptr, char **endptr, int base)
       break;
 
     in_number=1;
-    long res_before=res;
-    res=res*base+ch-sub;
-    if(res<res_before)
+    _Bool overflow = __CPROVER_overflow_mult(res, (long)base);
+#pragma CPROVER check push
+#pragma CPROVER check disable "signed-overflow"
+    // This is now safe; still do it within the scope of the pragma to avoid an
+    // unnecessary assertion to be generated.
+    if(!overflow)
+      res *= base;
+#pragma CPROVER check pop
+    if(overflow || __CPROVER_overflow_plus(res, (long)(ch - sub)))
     {
       errno=ERANGE;
       if(sign=='-')
         return LONG_MIN;
       else
         return LONG_MAX;
     }
+    res += ch - sub;
   }
 
   if(endptr!=0)