diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index de8963a4cb2a86247b80fad324d2a3064b59df12..891b2fb3a4be7fafa4dad423808b06e8dae0d002 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/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 -> diff --git a/tests/syntax/oracle/wide_string.res.oracle b/tests/syntax/oracle/wide_string.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..45f305b9ae1991c78e7a32f6f3bcdf563ff7e961 --- /dev/null +++ b/tests/syntax/oracle/wide_string.res.oracle @@ -0,0 +1,16 @@ +[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; +} + + diff --git a/tests/syntax/wide_string.c b/tests/syntax/wide_string.c new file mode 100644 index 0000000000000000000000000000000000000000..9cdfcba8a0fb762da403ac1bf186f97deb706bc5 --- /dev/null +++ b/tests/syntax/wide_string.c @@ -0,0 +1,7 @@ +#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){}