Merge pull request #757 from forejtv/bugfix/master-fixes

Fix broken master

Author: Daniel Kroening

regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc

@@ -3,9 +3,9 @@ main.c
 --show-goto-functions --verbosity 10 --pointer-check
 
 ^Removing function pointers and virtual functions$
-^\s*IF fp == \(void \(\*\)\(void\)\)f2 THEN GOTO [0-9]$
-^\s*IF fp == \(void \(\*\)\(void\)\)f3 THEN GOTO [0-9]$
-^\s*IF fp == \(void \(\*\)\(void\)\)f4 THEN GOTO [0-9]$
+^\s*IF fp == \(const void_fp\)f2 THEN GOTO [0-9]$
+^\s*IF fp == \(const void_fp\)f3 THEN GOTO [0-9]$
+^\s*IF fp == \(const void_fp\)f4 THEN GOTO [0-9]$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/cbmc/symex_bmc.cpp

@@ -88,7 +88,7 @@ void symex_bmct::symex_step(
      !state.guard.is_false() &&
      // avoid an invalid iterator in state.source.pc
      (!cur_pc->is_end_function() ||
-      cur_pc->function!=ID__start) &&
+      cur_pc->function!=goto_functions.entry_point()) &&
      // ignore transition to next instruction when goto points elsewhere
      (!cur_pc->is_goto() ||
       cur_pc->get_target()==state.source.pc ||