ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link

Fix CArray expression evaluation/conversion to boolean value #655

Closed bahnwaerter closed 1 year ago

bahnwaerter commented 1 year ago

This patch fixes the CArray expression evaluation/conversion to a boolean value to allow a CArray evaluation in a boolean expression:

assert(a != b && "This is a CArray error message")

In this example, the CArray as part of the conjunction will be always evaluated with an address check (memory address of CArray != NULL) to the boolean value true since the address of the error message string literal can never be NULL.

schuessf commented 1 year ago

The example does not quite show, what you want to change or do I missunderstand something here? The problematic example here would be assert(a), where a is an array, right?

bahnwaerter commented 1 year ago

The example does not quite show, what you want to change or do I missunderstand something here? The problematic example here would be assert(a), where a is an array, right?

Without the patch, Ultimate cannot handle CArrays in boolean expressions. And yes, your problematic example will be covered as well. In this case, the assertion should always hold (what it indeed does).

schuessf commented 1 year ago

So, we also crash on assert(a != b) right now, or what is the behavior?

bahnwaerter commented 1 year ago

So, we also crash on assert(a != b) right now, or what is the behavior?

No, assume that a and b are valid terms (boolean expressions), then we only have problems if the string literal comes into play.