XSTS-cli: Verifying a model with syntax errors should fail #303
Description
Theta version: docker 6.5.2
XSTS-cli ignores certain syntactical errors if the lexer can construct something meaningful out of the input model.
Example input:
var x : integer = 0
trans {
choice {
assume (x == 2);
} else {
x := 10;
}
}
init {}
env {}
prop {
x != 0
}
Expected outcome: Theta fails since else can't come after 'choice'
Actual outcome: Theta outputs the syntax errors, and continues by "covering" the 'else' branch.
stderr:
line 8:6 extraneous input 'else' expecting {'if', 'havoc', 'assume', 'choice', 'for', '{', '}', 'local', ID}
stdout:
Iteration 1
| Checking abstraction...
| | (Re)initializing ARG...done
| | Building ARG...done
| Checking abstraction done, result: (AbstractorResult Unsafe)
| Refining abstraction...
| | Checking trace...done, result: (ExprTraceStatus Feasible)
Refining abstraction done, result: (RefinerResult Unsafe)
! Precision did NOT change in this iteration
(SafetyResult Unsafe Trace length: 0)
CEX:
(XstsStateSequence (XstsState pre_init last_env (ExplState (x 0))))
Return code: 0
Proposed solution:
Theta should throw an exception if there are any syntactical errors.