From 9130d6f58c1c364a4804b5024322d2b6f5ab4584 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Nov 2011 11:59:45 +0100 Subject: [PATCH] Allow neverclaim guards of the form `!(x)' or `! (x)'. * src/neverparse/neverclaimscan.ll: Make the space between `!' and `(' optional. This fixes the patch from 2011-02-07 that made this space mandatory... * src/tgbatest/neverclaimread.test: Augment test case. --- ChangeLog | 9 +++++++++ src/neverparse/neverclaimscan.ll | 2 +- src/tgbatest/neverclaimread.test | 4 ++-- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/ChangeLog b/ChangeLog index d5067afa1..f9aa34cd9 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2011-11-08 Alexandre Duret-Lutz + + Allow neverclaim guards of the form `!(x)' or `! (x)'. + + * src/neverparse/neverclaimscan.ll: Make the space between `!' and + `(' optional. This fixes the patch from 2011-02-07 that made this + space mandatory... + * src/tgbatest/neverclaimread.test: Augment test case. + 2011-10-26 Alexandre Duret-Lutz Better documentation for print_tgba_run. diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll index 9d4e95af4..0ca759eed 100644 --- a/src/neverparse/neverclaimscan.ll +++ b/src/neverparse/neverclaimscan.ll @@ -56,7 +56,7 @@ eol \n|\r|\n\r|\r\n "goto" return token::GOTO; "false"|"0" return token::FALSE; -("!"[ \t]+)?"(".*")"|"true"|"1" { +("!"[ \t]*)?"(".*")"|"true"|"1" { yylval->str = new std::string(yytext, yyleng); return token::FORMULA; } diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index fcdd807d5..9de8eae35 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -34,7 +34,7 @@ fi; T1: if :: (p1 && (! p0)) -> goto accept_all -:: (p1) -> goto T1 +:: !(p1) -> goto T1 :: ! (p1) -> goto T2_init fi; accept_all: @@ -53,7 +53,7 @@ digraph G { 1 -> 2 [label="p0 & p1\n"] 2 [label="T1"] 2 -> 3 [label="p1 & !p0\n"] - 2 -> 2 [label="p1\n"] + 2 -> 2 [label="!p1\n"] 2 -> 1 [label="!p1\n"] 3 [label="accept_all"] 3 -> 3 [label="1\n{Acc[1]}"]