From 2653a4e6fec428a1c1c3fc256d641a0a76041986 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 16 Mar 2020 15:32:18 +0100
Subject: [PATCH] [ACSL] fixes casts to unsigned short int
---
src/kernel_internals/parsing/logic_parser.mly | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index c95a783a030..b19f7e478bd 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -812,6 +812,9 @@ type_spec:
| SHORT { LTint IShort } /** [short] */
| SIGNED SHORT { LTint IShort } /** [short] */
| UNSIGNED SHORT { LTint IUShort } /** [unsigned short] */
+| SHORT INT { LTint IShort } /** [short] */
+| SIGNED SHORT INT { LTint IShort } /** [short] */
+| UNSIGNED SHORT INT { LTint IUShort } /** [unsigned short] */
| LONG { LTint ILong } /** [long] */
| SIGNED LONG { LTint ILong } /** [long] */
| UNSIGNED LONG { LTint IULong } /** [unsigned long] */
--
GitLab