replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

mild strengthening of typing of array and vector constructors 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3412 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2014-01-11 15:45:29 +00:00
parent 9b15f5a3ab
commit 5609f6183f
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/linking/zero_initializer.cpp
View File

@ -110,7 +110,7 @@ exprt zero_initializert::zero_initializer_rec(
{
// we initialize this with an empty array
array_exprt value(type);
array_exprt value(array_type);
value.type().id(ID_array);
value.type().set(ID_size, gen_zero(size_type()));
value.location()=location;
@ -145,7 +145,7 @@ exprt zero_initializert::zero_initializer_rec(
throw 0;
}
array_exprt value(type);
array_exprt value(array_type);
value.operands().resize(integer2long(array_size), tmpval);
value.location()=location;
return value;

4
src/util/std_expr.h
View File

@ -915,7 +915,7 @@ public:
{
}
explicit inline array_exprt(const typet &_type):
explicit inline array_exprt(const array_typet &_type):
exprt(ID_array, _type)
{
}
@ -958,7 +958,7 @@ public:
{
}
explicit inline vector_exprt(const typet &_type):
explicit inline vector_exprt(const vector_typet &_type):
exprt(ID_vector, _type)
{
}