Added a side effect expr that pushes/pops Java try-catch handlers + irep ids for Java exception handling

These are used to recreate Java try-catch contructs from bytecode.

Author: cristina-david

src/util/irep_ids.txt

@@ -738,6 +738,8 @@ java_bytecode_index
 java_instanceof
 java_super_method_call
 java_enum_static_unwind
+push_catch
+handler
 string_constraint
 string_not_contains_constraint
 cprover_char_literal_func
@@ -800,4 +802,4 @@ cprover_string_to_char_array_func
 cprover_string_to_lower_case_func
 cprover_string_to_upper_case_func
 cprover_string_trim_func
-cprover_string_value_of_func
+cprover_string_value_of_func

src/util/std_code.h

@@ -1122,6 +1122,36 @@ inline const side_effect_expr_throwt &to_side_effect_expr_throw(
   assert(expr.get(ID_statement)==ID_throw);
   return static_cast<const side_effect_expr_throwt &>(expr);
 }
+/*! \brief A side effect that pushes/pops a catch handler
+*/
+class side_effect_expr_catcht:public side_effect_exprt
+{
+public:
+  inline side_effect_expr_catcht():side_effect_exprt(ID_push_catch)
+  {
+  }
+  // TODO: change to ID_catch
+  inline explicit side_effect_expr_catcht(const irept &exception_list):
+    side_effect_exprt(ID_push_catch)
+  {
+    set(ID_exception_list, exception_list);
+  }
+};
+
+static inline side_effect_expr_catcht &to_side_effect_expr_catch(exprt &expr)
+{
+  assert(expr.id()==ID_side_effect);
+  assert(expr.get(ID_statement)==ID_push_catch);
+  return static_cast<side_effect_expr_catcht &>(expr);
+}
+
+static inline const side_effect_expr_catcht &to_side_effect_expr_catch(
+  const exprt &expr)
+{
+  assert(expr.id()==ID_side_effect);
+  assert(expr.get(ID_statement)==ID_push_catch);
+  return static_cast<const side_effect_expr_catcht &>(expr);
+}
 
 /*! \brief A try/catch block
 */