Merge pull request #4955 from MatWise/feature/stl-module-name
STL frontend: Cut quotes from module names
This commit is contained in:
commit
7b23476525
|
@ -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$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
FUNCTION_BLOCK "Add_Int2"
|
||||
FUNCTION_BLOCK "Main"
|
||||
VERSION : 0.1
|
||||
VAR_INPUT
|
||||
in1 : Int;
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
CORE
|
||||
main.awl
|
||||
--function \"Add_Int2\"
|
||||
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
FUNCTION_BLOCK "Arithmetic"
|
||||
FUNCTION_BLOCK "Main"
|
||||
VERSION : 0.1
|
||||
VAR_TEMP
|
||||
compResult : Bool;
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
CORE
|
||||
main.awl
|
||||
--function \"Arithmetic\"
|
||||
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
|
|
|
@ -3,7 +3,7 @@ main.awl
|
|||
--show-parse-tree
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^Name: "Bool1"$
|
||||
^Name: Bool1$
|
||||
^Version: 0[.]1$
|
||||
^ \* type: bool$
|
||||
^ \* identifier: in1$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
FUNCTION_BLOCK "Bool2"
|
||||
FUNCTION_BLOCK "Main"
|
||||
VERSION : 0.1
|
||||
VAR_INPUT
|
||||
in1 : Bool;
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
CORE
|
||||
main.awl
|
||||
--function \"Bool2\"
|
||||
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^SAT checker: instance is SATISFIABLE$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
FUNCTION_BLOCK "Bool3"
|
||||
FUNCTION_BLOCK "Main"
|
||||
VERSION : 0.1
|
||||
VAR_INPUT
|
||||
in1 : Bool;
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
CORE
|
||||
main.awl
|
||||
--function \"Bool3\"
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 0 of 1 failed \(1 iterations\)$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
FUNCTION_BLOCK "Bool4"
|
||||
FUNCTION_BLOCK "Main"
|
||||
VERSION : 0.1
|
||||
VAR_TEMP
|
||||
temp1 : Bool;
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
CORE
|
||||
main.awl
|
||||
--function \"Bool4\"
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
FUNCTION_BLOCK "Bool5"
|
||||
FUNCTION_BLOCK "Main"
|
||||
VERSION : 0.1
|
||||
VAR_INPUT
|
||||
in1 : Bool;
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
CORE
|
||||
main.awl
|
||||
--function \"Bool5\"
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 0 of 1 failed \(1 iterations\)$
|
||||
|
|
|
@ -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$
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
CORE
|
||||
main.awl
|
||||
--function \"Function_Call2\"
|
||||
--function Function_Call2
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
|
|
|
@ -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$
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
FUNCTION_BLOCK "Sub_DInt"
|
||||
FUNCTION_BLOCK "Main"
|
||||
VERSION : 0.1
|
||||
VAR_INPUT
|
||||
in1 : DInt;
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
CORE
|
||||
main.awl
|
||||
--function \"Sub_DInt\"
|
||||
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^SAT checker: instance is SATISFIABLE$
|
||||
|
|
|
@ -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$
|
||||
|
|
|
@ -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]) ;
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -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)
|
||||
|
|
Loading…
Reference in New Issue