Allow "property" in immediate assertions

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-04-12 14:28:28 +02:00
parent 2f0ecff71c
commit 66ffc99695
1 changed files with 22 additions and 19 deletions

View File

@ -1236,39 +1236,42 @@ opt_label:
$$ = NULL; $$ = NULL;
}; };
opt_property:
TOK_PROPERTY | /* empty */;
assert: assert:
TOK_ASSERT '(' expr ')' ';' { TOK_ASSERT opt_property '(' expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $3)); ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $4));
} | } |
TOK_ASSUME '(' expr ')' ';' { TOK_ASSUME opt_property '(' expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3)); ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
} | } |
TOK_ASSERT '(' TOK_EVENTUALLY expr ')' ';' { TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $4)); ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $5));
} | } |
TOK_ASSUME '(' TOK_EVENTUALLY expr ')' ';' { TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $4)); ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $5));
} | } |
TOK_COVER '(' expr ')' ';' { TOK_COVER opt_property '(' expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(AST_COVER, $3)); ast_stack.back()->children.push_back(new AstNode(AST_COVER, $4));
} | } |
TOK_COVER '(' ')' ';' { TOK_COVER opt_property '(' ')' ';' {
ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false))); ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
} | } |
TOK_COVER ';' { TOK_COVER ';' {
ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false))); ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
} | } |
TOK_RESTRICT '(' expr ')' ';' { TOK_RESTRICT opt_property '(' expr ')' ';' {
if (norestrict_mode)
delete $3;
else
ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3));
} |
TOK_RESTRICT '(' TOK_EVENTUALLY expr ')' ';' {
if (norestrict_mode) if (norestrict_mode)
delete $4; delete $4;
else else
ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $4)); ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
} |
TOK_RESTRICT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
if (norestrict_mode)
delete $5;
else
ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $5));
}; };
assert_property: assert_property: