Open FahrJo opened 1 year ago
Sadly, this is a known limitation of our rather ad-hoc ACSL support. Each assertion needs to have its own line.
In what context do you encounter programs written in such a way?
I was thinking of automatic annotation of the input program from an easier understandable specification description. By inlining all the generated assertions, the line numbers of the original input file would have been still valid for the Ultimate results (e.g. the counter example) of the "preprocessed" input file. But if it's a konwn issue, I'll find a workaround for it👍
What other specifications do you want do add? Ultimate already supports various specifications like overflows and memsafety. Checking them can be enabled in the cacsl2boogietranslator settings. Assertions for those specifications are then added directly in the translation process (without adding ACSL assertions), therefore the correct line number occurs in the result.
It is for a POC of implementing THADs (temporal HAL-API dependencies) and it probably should be done directly as a Ultimate tool in a longterm perspective, but I didn't want to dive that deep directly at the beginning ;-)
Then you might also want to look at our support for LTL properties, in particular if you are interested in properties of the form "If I call this method, I will eventually call that method".
Yes, thanks for the hint, but it isn't possible to check function calls directly, is it? So I still need helper variables?
Yes, although it would be only a small extension.
Basic Info
Description
I would expect Ultimate to work steh same way on the following two semantically identical input files:
Ultimate Result:
VS.
Ultimate Result:
In the second case, the Assertions are not even detected.