Fixes for Match (#585)

* Update OS profile to be 64-bit platform. * Fixes for Match. * Another 64bit type update. * Fix dumb regression. * Fix.
kframework · Oct 2, 2019 · a293965 · a293965
1 parent 37fcac6
commit a293965
Show file tree

Hide file tree

Showing 10 changed files with 37 additions and 17 deletions.
diff --git a/profiles/x86-gcc-limited-libc/include/library/stdint.h b/profiles/x86-gcc-limited-libc/include/library/stdint.h
@@ -74,26 +74,24 @@ typedef unsigned long long int uint_fast64_t;
 # define INT_FAST64_MAX		(9223372036854775807LL)
 # define UINT_FAST64_MAX		(18446744073709551615ULL)
 
-
 // intptr_t and uintptr_t are optional
-typedef signed int intptr_t;
-typedef unsigned int uintptr_t;
+typedef signed long int intptr_t;
+typedef unsigned long int uintptr_t;
 
 typedef signed long long int intmax_t;
 typedef unsigned long long int uintmax_t;
 # define INTMAX_MIN		(-9223372036854775807LL-1)
 # define INTMAX_MAX		(9223372036854775807LL)
 # define UINTMAX_MAX		(18446744073709551615ULL)
 
-# define PTRDIFF_MIN (-2147483647-1)
-# define PTRDIFF_MAX (2147483647)
+# define PTRDIFF_MIN		(-9223372036854775807L-1)
+# define PTRDIFF_MAX		(9223372036854775807L)
 
-# define SIZE_MAX	(4294967295U)
+# define SIZE_MAX		(18446744073709551615UL)
 
 # define WCHAR_MIN (-2147483647-1)
 # define WCHAR_MAX (2147483647)
 
-
 # define INT8_C(value) ((int_least8_t) value)
 # define INT16_C(value) ((int_least16_t) value)
 # define INT32_C(value) ((int_least32_t) value)

diff --git a/profiles/x86-gcc-limited-libc/semantics/c-settings.k b/profiles/x86-gcc-limited-libc/semantics/c-settings.k
@@ -24,7 +24,7 @@ module C-SETTINGS
      rule cfg:sizeofSignedChar => 1
      rule cfg:sizeofShortInt => 2
      rule cfg:sizeofInt => 4
-     rule cfg:sizeofLongInt => 4
+     rule cfg:sizeofLongInt => 8
      rule cfg:sizeofLongLongInt => 8
      rule cfg:sizeofOversizedInt => 16
      rule cfg:sizeofFloat => 4
@@ -49,21 +49,21 @@ module C-SETTINGS
      rule cfg:sizeut => unsigned-long-int
      rule cfg:wintut => unsigned-int
      rule cfg:wcharut => int
-     rule cfg:ptrsize => 4
-     rule cfg:ptrdiffut => int
+     rule cfg:ptrsize => 8
+     rule cfg:ptrdiffut => long-int
 
      rule cfg:alignofBool => 1
      rule cfg:alignofSignedChar => 1
      rule cfg:alignofShortInt => 2
      rule cfg:alignofInt => 4
-     rule cfg:alignofLongInt => 4
+     rule cfg:alignofLongInt => 8
      rule cfg:alignofLongLongInt => 8
      rule cfg:alignofOversizedInt => 16
      rule cfg:alignofFloat => 4
      rule cfg:alignofDouble => 8
      rule cfg:alignofLongDouble => 16
      rule cfg:alignofOversizedFloat => 16
-     rule cfg:alignofPointer => 4
+     rule cfg:alignofPointer => 8
      // Max of the above.
      rule cfg:alignofMalloc => 16
 

diff --git a/semantics/c/language/common/dynamic.k b/semantics/c/language/common/dynamic.k
@@ -93,7 +93,8 @@ module C-DYNAMIC-SYNTAX
      syntax KItem ::= "comma"
      // these are semantic
 
-     syntax NoInit ::= initValue(CId, Type, K)
+     syntax KResult ::= initValue(CId, Type, K)
+     syntax NoInit
      syntax KResult ::= NoInit
 
      syntax CompoundLiteralId ::= compoundLiteral(Int)

diff --git a/semantics/c/language/translation/decl/global.k b/semantics/c/language/translation/decl/global.k
@@ -788,4 +788,6 @@ module C-DECL-GLOBAL
           requires notBool areDeclCompat(T, T')
           [structural]
 
+     rule isNoInit(initValue(_, _, .K)) => true
+
 endmodule
diff --git a/semantics/c/language/translation/syntax.k b/semantics/c/language/translation/syntax.k
@@ -181,7 +181,6 @@ module C-ABSTRACT-SYNTAX
      and init_name = name * init_expression
      */
      syntax KItem ::= InitName(KItem, K) [symbol]
-     context InitName(_, (HOLE:KItem => reval(HOLE))) [ndheat, result(RValue)]
 
      /*
      (* Single names are for declarations that cannot come in groups, like

diff --git a/semantics/c/library/stdio.k b/semantics/c/library/stdio.k
@@ -960,7 +960,7 @@ module LIBC-STDIO
           requires notBool isReadable(Mode)
           [structural]
      rule <k> fscanf'(FD::FD, _,
-               (ListItem(" ") => .List) _,
+               (ListItem(whitespace) => .List) _,
                _,
                _ => "",
                _)
@@ -1037,7 +1037,7 @@ module LIBC-STDIO
           [structural]
      rule str(C::String)
           ~> fscanf'(_, _,
-               (ListItem(" ") => .List) _,
+               (ListItem(whitespace) => .List) _,
                _,
                _ => "",
                _)
@@ -1446,7 +1446,7 @@ module LIBC-STDIO
 
      syntax List ::= "parseFormat'" "(" ParseResult "," Bool ")" [function]
      rule parseFormat'(parseResult(D::Directive, L::List), false)
-          => ListItem(" ") ListItem(normalizeDirective(D)) parseFormat(L)
+          => ListItem(whitespace) ListItem(normalizeDirective(D)) parseFormat(L)
           requires isSpaceSkipDirective(D)
      rule parseFormat'(parseResult(D::Directive, L::List), true)
           => ListItem(normalizeDirective(D)) parseFormat(L)

diff --git a/tests/unit-pass/pr28778.c → tests/unit-fail/pr28778.c b/tests/unit-pass/pr28778.c → tests/unit-fail/pr28778.c
diff --git a/tests/unit-fail/pr28778.c.ref b/tests/unit-fail/pr28778.c.ref
@@ -0,0 +1,10 @@
+Conversion to a pointer type with a stricter alignment requirement (possibly undefined):
+      > in find at pr28778.c:18:3
+        in main at pr28778.c:31:3
+
+    Undefined behavior (UB-CCV11):
+        see C11 section 6.3.2.3:7 http://rvdoc.org/C11/6.3.2.3
+        see C11 section J.2:1 item 25 http://rvdoc.org/C11/J.2
+        see CERT-C section EXP36-C http://rvdoc.org/CERT-C/EXP36-C
+        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1
+
diff --git a/tests/unit-pass/pr36343.c → tests/unit-fail/pr36343.c b/tests/unit-pass/pr36343.c → tests/unit-fail/pr36343.c
diff --git a/tests/unit-fail/pr36343.c.ref b/tests/unit-fail/pr36343.c.ref
@@ -0,0 +1,10 @@
+Conversion to a pointer type with a stricter alignment requirement (possibly undefined):
+      > in foo at pr36343.c:20:5
+        in main at pr36343.c:29:3
+
+    Undefined behavior (UB-CCV11):
+        see C11 section 6.3.2.3:7 http://rvdoc.org/C11/6.3.2.3
+        see C11 section J.2:1 item 25 http://rvdoc.org/C11/J.2
+        see CERT-C section EXP36-C http://rvdoc.org/CERT-C/EXP36-C
+        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1
+