From 37fcac6fc9a176d91684ecfe45db9d057740e908 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 1 Oct 2019 06:59:48 -0500 Subject: [PATCH] Fix encoded floats appearing in relational exps. (#584) * Fix encoded floats appearing in relational exps. * Test. * Fix test. --- semantics/c/language/common/expr/relational.k | 13 +++++++++++++ tests/unit-pass/memcmp.c | 12 ++++++++++++ 2 files changed, 25 insertions(+) create mode 100644 tests/unit-pass/memcmp.c diff --git a/semantics/c/language/common/expr/relational.k b/semantics/c/language/common/expr/relational.k index e499c8861..6a5f0647c 100644 --- 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 new file mode 100644 index 000000000..d3488ed57 --- /dev/null +++ b/tests/unit-pass/memcmp.c @@ -0,0 +1,12 @@ +#include + +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)); +}