Merge branch 'fix/acsl-cast--to-unsigned-short-int' into 'master'

[ACSL] fixes casts to unsigned short int

See merge request frama-c/frama-c!2575

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] */

tests/spec/cast_int.i

+unsigned short int toto;
+
+/*@ensures toto==(unsigned short int)param;*/
+int F(int param){
+return 0;
+}

tests/spec/oracle/cast_int.res.oracle

+[kernel] Parsing tests/spec/cast_int.i (no preprocessing)
+/* Generated by Frama-C */
+unsigned short toto;
+/*@ ensures toto ≡ (unsigned short)\old(param); */
+int F(int param)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+