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.

Author: MatWise

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$

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;

regression/statement-list/Add_Int2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Add_Int2\"
+
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/statement-list/Arithmetic/main.awl

@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Arithmetic"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_TEMP 
       compResult : Bool;

regression/statement-list/Arithmetic/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Arithmetic\"
+
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

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$

regression/statement-list/Bool2/main.awl

@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Bool2"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_INPUT 
       in1 : Bool;

regression/statement-list/Bool2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Bool2\"
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^SAT checker: instance is SATISFIABLE$

regression/statement-list/Bool3/main.awl

@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Bool3"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_INPUT 
       in1 : Bool;

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\)$

regression/statement-list/Bool4/main.awl

@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Bool4"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_TEMP 
       temp1 : Bool;

regression/statement-list/Bool4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Bool4\"
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/statement-list/Bool5/main.awl

@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Bool5"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_INPUT 
       in1 : Bool;

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\)$

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$

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

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$

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$

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

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;

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$

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$

src/statement-list/scanner.l

@@ -21,6 +21,8 @@
 #include <util/pragma_wnull_conversion.def>
 #include <util/pragma_wdeprecated_register.def>
 
+#include <algorithm>
+
 // 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; }
 }
+
+<MODULE_NAME>{
+  [\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; 
+                      }
+}
+
 <TAG_ATTRIBUTES>{
   [\t\r," ]           ;
   ([t|T][R|r][u|U][e|E])|([f|F][a|A][l|L][s|S][e|E]) ;

src/statement-list/statement_list_typecheck.cpp

@@ -30,9 +30,9 @@ Author: Matthias Weiss, [email protected]
 /// 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"
 

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)