Merge pull request #4955 from MatWise/feature/stl-module-name

pkesseli · web-flow · commit 7b234765259e · 2019-07-31T19:39:51.000+02:00
STL frontend: Cut quotes from module names
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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]) ;
diff --git 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
@@ -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)

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-FUNCTION_BLOCK "Add_Int2"`
	`1`	`+FUNCTION_BLOCK "Main"`
`2`	`2`	`VERSION : 0.1`
`3`	`3`	`VAR_INPUT`
`4`	`4`	`in1 : Int;`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-FUNCTION_BLOCK "Arithmetic"`
	`1`	`+FUNCTION_BLOCK "Main"`
`2`	`2`	`VERSION : 0.1`
`3`	`3`	`VAR_TEMP`
`4`	`4`	`compResult : Bool;`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-FUNCTION_BLOCK "Bool2"`
	`1`	`+FUNCTION_BLOCK "Main"`
`2`	`2`	`VERSION : 0.1`
`3`	`3`	`VAR_INPUT`
`4`	`4`	`in1 : Bool;`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-FUNCTION_BLOCK "Bool3"`
	`1`	`+FUNCTION_BLOCK "Main"`
`2`	`2`	`VERSION : 0.1`
`3`	`3`	`VAR_INPUT`
`4`	`4`	`in1 : Bool;`