Merge branch 'master' into latest

kframework · Oct 1, 2019 · 8520764 · 8520764
2 parents b57da64 + 37fcac6
commit 8520764
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 0 deletions.
diff --git a/semantics/c/language/common/expr/relational.k b/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)

diff --git a/tests/unit-pass/memcmp.c b/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));
+}