Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
divine-ltsmin-deb
Commits
c5804869
Commit
c5804869
authored
Aug 07, 2010
by
Elwin Pater
Committed by
Michael Weber
Nov 05, 2010
Browse files
Added co-enabled detection for const array index
parent
fe632e5f
Changes
2
Hide whitespace changes
Inline
Side-by-side
tools/dvecompile.cpp
View file @
c5804869
...
...
@@ -2398,6 +2398,38 @@ bool dve_compiler::get_const_expression( dve_expression_t & expr, int & value)
return
false
;
}
bool
dve_compiler
::
get_const_varname
(
dve_expression_t
&
expr
,
string
&
var
)
{
string
var_square_bracket
;
dve_symbol_table_t
*
parent_table
=
expr
.
get_symbol_table
();
if
(
!
parent_table
)
gerr
<<
"Get const var: Symbol table not set"
<<
thr
();
switch
(
expr
.
get_operator
())
{
case
T_SQUARE_BRACKETS
:
int
val
;
if
(
get_const_expression
(
*
expr
.
left
(),
val
))
{
var_square_bracket
=
"["
+
fmt
(
val
)
+
"]"
;
}
else
{
return
false
;
}
// fall through
case
T_ID
:
{
string
proc_part
(
""
);
string
var_part
(
parent_table
->
get_variable
(
expr
.
get_ident_gid
())
->
get_name
());
if
(
parent_table
->
get_variable
(
expr
.
get_ident_gid
())
->
get_process_gid
()
!=
NO_ID
)
{
proc_part
=
parent_table
->
get_process
(
parent_table
->
get_variable
(
expr
.
get_ident_gid
())
->
get_process_gid
())
->
get_name
();
proc_part
+=
"."
;
}
var
=
proc_part
+
var_part
+
var_square_bracket
;
}
return
true
;
default:
var
=
""
;
}
return
false
;
}
void
dve_compiler
::
extract_predicates
(
std
::
vector
<
simple_predicate
>&
p
,
dve_expression_t
&
expr
)
{
dve_symbol_table_t
*
parent_table
=
expr
.
get_symbol_table
();
...
...
@@ -2406,18 +2438,10 @@ void dve_compiler::extract_predicates( std::vector<simple_predicate>& p, dve_exp
{
case
T_PARENTHESIS
:
return
extract_predicates
(
p
,
*
expr
.
left
());
case
T_LT
:
case
T_LEQ
:
case
T_EQ
:
case
T_NEQ
:
case
T_GT
:
case
T_GEQ
:
if
((
*
expr
.
left
()).
get_operator
()
==
T_ID
)
{
simple_predicate
sp
;
case
T_LT
:
case
T_LEQ
:
case
T_EQ
:
case
T_NEQ
:
case
T_GT
:
case
T_GEQ
:
{
simple_predicate
sp
;
if
(
get_const_varname
(
*
expr
.
left
(),
sp
.
variable_name
))
{
if
(
get_const_expression
(
*
expr
.
right
(),
sp
.
variable_value
)
)
{
string
proc_part
(
""
);
string
var_part
(
parent_table
->
get_variable
((
expr
.
left
())
->
get_ident_gid
())
->
get_name
());
if
(
parent_table
->
get_variable
(
expr
.
get_ident_gid
())
->
get_process_gid
()
!=
NO_ID
)
{
proc_part
=
parent_table
->
get_process
(
parent_table
->
get_variable
(
expr
.
get_ident_gid
())
->
get_process_gid
())
->
get_name
();
proc_part
+=
"."
;
}
sp
.
variable_name
=
proc_part
+
var_part
;
switch
(
expr
.
get_operator
())
{
case
T_LT
:
sp
.
relation
=
PRED_LT
;
break
;
case
T_LEQ
:
sp
.
relation
=
PRED_LEQ
;
break
;
...
...
@@ -2429,7 +2453,7 @@ void dve_compiler::extract_predicates( std::vector<simple_predicate>& p, dve_exp
p
.
push_back
(
sp
);
}
}
break
;
}
break
;
case
T_BOOL_AND
:
{
extract_predicates
(
p
,
*
expr
.
left
());
...
...
tools/dvecompile.h
View file @
c5804869
...
...
@@ -230,6 +230,7 @@ struct dve_compiler: public dve_explicit_system_t
bool
split_conjunctive_expression
(
std
::
vector
<
guard
>&
guard
,
dve_expression_t
*
expr
);
void
merge_dependent_expression
(
std
::
vector
<
guard
>&
guard
,
int
sv_count
);
void
gen_transition_info
();
bool
get_const_varname
(
dve_expression_t
&
expr
,
string
&
var
);
bool
get_const_expression
(
dve_expression_t
&
expr
,
int
&
value
);
bool
is_guard_nes
(
guard
&
g
,
ext_transition_t
&
t
);
bool
may_be_coenabled
(
guard
&
ga
,
guard
&
gb
);
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment