From 5a775c15c2e64e7639ef7611d4c64a6fda779bdd Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Sun, 5 Jun 2016 21:10:21 +0200
Subject: [PATCH] Fix consistency error in SSA level 1 renaming

a5bc493713 introduced cases where information in the frame may become
inconsistent with the actual renaming being used, as shown in the regression
test.
---
 regression/cbmc/Local_out_of_scope2/main.c    | 25 +++++++++++++++++++
 regression/cbmc/Local_out_of_scope2/test.desc |  8 ++++++
 src/goto-symex/symex_function_call.cpp        |  2 +-
 3 files changed, 34 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/Local_out_of_scope2/main.c
 create mode 100644 regression/cbmc/Local_out_of_scope2/test.desc

diff --git a/regression/cbmc/Local_out_of_scope2/main.c b/regression/cbmc/Local_out_of_scope2/main.c
new file mode 100644
index 0000000000..0794c634c5
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope2/main.c
@@ -0,0 +1,25 @@
+inline void foo(int x)
+{
+}
+
+void bar()
+{
+  foo(0);
+}
+
+void foobar()
+{
+  // different argument values must not cause an inconsistency in the
+  // equation system
+  foo(0);
+  bar();
+  foo(1);
+}
+
+int main()
+{
+  foobar();
+  foobar();
+  __CPROVER_assert(0, "");
+  return 0;
+}
diff --git a/regression/cbmc/Local_out_of_scope2/test.desc b/regression/cbmc/Local_out_of_scope2/test.desc
new file mode 100644
index 0000000000..6de7955991
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index cb16ffc7b1..869a919380 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -501,9 +501,9 @@ void goto_symext::locality(
     while(state.l1_history.find(l1_name)!=state.l1_history.end())
     {
       state.level1.increase_counter(l0_name);
+      ++offset;
       ssa.set_level_1(frame_nr+offset);
       l1_name=ssa.get_identifier();
-      ++offset;
     }
     
     // now unique -- store