[typing] always push current pack status on pragma pack push directives

Even if we don't know what to do with the argument of the push, this at least
ensures that push/pop directives stay well parenthesized.

src/kernel_internals/typing/cabs2cil.ml

@@ -448,6 +448,19 @@ let process_pack_pragma name args =
             current_packing_pragma:= new_pragma; None
           end else
             Some (Attr (name, args))
+        | ACons ("push",[]) :: args (* unknown push directive *) ->
+          Kernel.warning ~current:true
+            "Unsupported argument for pragma pack push directive: `%a'."
+            Format.(
+              pp_print_list
+                ~pp_sep:(fun fmt ()->pp_print_string fmt ", ")
+                Cil_printer.pp_attrparam)
+            args;
+          (* We don't change the current packing directive, but
+             nevertheless push it on the stack, to avoid a mismatched
+             pop somewhere later. *)
+          Stack.push !current_packing_pragma packing_pragma_stack;
+          None
         | [ACons ("pop",[])] (* #pragma pack(pop) *) ->
           begin try
               current_packing_pragma := Stack.pop packing_pragma_stack;

tests/syntax/oracle/pragma.res.oracle

+[kernel] Parsing tests/syntax/pragma.i (no preprocessing)
+[kernel] tests/syntax/pragma.i:1: Warning: 
+  Unsupported argument for pragma pack push directive: `_CRT_PACKING'.
+/* Generated by Frama-C */
+int main(void)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+

tests/syntax/pragma.i

+#pragma pack(push, _CRT_PACKING)
+#pragma pack(pop)
+int main() {
+    return 0;
+}