Cleanup fmod vs IEEE remainder

1. Add tests for both the C and Java front-end.
2. Make sure we support both variants of the modulus operator on
floating-point values in the back-ends: the SMT back-end only supported
remainder (and only for FPA mode), the propositional back-end did not
distinguish between fmod and IEEE remainder.

Author: tautschnig

jbmc/regression/jbmc/farith2/farith2.class

@@ -0,0 +1,17 @@
+class farith2
+{
+  public static void main(String[] args)
+  {
+    // examples from
+    // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double
+    // and
+    // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+    double d1 = 0.5 % 0.3;
+    assert d1 == 0.2;
+    double d2 = (-0.5) % 0.3;
+    assert d2 == -0.2;
+    double x = 7.5, y = 2.1;
+    double xModY = x % y;
+    assert xModY > 1.19 && xModY < 1.21;
+  }
+}

jbmc/regression/jbmc/farith2/farith2.java

@@ -1,6 +1,6 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
+CORE
+farith2
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-library/__sort_of_CPROVER_remainder-01/test.desc renamed to jbmc/regression/jbmc/farith2/test.desc

@@ -3,7 +3,15 @@
 
 int main()
 {
-  fmod();
-  assert(0);
-  return 0;
+  // examples from
+  // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double
+  // and
+  // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod
+  double d1 = fmod(0.5, 0.3);
+  assert(d1 == 0.2);
+  double d2 = fmod(-0.5, 0.3);
+  assert(d2 == -0.2);
+  double x = 7.5, y = 2.1;
+  double xModY = fmod(x, y);
+  assert(xModY > 1.19 && xModY < 1.21);
 }

regression/cbmc-library/__sort_of_CPROVER_remainder-01/main.c

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--float-overflow-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$