silver icon indicating copy to clipboard operation
silver copied to clipboard
verified publisher icon viperproject

(AdtPlugin) fixes and regression tests for #581

Open Pointerbender opened this issue 3 years ago • 2 comments

The new ADT plugin did not handle result expressions in post-conditions yet properly. This PR is a patch to fix a couple of corner cases with additional regression tests.

Pointerbender avatar May 27 '22 10:05 Pointerbender

Thank you for investigating the issue. I assume the PR is WIP until a complete solution is found. If so, please mark the PR as such, so that it doesn't get merged accidentally, or code-reviewed prematurely.

mschwerhoff avatar May 30 '22 07:05 mschwerhoff

I just converted this PR to draft. Although the work-around in this PR works, I suspect a better solution will come out of #581. It seems to be related to a problem in the transformer logic itself and the final fix is probably better addressed in that part of the code (hoping someone might look alongside to see what the issue is in the transformer, I didn't have much luck spotting it yet :) ). Thanks!

Pointerbender avatar May 30 '22 08:05 Pointerbender