Skip to content

Conversation

@arminzavada
Copy link
Member

@arminzavada arminzavada commented Nov 28, 2025

closes #303

@arminzavada arminzavada self-assigned this Nov 28, 2025
@arminzavada arminzavada force-pushed the xsts-parser-error-handling branch from b360291 to 4c81e74 Compare November 28, 2025 22:30
mondokm
mondokm previously approved these changes Nov 28, 2025
Copy link
Contributor

@mondokm mondokm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is great, thank you!:)

@mondokm
Copy link
Contributor

mondokm commented Nov 28, 2025

I think the folder names correct-models and incorrect-models might be confusing (one might think they indicate whether the model is safe or unsafe). I would rename the former to simply models as before, and the latter to syntax-error-models.

ctrl var n: integer = 0

trans{
arr:=arr[n<--true];
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we would need semantic validation in order to throw an error here, syntactically -true is a valid expression.

@github-actions
Copy link
Contributor

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

Rundefinition COMPLEX EMERGENT HORN
SV-COMP25_no-data-race ✅ (59 / 0 / 89) HTML/CSV ✅ (32 / 0 / 68) HTML/CSV ✅ (20 / 0 / 83) HTML/CSV
SV-COMP25_no-overflow ✅ (17 / 0 / 49) HTML/CSV ❓ (0 / 0 / 37) HTML/CSV ❓ (0 / 0 / 67) HTML/CSV
SV-COMP25_termination ✅ (1 / 0 / 204) HTML/CSV ✅ (1 / 0 / 207) HTML/CSV ✅ (14 / 0 / 304) HTML/CSV
SV-COMP25_unreach-call ✅ (18 / 0 / 94) HTML/CSV ✅ (16 / 0 / 94) HTML/CSV ✅ (9 / 0 / 137) HTML/CSV
SV-COMP25_valid-memcleanup ❓ (0 / 0 / 66) HTML/CSV ❓ (0 / 0 / 66) HTML/CSV ❓ (0 / 0 / 66) HTML/CSV
SV-COMP25_valid-memsafety ✅ (34 / 0 / 311) HTML/CSV ✅ (3 / 0 / 285) HTML/CSV ❓ (0 / 0 / 423) HTML/CSV

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.

XSTS-cli: Verifying a model with syntax errors should fail

3 participants