Skip to content

Conversation

@keyboardDrummer
Copy link
Contributor

@keyboardDrummer keyboardDrummer commented Dec 24, 2025

Changes

  • Update testing infrastructure so the Laurel examples that include expected diagnostics can be run from the file where they are defined in.
    • Updated Laurel tests T1 to T10 to use this
  • Add a ToFormat instance for the Laurel type to help with debugging
  • Make changes so that Laurel test T2 and T3 pass.
    • This includes simple extensions to ConcreteToAbstractTreeTranslator and LaurelToBoogieTranslator, which perform 1-1 translations.
    • The most interesting change is the addition of LiftExpressionAssignments, which attempts to lift any assignments that occur in an expression position so they are done in the innermost enclosing statement block instead.

Caveats

I think there are a lot of cases of impure expressions that either don't translate correctly or fail to translate. It would be good to add explicit tests for those and to return not supported diagnostics in those cases. Created a GH issue to address something that's not supported: #282

Testing

  • Laurel T2 and T3 are now running and passing as well.

@shigoel shigoel enabled auto-merge December 26, 2025 21:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants