invd

multiple heap out of bounds reads in libinjection_xss()

13

Mid-June, I discovered and privately reported out of bounds read issues in the XSS detection to @client9, but so far have not received a reply. The out of bounds reads...

nested ncr() calls can be very slow (potential denial of service)

4

### Issue description I've recently discovered via fuzzing with libFuzzer that nested usage of the `ncr()` expression can result in unexpectedly long expression evaluation times. The smallest representation of the...

Conform to -Wstrict-prototypes on New Compilers

1

The codebase contains a number of C functions that do not take any parameters but are not marked with `void`. This style is deprecated, and compilers warn for it with...

From what I can see in the Solo V1 source code, the firmware currently does not use or support the ARM GCC provided standard functionality to mitigate certain stack buffer...

rcfgbuilder.add.additional.assume.for.each.assert true may produce confusing / spurious results

8

As observed in #306, Ultimate flags unreachable, but incorrect code as valid. In the (shortened) example, the first out of bound read is found as an error, but the second...

Soundness issue for printf(), fprintf(), sprintf() parameters

8

Ultimate ignores operations in **printf()** statements which results in severe false negatives for error detection: [soundness_printf_1.c](https://github.com/ultimate-pa/ultimate/blob/dev/trunk/examples/CToBoogieTranslation/trezor/soundness_printf_1.c): ``` #include #include // Ultimate needs this typedef unsigned char uint8_t; uint8_t data[1]; int...

Impossible variable values in FailurePath

1

Ultimate provides impossible value assignments for certain FailurePath couterexamples. bmp is of type BITMAP, which is defined to have uint8_t width and height: ``` typedef struct { uint8_t width, height;...

Encode and enforce read-only markings in memory handling

3

This ticket is opened on behalf of @jhoenicke, who has suggested it during the last meeting. To my knowledge, Ultimate currently has no concept of memory areas which are supposed...

Ultimate does not support u'' and U'' type unicode chars and strings

7

_Note: please add the appropriate labels such as feature/enhancement_. Newer C standards are able to handle 16-bit and 32-bit unicode characters and strings. The following [unicode_u16_u32_string_test.c](https://github.com/ultimate-pa/ultimate/blob/dev/trunk/examples/CToBoogieTranslation/trezor/unicode_u16_u32_string_test.c) is valid with `gcc...

NPE: TypeHandler.cType2AstType

18

Observed in Ultimate 08d4a0152fab59f1da0c9942206f8aa51963d6ea after fixes in #359. Note that this only appears with the Automizer_Default settings, for Bitvector #378 is encountered. Settings: ``` AutomizerMemDerefMemtrack.xml svcomp-DerefFreeMemtrack-32bit-Automizer_Default.epf ``` Error message: ```...