From e53a82b00def8e26be5274917af91a65ab270108 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 19 Jan 2019 16:25:58 +0000
Subject: [PATCH] Set a property id for recursion unwinding assertions

Previously we displayed an empty id.
---
 regression/cbmc/unwinding_assertions1/main.c    | 9 +++++++++
 regression/cbmc/unwinding_assertions1/test.desc | 8 ++++++++
 src/goto-symex/symex_target_equation.cpp        | 6 ++++++
 3 files changed, 23 insertions(+)
 create mode 100644 regression/cbmc/unwinding_assertions1/main.c
 create mode 100644 regression/cbmc/unwinding_assertions1/test.desc

diff --git a/regression/cbmc/unwinding_assertions1/main.c b/regression/cbmc/unwinding_assertions1/main.c
new file mode 100644
index 0000000000..14db6eba80
--- /dev/null
+++ b/regression/cbmc/unwinding_assertions1/main.c
@@ -0,0 +1,9 @@
+void foo()
+{
+  foo();
+}
+
+int main()
+{
+  foo();
+}
diff --git a/regression/cbmc/unwinding_assertions1/test.desc b/regression/cbmc/unwinding_assertions1/test.desc
new file mode 100644
index 0000000000..33d9d83a07
--- /dev/null
+++ b/regression/cbmc/unwinding_assertions1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 3 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[foo.recursion\]
+--
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 90ad0e9017..5387ec6460 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -988,6 +988,12 @@ irep_idt symex_target_equationt::SSA_stept::get_property_id() const
     property_id = id2string(source.pc->source_location.get_function()) +
                   ".unwind." + std::to_string(source.pc->loop_number);
   }
+  else if(source.pc->is_function_call())
+  {
+    // this is likely a recursion unwinding assertion
+    property_id =
+      id2string(source.pc->source_location.get_function()) + ".recursion";
+  }
   else
   {
     // return empty