[RFC] Handling infinity in the back-end

The test demonstrates that we currently do not handle infinity_exprt in
the back-end, although the C front-end can legitimately generate such
expressions.

Author: tautschnig

Diff for: regression/cbmc/infinity1/main.c

@@ -0,0 +1,6 @@
+int A[__CPROVER_constant_infinity_uint];
+
+int main()
+{
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(A) > 0, "infinity is positive");
+}

Diff for: regression/cbmc/infinity1/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring