Missing typecast for hexadecimal format of floating point value

[yangzao]

Description

Original code:

((double)(13134243433))

Decompiled code:

0x420876e533480000

0x420876e533480000 is the hexadecimal format of 13134243433.0,
but there is no explicit typecasting for it, which makes it being considered as a long long integer.

Steps to reproduce the bug

Files:
2.zip

1. compile orig.c with GCC and -O0
2. decompile the compiled program with angr
3. in the decompiled code, go to func_1() and the issue is at the for loop near the end of func_1().

Environment

No response

Additional context

No response