invd

@zimmerle, @client9 : thanks for the positive feedback! Given the (presumably) low severity of the memory issues and realistic chance of a patch, I have no objections to keeping the...

During private discussion, @zimmerle and I have figured out that the out of bounds reads are actually not a problem if `libinjection_xss()` is called with a pointer to a **null-terminated...

Good question, this is something for @zimmerle to decide / clarify. My original fuzzer harness was passing arbitrary bytes & length of the byte buffer, but this was not the...

While the printf() code still returns a ```RESULT: Ultimate proved your program to be correct!```, the (preprocessed) sprintf example is correctly identified as problematic for the current Ultimate versions, which...

Ultimate 0.1.23-f020fd9 manages to verify [soundness_sprintf_1.c](https://github.com/ultimate-pa/ultimate/blob/dev/trunk/examples/CToBoogieTranslation/trezor/soundness_sprintf_1.c) without preprocessing. (If the preprocessed version is used, Ultimate refuses with `UnsupportedSyntaxResult`) However, the result is **unsound**: ``` - PositiveResult [Line: 16]: array index...

The unsound error location due to a certain flag is discussed in #336.

As noted in #336, the following combination * AutomizerMemDerefMemtrack.xml * svcomp-DerefFreeMemtrack-32bit-Automizer_Default.epf * `--traceabstraction.stop.after.first.violation.was.found false` * `--rcfgbuilder.add.additional.assume.for.each.assert false` results in a verification output that includes both error locations for the *soundness_sprintf_1.c*...

Today's Ultimate fails with a null pointer exception when it is run against the unprocessed **soundness_fprintf_2.c** example: ``` ./Ultimate -tc ~/ultimate/releaseScripts/default/UAutomizer-linux/config/AutomizerMemDerefMemtrack.xml -s ~/ultimate/trunk/examples/settings/default/automizer/svcomp-DerefFreeMemtrack-32bit-Automizer_Default.epf -i ~/ultimate/trunk/examples/CToBoogieTranslation/trezor/soundness_fprintf_2.c [...] - ExceptionOrErrorResult: NullPointerException: null...

For the record, the error behavior has been improved from a **NullPointerException** to an **UnsupportedOperationException**: ``` [...] * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator: - ExceptionOrErrorResult: UnsupportedOperationException: No Boogie because C type is...

Recent Ultimate versions after the (potential) bugfix show an improved behavior that no longer references cType2AstType. Instead, the expected "UnsupportedOperationException: multibyte characters are not supported yet" is returned. If the...