Make get_failed_symbol return optional symbol_exprt

This is more precise on the type of object returned.

Author: romainbrenguier

src/goto-symex/symex_dead.cpp

@@ -32,14 +32,11 @@ void goto_symext::symex_dead(statet &state)
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)
   {
-    exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns);
-
-    exprt rhs;
-
-    if(failed.is_not_nil())
-      rhs = address_of_exprt(failed, to_pointer_type(code.symbol().type()));
-    else
-      rhs=exprt(ID_invalid);
+    exprt rhs = [&]() -> exprt {
+      if(auto failed = get_failed_symbol(code.symbol(), ns))
+        return address_of_exprt(*failed, to_pointer_type(code.symbol().type()));
+      return exprt(ID_invalid);
+    }();
 
     state.rename(rhs, ns, goto_symex_statet::L1);
     state.value_set.assign(ssa, rhs, ns, true, false);

src/goto-symex/symex_decl.cpp

@@ -48,15 +48,11 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // in case of pointers, put something into the value set
   if(expr.type().id() == ID_pointer)
   {
-    exprt failed=
-      get_failed_symbol(expr, ns);
-
-    exprt rhs;
-
-    if(failed.is_not_nil())
-      rhs=address_of_exprt(failed, to_pointer_type(expr.type()));
-    else
-      rhs=exprt(ID_invalid);
+    exprt rhs = [&]() -> exprt {
+      if(auto failed = get_failed_symbol(expr, ns))
+        return address_of_exprt(*failed, to_pointer_type(expr.type()));
+      return exprt(ID_invalid);
+    }();
 
     state.rename(rhs, ns, goto_symex_statet::L1);
     state.value_set.assign(ssa, rhs, ns, true, false);

src/pointer-analysis/add_failed_symbols.cpp

@@ -89,17 +89,16 @@ void add_failed_symbols(symbol_table_baset &symbol_table)
 /// Get the failed-dereference symbol for the given symbol
 /// \param expr: symbol expression to get a failed symbol for
 /// \param ns: global namespace
-/// \return symbol expression for the failed-dereference symbol, or nil_exprt
-///   if none exists.
-exprt get_failed_symbol(
-  const symbol_exprt &expr,
-  const namespacet &ns)
+/// \return symbol expression for the failed-dereference symbol, or an empty
+///   optional if none exists.
+optionalt<symbol_exprt>
+get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
 {
   const symbolt &symbol=ns.lookup(expr);
   irep_idt failed_symbol_id=symbol.type.get(ID_C_failed_symbol);
 
   if(failed_symbol_id.empty())
-    return nil_exprt();
+    return {};
 
   const symbolt &failed_symbol=ns.lookup(failed_symbol_id);
 

src/pointer-analysis/add_failed_symbols.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H
 
 #include <util/irep.h>
+#include <util/optional.h>
 
 class symbol_table_baset;
 class symbolt;
@@ -27,8 +28,7 @@ void add_failed_symbol_if_needed(
 
 irep_idt failed_symbol_id(const irep_idt &identifier);
 
-exprt get_failed_symbol(
-  const symbol_exprt &expr,
-  const namespacet &ns);
+optionalt<symbol_exprt>
+get_failed_symbol(const symbol_exprt &expr, const namespacet &ns);
 
 #endif // CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H

src/pointer-analysis/value_set.cpp

@@ -1469,12 +1469,9 @@ void value_sett::apply_code_rec(
       (lhs_type.id() == ID_array && lhs_type.subtype().id() == ID_pointer))
     {
       // assign the address of the failed object
-      exprt failed=get_failed_symbol(to_symbol_expr(lhs), ns);
-
-      if(failed.is_not_nil())
+      if(auto failed = get_failed_symbol(to_symbol_expr(lhs), ns))
       {
-        address_of_exprt address_of_expr(
-          failed, to_pointer_type(lhs.type()));
+        address_of_exprt address_of_expr(*failed, to_pointer_type(lhs.type()));
         assign(lhs, address_of_expr, ns, false, false);
       }
       else