Merge branch 'fix/typing/wide-string' into 'master'

Correctly compute `sizeof(L"wide string")`

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

src/kernel_services/ast_queries/cil.ml

@@ -4590,6 +4590,10 @@ and constFold (machdep: bool) (e: exp) : exp =
       try kinteger ~loc theMachine.kindOfSizeOf (bytesSizeOf t)
       with SizeOfError _ -> e
     end
+  | SizeOfE { enode = Const (CWStr l) } when machdep ->
+    let len = List.length l in
+    let wchar_size = bitsSizeOfInt theMachine.wcharKind / 8 in
+    kinteger ~loc theMachine.kindOfSizeOf ((len + 1) * wchar_size)
   | SizeOfE e when machdep ->
     constFold machdep (new_exp ~loc:e.eloc (SizeOf (typeOf e)))
   | SizeOfStr s when machdep ->

tests/syntax/oracle/wide_string.res.oracle

+[kernel] Parsing wide_string.c (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.h"
+#include "signal.h"
+#include "string.h"
+#include "strings.h"
+#include "time.h"
+#include "wchar.h"
+int main(void)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+

tests/syntax/wide_string.c

+#include <wchar.h>
+
+_Static_assert(sizeof(L"AA") == 3*sizeof(wchar_t), "Incorrect sizeof behaviour");
+
+_Static_assert(sizeof(L"\123\456") == 3*sizeof(wchar_t), "Incorrect handling of escape sequences");
+
+int main(void){}