From 053eab050404ec6e19fa6ae5159facf7cea239ab Mon Sep 17 00:00:00 2001 From: Matthias Weiss Date: Fri, 26 Jul 2019 17:45:43 +0100 Subject: [PATCH] Remove quotes around STL module names This commit introduces an extra state to the STL scanner in order to detect if the current identifier is a module name. If it is, the surrounding quotes are cut. The quotes are syntactically required but do not contribute to the module names being unique, therefore cutting them is allowed. Doing so simplifies both the user and the language interface. Existing regression tests were changed in a way that all directly refer to the default entry point which was introduced by a past commit. One test, Function_Call2, is now responsible for checking the --function flag. --- regression/statement-list/Add_Int/test.desc | 2 +- regression/statement-list/Add_Int2/main.awl | 2 +- regression/statement-list/Add_Int2/test.desc | 2 +- regression/statement-list/Arithmetic/main.awl | 2 +- .../statement-list/Arithmetic/test.desc | 2 +- regression/statement-list/Bool1/test.desc | 2 +- regression/statement-list/Bool2/main.awl | 2 +- regression/statement-list/Bool2/test.desc | 2 +- regression/statement-list/Bool3/main.awl | 2 +- regression/statement-list/Bool3/test.desc | 2 +- regression/statement-list/Bool4/main.awl | 2 +- regression/statement-list/Bool4/test.desc | 2 +- regression/statement-list/Bool5/main.awl | 2 +- regression/statement-list/Bool5/test.desc | 2 +- regression/statement-list/Div_Real/test.desc | 2 +- .../statement-list/Function_Call1/test.desc | 4 +-- .../statement-list/Function_Call2/test.desc | 2 +- regression/statement-list/Mul_DInt/test.desc | 2 +- .../Multiple_Elements/test.desc | 6 ++--- regression/statement-list/Sub_DInt/main.awl | 2 +- regression/statement-list/Sub_DInt/test.desc | 2 +- .../statement-list/Var_Declaration/test.desc | 4 +-- src/statement-list/scanner.l | 27 ++++++++++++++++--- .../statement_list_typecheck.cpp | 4 +-- src/util/irep_ids.def | 2 +- 25 files changed, 53 insertions(+), 32 deletions(-) diff --git a/regression/statement-list/Add_Int/test.desc b/regression/statement-list/Add_Int/test.desc index a4385da427..afa12c0687 100644 --- a/regression/statement-list/Add_Int/test.desc +++ b/regression/statement-list/Add_Int/test.desc @@ -3,7 +3,7 @@ main.awl --show-parse-tree ^EXIT=0$ ^SIGNAL=0$ -^Name: "Add_Int"$ +^Name: Add_Int$ ^Version: 0[.]1$ ^ \* type: signedbv$ ^ \* width: 16$ diff --git a/regression/statement-list/Add_Int2/main.awl b/regression/statement-list/Add_Int2/main.awl index 80a6f4704f..d3f928bf23 100644 --- a/regression/statement-list/Add_Int2/main.awl +++ b/regression/statement-list/Add_Int2/main.awl @@ -1,4 +1,4 @@ -FUNCTION_BLOCK "Add_Int2" +FUNCTION_BLOCK "Main" VERSION : 0.1 VAR_INPUT in1 : Int; diff --git a/regression/statement-list/Add_Int2/test.desc b/regression/statement-list/Add_Int2/test.desc index bbf4830a91..13d2530c81 100644 --- a/regression/statement-list/Add_Int2/test.desc +++ b/regression/statement-list/Add_Int2/test.desc @@ -1,6 +1,6 @@ CORE main.awl ---function \"Add_Int2\" + ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/statement-list/Arithmetic/main.awl b/regression/statement-list/Arithmetic/main.awl index 2aa832d14b..bffa90c0d2 100644 --- a/regression/statement-list/Arithmetic/main.awl +++ b/regression/statement-list/Arithmetic/main.awl @@ -1,4 +1,4 @@ -FUNCTION_BLOCK "Arithmetic" +FUNCTION_BLOCK "Main" VERSION : 0.1 VAR_TEMP compResult : Bool; diff --git a/regression/statement-list/Arithmetic/test.desc b/regression/statement-list/Arithmetic/test.desc index 60576b9bbf..13d2530c81 100644 --- a/regression/statement-list/Arithmetic/test.desc +++ b/regression/statement-list/Arithmetic/test.desc @@ -1,6 +1,6 @@ CORE main.awl ---function \"Arithmetic\" + ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/statement-list/Bool1/test.desc b/regression/statement-list/Bool1/test.desc index 6caf68dd16..e0528e08d3 100644 --- a/regression/statement-list/Bool1/test.desc +++ b/regression/statement-list/Bool1/test.desc @@ -3,7 +3,7 @@ main.awl --show-parse-tree ^EXIT=0$ ^SIGNAL=0$ -^Name: "Bool1"$ +^Name: Bool1$ ^Version: 0[.]1$ ^ \* type: bool$ ^ \* identifier: in1$ diff --git a/regression/statement-list/Bool2/main.awl b/regression/statement-list/Bool2/main.awl index 1e2c013ac3..63c354259b 100644 --- a/regression/statement-list/Bool2/main.awl +++ b/regression/statement-list/Bool2/main.awl @@ -1,4 +1,4 @@ -FUNCTION_BLOCK "Bool2" +FUNCTION_BLOCK "Main" VERSION : 0.1 VAR_INPUT in1 : Bool; diff --git a/regression/statement-list/Bool2/test.desc b/regression/statement-list/Bool2/test.desc index 5e21dd6bb9..48435b6da5 100644 --- a/regression/statement-list/Bool2/test.desc +++ b/regression/statement-list/Bool2/test.desc @@ -1,6 +1,6 @@ CORE main.awl ---function \"Bool2\" + ^EXIT=10$ ^SIGNAL=0$ ^SAT checker: instance is SATISFIABLE$ diff --git a/regression/statement-list/Bool3/main.awl b/regression/statement-list/Bool3/main.awl index 1d0120cbe6..dc1a0f47c3 100644 --- a/regression/statement-list/Bool3/main.awl +++ b/regression/statement-list/Bool3/main.awl @@ -1,4 +1,4 @@ -FUNCTION_BLOCK "Bool3" +FUNCTION_BLOCK "Main" VERSION : 0.1 VAR_INPUT in1 : Bool; diff --git a/regression/statement-list/Bool3/test.desc b/regression/statement-list/Bool3/test.desc index b6c9799ef8..f6ef8634b0 100644 --- a/regression/statement-list/Bool3/test.desc +++ b/regression/statement-list/Bool3/test.desc @@ -1,6 +1,6 @@ CORE main.awl ---function \"Bool3\" + ^EXIT=0$ ^SIGNAL=0$ ^\*\* 0 of 1 failed \(1 iterations\)$ diff --git a/regression/statement-list/Bool4/main.awl b/regression/statement-list/Bool4/main.awl index 8e31722833..6b37525d85 100644 --- a/regression/statement-list/Bool4/main.awl +++ b/regression/statement-list/Bool4/main.awl @@ -1,4 +1,4 @@ -FUNCTION_BLOCK "Bool4" +FUNCTION_BLOCK "Main" VERSION : 0.1 VAR_TEMP temp1 : Bool; diff --git a/regression/statement-list/Bool4/test.desc b/regression/statement-list/Bool4/test.desc index 3de6d88bfb..b67aeca7c1 100644 --- a/regression/statement-list/Bool4/test.desc +++ b/regression/statement-list/Bool4/test.desc @@ -1,6 +1,6 @@ CORE main.awl ---function \"Bool4\" + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/statement-list/Bool5/main.awl b/regression/statement-list/Bool5/main.awl index 5dbf7784a1..346b4f4531 100644 --- a/regression/statement-list/Bool5/main.awl +++ b/regression/statement-list/Bool5/main.awl @@ -1,4 +1,4 @@ -FUNCTION_BLOCK "Bool5" +FUNCTION_BLOCK "Main" VERSION : 0.1 VAR_INPUT in1 : Bool; diff --git a/regression/statement-list/Bool5/test.desc b/regression/statement-list/Bool5/test.desc index 5ac3565925..f6ef8634b0 100644 --- a/regression/statement-list/Bool5/test.desc +++ b/regression/statement-list/Bool5/test.desc @@ -1,6 +1,6 @@ CORE main.awl ---function \"Bool5\" + ^EXIT=0$ ^SIGNAL=0$ ^\*\* 0 of 1 failed \(1 iterations\)$ diff --git a/regression/statement-list/Div_Real/test.desc b/regression/statement-list/Div_Real/test.desc index eea28dcc9f..fb04e55fe7 100644 --- a/regression/statement-list/Div_Real/test.desc +++ b/regression/statement-list/Div_Real/test.desc @@ -3,7 +3,7 @@ main.awl --show-parse-tree ^EXIT=0$ ^SIGNAL=0$ -^Name: "Div_Real"$ +^Name: Div_Real$ ^Version: 0[.]1$ ^ \* type: floatbv$ ^ \* width: 32$ diff --git a/regression/statement-list/Function_Call1/test.desc b/regression/statement-list/Function_Call1/test.desc index 05b229262a..3fe4a9c113 100644 --- a/regression/statement-list/Function_Call1/test.desc +++ b/regression/statement-list/Function_Call1/test.desc @@ -3,9 +3,9 @@ main.awl --show-parse-tree ^EXIT=0$ ^SIGNAL=0$ -^Name: "Function_Call1"$ +^Name: Function_Call1$ ^Version: 0[.]1$ -^statement_list_call "__Function"$ +^statement_list_call __Function$ ^ param := In1$ -- ^warning: ignoring diff --git a/regression/statement-list/Function_Call2/test.desc b/regression/statement-list/Function_Call2/test.desc index 9afe8d2a1a..d57c7589ea 100644 --- a/regression/statement-list/Function_Call2/test.desc +++ b/regression/statement-list/Function_Call2/test.desc @@ -1,6 +1,6 @@ CORE main.awl ---function \"Function_Call2\" +--function Function_Call2 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/statement-list/Mul_DInt/test.desc b/regression/statement-list/Mul_DInt/test.desc index 76649cd093..2b6b2dce0a 100644 --- a/regression/statement-list/Mul_DInt/test.desc +++ b/regression/statement-list/Mul_DInt/test.desc @@ -3,7 +3,7 @@ main.awl --show-parse-tree ^EXIT=0$ ^SIGNAL=0$ -^Name: "Mul_DInt"$ +^Name: Mul_DInt$ ^Version: 0[.]1$ ^ \* type: signedbv$ ^ \* width: 32$ diff --git a/regression/statement-list/Multiple_Elements/test.desc b/regression/statement-list/Multiple_Elements/test.desc index de72c04c52..3aa343eea3 100644 --- a/regression/statement-list/Multiple_Elements/test.desc +++ b/regression/statement-list/Multiple_Elements/test.desc @@ -3,8 +3,8 @@ main.awl --show-parse-tree ^EXIT=0$ ^SIGNAL=0$ -^Name: "Mult_1"$ -^Name: "Mult_2"$ -^Name: "Mult_3"$ +^Name: Mult_1$ +^Name: Mult_2$ +^Name: Mult_3$ -- ^warning: ignoring diff --git a/regression/statement-list/Sub_DInt/main.awl b/regression/statement-list/Sub_DInt/main.awl index cc93f926e4..dfcc720fed 100644 --- a/regression/statement-list/Sub_DInt/main.awl +++ b/regression/statement-list/Sub_DInt/main.awl @@ -1,4 +1,4 @@ -FUNCTION_BLOCK "Sub_DInt" +FUNCTION_BLOCK "Main" VERSION : 0.1 VAR_INPUT in1 : DInt; diff --git a/regression/statement-list/Sub_DInt/test.desc b/regression/statement-list/Sub_DInt/test.desc index 13fae12157..48435b6da5 100644 --- a/regression/statement-list/Sub_DInt/test.desc +++ b/regression/statement-list/Sub_DInt/test.desc @@ -1,6 +1,6 @@ CORE main.awl ---function \"Sub_DInt\" + ^EXIT=10$ ^SIGNAL=0$ ^SAT checker: instance is SATISFIABLE$ diff --git a/regression/statement-list/Var_Declaration/test.desc b/regression/statement-list/Var_Declaration/test.desc index 937379af61..942893abe4 100644 --- a/regression/statement-list/Var_Declaration/test.desc +++ b/regression/statement-list/Var_Declaration/test.desc @@ -3,8 +3,8 @@ main.awl --show-parse-tree ^EXIT=0$ ^SIGNAL=0$ -^Name: "Var_assign_FB"$ -^Name: "Var_assign_FC"$ +^Name: Var_assign_FB$ +^Name: Var_assign_FC$ ^Version: 0[.]1$ ^ \* type: bool$ ^ \* type: floatbv$ diff --git a/src/statement-list/scanner.l b/src/statement-list/scanner.l index 892942eff3..6ede333edc 100644 --- a/src/statement-list/scanner.l +++ b/src/statement-list/scanner.l @@ -21,6 +21,8 @@ #include #include +#include + // Visual Studio #if defined _MSC_VER // Disable warning for signed/unsigned mismatch. @@ -75,6 +77,7 @@ void statement_list_scanner_init() %x GRAMMAR %x TAG_NAME +%x MODULE_NAME %x TAG_ATTRIBUTES %x VERSION_ANNOTATION @@ -90,9 +93,9 @@ void statement_list_scanner_init() TAG { loc(); BEGIN(TAG_NAME); return TOK_TAG; } BEGIN { loc(); return TOK_BEGIN; } VERSION { loc(); BEGIN(VERSION_ANNOTATION); return TOK_VERSION; } - FUNCTION_BLOCK { loc(); return TOK_FUNCTION_BLOCK; } + FUNCTION_BLOCK { loc(); BEGIN(MODULE_NAME); return TOK_FUNCTION_BLOCK; } END_FUNCTION_BLOCK { loc(); return TOK_END_FUNCTION_BLOCK; } - FUNCTION { loc(); return TOK_FUNCTION; } + FUNCTION { loc(); BEGIN(MODULE_NAME); return TOK_FUNCTION; } END_FUNCTION { loc(); return TOK_END_FUNCTION; } VAR_INPUT { loc(); return TOK_VAR_INPUT; } VAR_OUTPUT { loc(); return TOK_VAR_OUTPUT; } @@ -110,7 +113,7 @@ void statement_list_scanner_init() Void { loc(); return TOK_VOID; } L { loc(); return TOK_LOAD; } T { loc(); return TOK_TRANSFER; } - CALL { loc(); return TOK_CALL; } + CALL { loc(); BEGIN(MODULE_NAME); return TOK_CALL; } NOP { loc(); return TOK_NOP; } SET { loc(); return TOK_SET_RLO; } CLR { loc(); return TOK_CLR_RLO; } @@ -292,6 +295,24 @@ void statement_list_scanner_init() } END_TAG { loc(); BEGIN(GRAMMAR); return TOK_END_TAG; } } + +{ + [\t\r\n ] ; + \"[^\"\r\t\n]+\" { + newstack(yystatement_listlval); + std::string str{yytext}; + str.erase( + std::remove(begin(str), end(str), '\"' ), + end(str)); + parser_stack(yystatement_listlval) = + convert_identifier(str); + PARSER.set_source_location( + parser_stack(yystatement_listlval)); + BEGIN(GRAMMAR); + return TOK_IDENTIFIER; + } +} + { [\t\r," ] ; ([t|T][R|r][u|U][e|E])|([f|F][a|A][l|L][s|S][e|E]) ; diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp index 13380f934e..afde15561b 100644 --- a/src/statement-list/statement_list_typecheck.cpp +++ b/src/statement-list/statement_list_typecheck.cpp @@ -30,9 +30,9 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com /// Postfix for the type of a data block. #define DATA_BLOCK_TYPE_POSTFIX "_db" /// Name of the CBMC assert function. -#define CPROVER_ASSERT "\"" CPROVER_PREFIX "assert\"" +#define CPROVER_ASSERT CPROVER_PREFIX "assert" /// Name of the CBMC assume function. -#define CPROVER_ASSUME "\"" CPROVER_PREFIX "assume\"" +#define CPROVER_ASSUME CPROVER_PREFIX "assume" /// Name of the RLO symbol used in some operations. #define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo" diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 4b5b4b92a7..ef2676574d 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -766,7 +766,7 @@ IREP_ID_TWO(statement_list, Statement List) IREP_ID_ONE(statement_list_type) IREP_ID_ONE(statement_list_function) IREP_ID_ONE(statement_list_function_block) -IREP_ID_TWO(statement_list_main_function, "Main") +IREP_ID_TWO(statement_list_main_function, Main) IREP_ID_ONE(statement_list_data_block) IREP_ID_ONE(statement_list_version) IREP_ID_ONE(statement_list_var_input)