Merge pull request #8324 from tautschnig/bugfixes/mathematical-types

Fix support for mathematical types

Author: tautschnig

regression/cbmc/rational1/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  __CPROVER_rational x;
+  __CPROVER_rational y;
+  x = 6 / 10;
+  y = 3 / 5;
+
+  __CPROVER_assert(y + 1 != x, "should pass");
+  __CPROVER_assert(y != x, "should fail");
+}

regression/cbmc/rational1/test.desc

@@ -0,0 +1,10 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--trace --smt2
+^\[main.assertion.2\] line 9 should fail: FAILURE$
+^\s*x=3/5
+^\s*y=3/5
+^\*\* 1 of 2 failed
+^EXIT=10$
+^SIGNAL=0$
+--

regression/cbmc/rational1/typecheck.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^[[:space:]]*ASSIGN main::1::x := 3/5
+^[[:space:]]*ASSIGN main::1::y := 3/5
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cbmc/real-assignments1/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  __CPROVER_real a, b;
+  a = 0;
+  b = a;
+  b++;
+  b *= 100;
+  __CPROVER_assert(0, "");
+}

regression/cbmc/real-assignments1/test.desc

@@ -0,0 +1,7 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--trace --smt2
+^EXIT=10$
+^SIGNAL=0$
+^  b=100
+--

regression/cbmc/real-assignments1/typecheck.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^[[:space:]]*ASSIGN main::1::b := main::1::b \* cast\(100, ℝ\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^[[:space:]]*ASSIGN main::1::b := main::1::b \* 100$

regression/cbmc/real-irrational1/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  __CPROVER_real a;
+  __CPROVER_real a2 = a * a;
+  __CPROVER_assert(a2 != 2, "");
+}

regression/cbmc/real-irrational1/test.desc

@@ -0,0 +1,8 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--trace --smt2
+^  a=x ∈ ℝ\.\(x\^2 \+ -2 = 0\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/validate-trace-xml-schema/check.py

@@ -29,7 +29,9 @@
     ['enum_is_in_range', 'enum_test3-simplified.desc'],
     ['enum_is_in_range', 'format.desc'],
     ['r_w_ok9', 'simplify.desc'],
+    ['rational1', 'typecheck.desc'],
     ['reachability-slice-interproc2', 'test.desc'],
+    ['real-assignments1', 'typecheck.desc'],
     ['saturating_arithmetric', 'output-goto.desc'],
     # this one wants show-properties instead producing a trace
     ['show_properties1', 'test.desc'],
@@ -80,7 +82,9 @@
     ['integer-assignments1', 'test.desc'],
     # this test is expected to abort, thus producing invalid XML
     ['String_Abstraction17', 'test.desc'],
-    ['Quantifiers1', 'quantifier-with-side-effect.desc']
+    ['Quantifiers1', 'quantifier-with-side-effect.desc'],
+    # this test produces unicode output that cannot be decoded as ASCII
+    ['real-irrational1', 'test.desc']
 ]))
 
 # TODO maybe consider looking them up on PATH, but direct paths are

src/ansi-c/ansi_c_internal_additions.cpp

@@ -144,7 +144,9 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
       " " CPROVER_PREFIX "ssize_t;\n"
     "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
     "typedef void " CPROVER_PREFIX "integer;\n"
+    "typedef void " CPROVER_PREFIX "natural;\n"
     "typedef void " CPROVER_PREFIX "rational;\n"
+    "typedef void " CPROVER_PREFIX "real;\n"
     "extern unsigned char " CPROVER_PREFIX "memory["
       CPROVER_PREFIX "constant_infinity_uint];\n"