diff --git a/regression/cbmc/Endianness8/main.c b/regression/cbmc/Endianness8/main.c new file mode 100644 index 0000000000..c31b2afcc2 --- /dev/null +++ b/regression/cbmc/Endianness8/main.c @@ -0,0 +1,26 @@ +#include + +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; +} diff --git a/regression/cbmc/Endianness8/test.desc b/regression/cbmc/Endianness8/test.desc new file mode 100644 index 0000000000..81ceb4c6dc --- /dev/null +++ b/regression/cbmc/Endianness8/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--big-endian +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 0d1c08146f..d0453b97c1 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -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 {