Skip to content

Commit

Permalink
this commit is out of control, started as preventing asserts against …
Browse files Browse the repository at this point in the history
…expired states, became something different, plus clean up
  • Loading branch information
mbellotti committed Feb 10, 2023
1 parent 155de37 commit 853751c
Show file tree
Hide file tree
Showing 7 changed files with 425 additions and 573 deletions.
20 changes: 5 additions & 15 deletions listener/listener.go
Original file line number Diff line number Diff line change
Expand Up @@ -1297,21 +1297,11 @@ func (l *FaultListener) ExitAssertion(c *parser.AssertionContext) {
}
case *ast.InfixExpression:

if e.Operator == "==" {
con = &ast.InvariantClause{
Token: e.Token,
Left: &ast.Boolean{Value: true},
Operator: "==",
Right: e,
}
} else {

con = &ast.InvariantClause{
Token: e.Token,
Left: e.Left,
Operator: e.Operator,
Right: e.Right,
}
con = &ast.InvariantClause{
Token: e.Token,
Left: e.Left,
Operator: e.Operator,
Right: e.Right,
}
case *ast.InvariantClause:
con = e
Expand Down
2 changes: 1 addition & 1 deletion preprocess/preprocess_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -452,7 +452,7 @@ func TestAsserts(t *testing.T) {
t.Fatalf("assumption var name 1 not correct got=%s", str1)
}

str1a := spec[4].(*ast.AssertionStatement).Constraint.Left.(ast.Nameable).RawId()
str1a := spec[4].(*ast.AssertionStatement).Constraint.Right.(*ast.InfixExpression).Left.(ast.Nameable).RawId()
if len(str1a) != 3 || str1a[0] != "test1" || str1a[1] != "foo" || str1a[2] != "bar" {
t.Fatalf("assumption var name 2 not correct got=%s", str1a)
}
Expand Down
346 changes: 0 additions & 346 deletions smt/asserts-new.go

This file was deleted.

0 comments on commit 853751c

Please sign in to comment.