hash_set_cont iterators aren't stable

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4363 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2014-07-28 15:03:24 +00:00
parent aedbc7bc1b
commit 184e399a05
3 changed files with 37 additions and 4 deletions

View File

@ -0,0 +1,26 @@
#include <assert.h>
union U
{
short a;
int b;
char c[4];
};
int main()
{
if(sizeof(short)!=2 ||
sizeof(int)!=4)
return 0;
union U u;
u.b=0x04030201;
assert(u.a==0x0403);
assert(u.c[0]==0x04);
assert(u.c[1]==0x03);
assert(u.c[2]==0x02);
assert(u.c[3]==0x01);
return 0;
}

View File

@ -0,0 +1,8 @@
CORE
main.c
--big-endian
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring

View File

@ -300,7 +300,7 @@ void goto_inlinet::expand_function_call(
"but got `"+function.id_string()+"'";
}
const irep_idt &identifier=function.get(ID_identifier);
const irep_idt identifier=function.get(ID_identifier);
// see if we are already expanding it
if(recursion_set.find(identifier)!=recursion_set.end())
@ -353,8 +353,7 @@ void goto_inlinet::expand_function_call(
if(f.body_available)
{
recursion_sett::iterator recursion_it=
recursion_set.insert(identifier).first;
recursion_set.insert(identifier);
// first make sure that this one is already inlined
goto_inline_rec(m_it, full);
@ -398,7 +397,7 @@ void goto_inlinet::expand_function_call(
dest.instructions.splice(next_target, tmp.instructions);
target=next_target;
recursion_set.erase(recursion_it);
recursion_set.erase(identifier);
}
else // no body available
{