Fix encoded floats appearing in relational exps. (#584)

* Fix encoded floats appearing in relational exps.

* Test.

* Fix test.

Author: chathhorn

semantics/c/language/common/expr/relational.k

@@ -341,6 +341,19 @@ module C-COMMON-EXPR-RELATIONAL
           requires notBool hasLint
           [structural]
 
+     rule tv(encodedValue(V:EncodableValue, N:Int, M:Int), T::UType) == tv(encodedValue(V':EncodableValue, N, M), T'::UType)
+          => tv(V, T) == tv(V', T')
+     rule tv(encodedValue(V:EncodableValue, N:Int, M:Int), T::UType) != tv(encodedValue(V':EncodableValue, N, M), T'::UType)
+          => tv(V, T) != tv(V', T')
+     rule tv(encodedValue(V:EncodableValue, N:Int, M:Int), T::UType) < tv(encodedValue(V':EncodableValue, N, M), T'::UType)
+          => tv(V, T) < tv(V', T')
+     rule tv(encodedValue(V:EncodableValue, N:Int, M:Int), T::UType) <= tv(encodedValue(V':EncodableValue, N, M), T'::UType)
+          => tv(V, T) <= tv(V', T')
+     rule tv(encodedValue(V:EncodableValue, N:Int, M:Int), T::UType) > tv(encodedValue(V':EncodableValue, N, M), T'::UType)
+          => tv(V, T) > tv(V', T')
+     rule tv(encodedValue(V:EncodableValue, N:Int, M:Int), T::UType) >= tv(encodedValue(V':EncodableValue, N, M), T'::UType)
+          => tv(V, T) >= tv(V', T')
+
      rule tv(encodedPtr(Loc:SymLoc, N:Int, M:Int), T::UType) == tv(encodedPtr(Loc':SymLoc, N:Int, M:Int), T'::UType)
           => tv(Loc, T) == tv(Loc', T')
      rule tv(encodedPtr(Loc:SymLoc, N:Int, M:Int), T::UType) != tv(encodedPtr(Loc':SymLoc, N:Int, M:Int), T'::UType)

tests/unit-pass/memcmp.c

@@ -0,0 +1,12 @@
+#include <string.h>
+
+int main() {
+      int x = 1;
+      float y = 1;
+      double z = 1;
+      int * p = &x;
+      return memcmp(&x, &x, sizeof(x))
+          || memcmp(&y, &y, sizeof(y))
+          || memcmp(&z, &z, sizeof(z))
+          || memcmp(&p, &p, sizeof(p));
+}