{"action":"created","comment":{"url":"https://api.github.com/repos/diffblue/cbmc/pulls/comments/99881369","pull_request_review_id":20564345,"id":99881369,"diff_hunk":"@@ -0,0 +1,583 @@\n+/*******************************************************************\\\n+\n+Module: Remove exception handling \n+\n+Author: Cristina David\n+\n+Date:   December 2016\n+\n+\\*******************************************************************/\n+// #define DEBUG\n+#ifdef DEBUG\n+#include<iostream>\n+#endif\n+#include <stack>\n+\n+#include <util/std_expr.h>\n+#include <util/symbol_table.h>\n+\n+#include \"remove_exceptions.h\"\n+\n+class exceptiont\n+{\n+public:\n+  typedef std::vector<std::pair<irep_idt,\n+    goto_programt::targett>> catch_handlerst;\n+  catch_handlerst catch_handlers;\n+};\n+\n+typedef std::vector<exceptiont> stack_catcht;\n+\n+class remove_exceptionst\n+{\n+public:\n+  explicit remove_exceptionst(symbol_tablet &_symbol_table):\n+    symbol_table(_symbol_table)\n+  {\n+  }\n+\n+  void operator()(\n+    goto_functionst &goto_functions);\n+\n+protected:\n+  symbol_tablet &symbol_table;\n+\n+  void add_exceptional_returns(\n+    goto_functionst::function_mapt::iterator);\n+\n+  void replace_throws(\n+    goto_functionst::function_mapt::iterator);\n+\n+  void instrument_function_calls(\n+    goto_functionst::function_mapt::iterator);\n+\n+  void instrument_exception_handlers(\n+    goto_functionst::function_mapt::iterator);\n+  void add_gotos(\n+    goto_functionst::function_mapt::iterator);\n+\n+  void add_throw_gotos(\n+    goto_functionst::function_mapt::iterator,\n+    goto_programt::instructionst::iterator instr_it,\n+    stack_catcht stack_catch);\n+\n+  void add_function_call_gotos(\n+    goto_functionst::function_mapt::iterator func_it,\n+    goto_programt::instructionst::iterator instr_it,\n+    stack_catcht stack_catch);\n+};\n+\n+void remove_exceptionst::add_exceptional_returns(\n+  goto_functionst::function_mapt::iterator func_it)\n+{\n+  const irep_idt function_id=func_it->first;\n+  goto_programt &goto_program=func_it->second.body;\n+\n+  if(goto_program.empty())\n+    return;\n+\n+  // We generate an exceptional return value for any function that has\n+  // a throw or a function call. This can be improved by only considering\n+  // function calls that may escape exceptions. However, this will\n+  // require multiple passes.\n+  Forall_goto_program_instructions(instr_it, goto_program)\n+  {\n+    if(instr_it->is_throw() || instr_it->is_function_call())\n+    {\n+      // look up the function symbol\n+      symbol_tablet::symbolst::iterator s_it=\n+        symbol_table.symbols.find(function_id);\n+\n+      assert(s_it!=symbol_table.symbols.end());\n+      symbolt &function_symbol=s_it->second;\n+\n+      auxiliary_symbolt new_symbol;\n+      new_symbol.is_static_lifetime=true;\n+      new_symbol.module=function_symbol.module;\n+      new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;\n+      new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;\n+      new_symbol.mode=function_symbol.mode;\n+      new_symbol.type=typet(ID_pointer, empty_typet());\n+      symbol_table.add(new_symbol);\n+\n+      // initialize the exceptional return with NULL\n+      symbol_exprt lhs_expr_null;\n+      lhs_expr_null.set_identifier(id2string(function_symbol.name)+EXC_SUFFIX);\n+      lhs_expr_null.type()=typet(ID_pointer, empty_typet());\n+\n+      exprt rhs_expr_null;\n+      rhs_expr_null=null_pointer_exprt(pointer_typet());\n+      goto_programt::targett t_null=goto_program.insert_before(instr_it);\n+      t_null->make_assignment();\n+      t_null->source_location=instr_it->source_location;\n+      t_null->code=code_assignt(\n+        lhs_expr_null,\n+        typecast_exprt(rhs_expr_null, lhs_expr_null.type()));\n+      t_null->function=instr_it->function;\n+      return;\n+    }\n+  }\n+}\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptionst::replace_throws\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose: turns 'throw x' in function f into an assignment to f#exc_value\n+\n+\\*******************************************************************/\n+\n+void remove_exceptionst::replace_throws(\n+  goto_functionst::function_mapt::iterator func_it)\n+{\n+  const irep_idt function_id=func_it->first;\n+  goto_programt &goto_program=func_it->second.body;\n+\n+  if(goto_program.empty())\n+    return;\n+\n+  Forall_goto_program_instructions(instr_it, goto_program)\n+  {\n+    if(instr_it->is_throw() &&\n+       symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX))\n+    {\n+      assert(instr_it->code.operands().size()==1);\n+      symbolt &function_symbol=symbol_table.lookup(id2string(function_id)+\n+                                                  EXC_SUFFIX);\n+\n+      // replace \"throw x;\" by \"f#exception_value=x;\"\n+      symbol_exprt lhs_expr;\n+      lhs_expr.set_identifier(id2string(function_id)+EXC_SUFFIX);\n+      lhs_expr.type()=function_symbol.type;\n+\n+      // find the symbol corresponding to the thrown exceptions\n+      exprt exc_symbol=instr_it->code;\n+      while(exc_symbol.id()!=ID_symbol)\n+        exc_symbol=exc_symbol.op0();\n+\n+      // add the assignment with the appropriate cast\n+      code_assignt assignment(typecast_exprt(lhs_expr, exc_symbol.type()),\n+                              exc_symbol);\n+\n+      // now turn the `throw' into `assignment'\n+      instr_it->type=ASSIGN;\n+      instr_it->code=assignment;\n+    }\n+  }\n+}\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptionst::instrument_function_calls\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose: after each function call g() in function f \n+         adds f#exception_value=g#exception_value;\n+\n+\\*******************************************************************/\n+\n+void remove_exceptionst::instrument_function_calls(\n+  goto_functionst::function_mapt::iterator func_it)\n+{\n+  const irep_idt &caller_id=func_it->first;\n+  goto_programt &goto_program=func_it->second.body;\n+\n+  if(goto_program.empty())\n+    return;\n+\n+  Forall_goto_program_instructions(instr_it, goto_program)\n+  {\n+    if(instr_it->is_function_call())\n+    {\n+      code_function_callt &function_call=to_code_function_call(instr_it->code);\n+      const irep_idt &callee_id=\n+        to_symbol_expr(function_call.function()).get_identifier();\n+\n+      // can exceptions escape?\n+      if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX) &&\n+        symbol_table.has_symbol(id2string(caller_id)+EXC_SUFFIX))\n+      {\n+        symbolt &callee=symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX);\n+        symbolt &caller=symbol_table.lookup(id2string(caller_id)+EXC_SUFFIX);\n+\n+        symbol_exprt rhs_expr;\n+        rhs_expr.set_identifier(id2string(callee_id)+EXC_SUFFIX);\n+        rhs_expr.type()=callee.type;\n+\n+        symbol_exprt lhs_expr;\n+        lhs_expr.set_identifier(id2string(caller_id)+EXC_SUFFIX);\n+        lhs_expr.type()=caller.type;\n+\n+        goto_programt::targett t=goto_program.insert_after(instr_it);\n+        t->make_assignment();\n+        t->source_location=instr_it->source_location;\n+        t->code=code_assignt(lhs_expr, rhs_expr);\n+        t->function=instr_it->function;\n+      }\n+    }\n+  }\n+}\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptionst::instrument_exception_handlers\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose: at the beginning of each handler in function f \n+         adds exc=f#exception_value; f#exception_value=NULL;\n+\n+\\*******************************************************************/\n+\n+void remove_exceptionst::instrument_exception_handlers(\n+  goto_functionst::function_mapt::iterator func_it)\n+{\n+  const irep_idt &function_id=func_it->first;\n+  goto_programt &goto_program=func_it->second.body;\n+\n+  if(goto_program.empty())\n+    return;\n+\n+  Forall_goto_program_instructions(instr_it, goto_program)\n+  {\n+    // is this a handler\n+    if(instr_it->type==CATCH && instr_it->code.find(ID_handler)!=get_nil_irep())\n+    {\n+      // retrieve the exception variable\n+      const irept &exception=instr_it->code.find(ID_handler);\n+\n+      if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX))\n+      {\n+        symbolt &function_symbol=symbol_table.lookup(id2string(function_id)+\n+                                                    EXC_SUFFIX);\n+        // next we reset the exceptional return to NULL\n+        symbol_exprt lhs_expr_null;\n+        lhs_expr_null.set_identifier(id2string(function_id)+EXC_SUFFIX);\n+        lhs_expr_null.type()=function_symbol.type;\n+        exprt rhs_expr_null;\n+        rhs_expr_null=null_pointer_exprt(pointer_typet());\n+\n+        // add the assignment\n+        goto_programt::targett t_null=goto_program.insert_after(instr_it);\n+        t_null->make_assignment();\n+        t_null->source_location=instr_it->source_location;\n+        t_null->code=code_assignt(\n+          lhs_expr_null,\n+          typecast_exprt(rhs_expr_null, lhs_expr_null.type()));\n+        t_null->function=instr_it->function;\n+\n+        // add the assignment exc=f#exception_value\n+        symbol_exprt rhs_expr_exc;\n+        rhs_expr_exc.set_identifier(id2string(function_id)+EXC_SUFFIX);\n+        rhs_expr_exc.type()=function_symbol.type;\n+\n+        const exprt &lhs_expr_exc=static_cast<const exprt &>(exception);\n+        goto_programt::targett t_exc=goto_program.insert_after(instr_it);\n+        t_exc->make_assignment();\n+        t_exc->source_location=instr_it->source_location;\n+        t_exc->code=code_assignt(\n+          typecast_exprt(lhs_expr_exc, rhs_expr_exc.type()),\n+          rhs_expr_exc);\n+        t_exc->function=instr_it->function;\n+      }\n+\n+      instr_it->make_skip();\n+    }\n+  }\n+}\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptionst::add_gotos_throw\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose: instruments each throw with conditional GOTOS to the \n+         corresponding exception handlers\n+\n+\\*******************************************************************/\n+void remove_exceptionst::add_throw_gotos(\n+  goto_functionst::function_mapt::iterator func_it,\n+  goto_programt::instructionst::iterator instr_it,\n+  stack_catcht stack_catch)\n+{\n+  assert(instr_it->type==THROW);\n+\n+  goto_programt &goto_program=func_it->second.body;\n+\n+  assert(instr_it->code.operands().size()==1);\n+\n+  // make sure that these are always forward gotos\n+  assert(!instr_it->is_backwards_goto());\n+\n+  // jump to the end of the function\n+  // this will appear after the GOTO-based dynamic dispatch below\n+  goto_programt::targett t_end=goto_program.insert_after(instr_it);\n+  goto_programt::targett new_state;\n+  // find the end of the function\n+  for(goto_programt::instructionst::iterator inner_it=instr_it;\n+      inner_it!=goto_program.instructions.end();\n+      ++inner_it)\n+  {\n+    if(inner_it->is_end_function())\n+      new_state=inner_it;\n+  }\n+  t_end->make_goto(new_state);\n+  t_end->source_location=instr_it->source_location;\n+  t_end->function=instr_it->function;\n+\n+  // add GOTOs implementing the dynamic dispatch of the\n+  // exception handlers\n+  for(std::size_t i=stack_catch.size(); i-->0;)\n+  {\n+    for(std::size_t j=stack_catch[i].catch_handlers.size(); j-->0;)\n+    {\n+      goto_programt::targett new_state_pc;\n+      new_state_pc=stack_catch[i].catch_handlers[j].second;\n+\n+      // find handler\n+      goto_programt::targett t_exc=goto_program.insert_after(instr_it);\n+      t_exc->make_goto(new_state_pc);\n+      t_exc->source_location=instr_it->source_location;\n+      t_exc->function=instr_it->function;\n+\n+      // use instanceof to check that this is the correct handler\n+      symbol_typet type(stack_catch[i].catch_handlers[j].first);\n+      type_exprt expr(type);\n+      // find the symbol corresponding to the caught exceptions\n+      exprt exc_symbol=instr_it->code;\n+      while(exc_symbol.id()!=ID_symbol)\n+        exc_symbol=exc_symbol.op0();\n+\n+      binary_predicate_exprt check(exc_symbol, ID_java_instanceof, expr);\n+      t_exc->guard=check;\n+    }\n+  }\n+}\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptionst::add_function_call_gotos\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose: instruments each function call that may escape exceptions\n+          with conditional GOTOS to the corresponding exception handlers\n+\n+\\*******************************************************************/\n+void remove_exceptionst::add_function_call_gotos(\n+  goto_functionst::function_mapt::iterator func_it,\n+  goto_programt::instructionst::iterator instr_it,\n+  stack_catcht stack_catch)\n+{\n+  assert(instr_it->type==FUNCTION_CALL);\n+\n+  goto_programt &goto_program=func_it->second.body;\n+\n+  // save the address of the next instruction\n+  goto_programt::instructionst::iterator next_it=instr_it;\n+  next_it++;\n+\n+  code_function_callt &function_call=to_code_function_call(instr_it->code);\n+  assert(function_call.function().id()==ID_symbol);\n+  const irep_idt &callee_id=\n+    to_symbol_expr(function_call.function()).get_identifier();\n+\n+  if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX))\n+  {\n+    // dynamic dispatch of the escaped exception\n+    symbolt &callee_exc_symbol=symbol_table.lookup(id2string(callee_id)+\n+                                                   EXC_SUFFIX);\n+    symbol_exprt callee_exc;\n+    callee_exc.set_identifier(id2string(callee_id)+EXC_SUFFIX);\n+    callee_exc.type()=callee_exc_symbol.type;\n+\n+    for(std::size_t i=stack_catch.size(); i-->0;)\n+    {\n+      for(std::size_t j=stack_catch[i].catch_handlers.size(); j-->0;)\n+      {\n+        goto_programt::targett new_state_pc;\n+        new_state_pc=stack_catch[i].catch_handlers[j].second;\n+        goto_programt::targett t_exc=goto_program.insert_after(instr_it);\n+        t_exc->make_goto(new_state_pc);\n+        t_exc->source_location=instr_it->source_location;\n+        t_exc->function=instr_it->function;\n+        // use instanceof to check that this is the correct handler\n+        symbol_typet type(stack_catch[i].catch_handlers[j].first);\n+        type_exprt expr(type);\n+        binary_predicate_exprt check_instanceof(\n+          callee_exc,\n+          ID_java_instanceof,\n+          expr);\n+        t_exc->guard=check_instanceof;\n+      }\n+    }\n+\n+    // add a null check (so that instanceof can ba applied)\n+    equal_exprt eq_null(typecast_exprt(callee_exc, pointer_typet()),\n+                        null_pointer_exprt(pointer_typet()));\n+    // jump to the next instruction\n+    goto_programt::targett t_null=goto_program.insert_after(instr_it);\n+    t_null->make_goto(next_it);\n+    t_null->source_location=instr_it->source_location;\n+    t_null->function=instr_it->function;\n+    t_null->guard=eq_null;\n+  }\n+}\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptionst::add_gotos\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose: instruments each throw and function calls that may escape exceptions\n+         with conditional GOTOS to the corresponding exception handlers\n+\n+\\*******************************************************************/\n+void remove_exceptionst::add_gotos(\n+  goto_functionst::function_mapt::iterator func_it)\n+{\n+  // Stack of try-catch blocks\n+  stack_catcht stack_catch;\n+\n+  goto_programt &goto_program=func_it->second.body;\n+\n+  if(goto_program.empty())\n+    return;\n+  Forall_goto_program_instructions(instr_it, goto_program)\n+  {\n+    // it's a CATCH but not a handler\n+    if(instr_it->type==CATCH && instr_it->code.find(ID_handler)==get_nil_irep())\n+    {\n+      if(instr_it->targets.empty()) // pop\n+      {\n+        // pop from the stack if possible\n+        if(!stack_catch.empty())\n+        {\n+          stack_catch.pop_back();\n+        }\n+        else\n+        {\n+#ifdef DEBUG\n+          std::cout << \"Remove exceptions: empty stack\" << std::endl;\n+#endif\n+        }\n+      }\n+      else // push\n+      {\n+        exceptiont exception;\n+        // copy targets\n+        const irept::subt &exception_list=\n+          instr_it->code.find(ID_exception_list).get_sub();\n+        assert(exception_list.size()==instr_it->targets.size());\n+\n+        // Fill the map with the catch type and the target\n+        unsigned i=0;\n+        for(auto target : instr_it->targets)\n+        {\n+          exception.catch_handlers.push_back(\n+            std::make_pair(exception_list[i].id(), target));\n+          i++;\n+        }\n+\n+        // Stack it\n+        stack_catch.push_back(exception);\n+      }\n+\n+      instr_it->make_skip();\n+    }\n+    else if(instr_it->type==THROW)\n+    {\n+      add_throw_gotos(func_it, instr_it, stack_catch);\n+    }\n+    else if(instr_it->type==FUNCTION_CALL)\n+    {\n+      add_function_call_gotos(func_it, instr_it, stack_catch);\n+    }\n+  }\n+}\n+\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptionst::operator()\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose:\n+\n+\\*******************************************************************/\n+\n+void remove_exceptionst::operator()(goto_functionst &goto_functions)\n+{\n+  Forall_goto_functions(it, goto_functions)\n+  {\n+    add_exceptional_returns(it);\n+  }\n+  Forall_goto_functions(it, goto_functions)\n+  {\n+    instrument_exception_handlers(it);\n+    add_gotos(it);\n+    instrument_function_calls(it);\n+    replace_throws(it);\n+  }\n+}\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptions\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose: removes throws/CATCH-POP/CATCH-PUSH\n+\n+\\*******************************************************************/\n+\n+void remove_exceptions(\n+  symbol_tablet &symbol_table,\n+  goto_functionst &goto_functions)\n+{\n+  remove_exceptionst remove_exceptions(symbol_table);\n+  remove_exceptions(goto_functions);\n+}\n+\n+/*******************************************************************\\\n+\n+Function: remove_exceptions\n+\n+Inputs:\n+\n+Outputs:\n+\n+Purpose: removes throws/CATCH-POP/CATCH-PUSH\n+\n+\\*******************************************************************/\n+\n+void remove_exceptions(goto_modelt &goto_model)\n+{\n+  remove_exceptionst rr(goto_model.symbol_table);\n+  rr(goto_model.goto_functions);\n+}\n+\n+","path":"src/goto-programs/remove_exceptions.cpp","position":582,"original_position":582,"commit_id":"2a98385ca083f47603bf1b076a5d27796bb36db4","original_commit_id":"2a98385ca083f47603bf1b076a5d27796bb36db4","user":{"login":"peterschrammel","id":4222448,"avatar_url":"https://avatars.githubusercontent.com/u/4222448?v=3","gravatar_id":"","url":"https://api.github.com/users/peterschrammel","html_url":"https://github.com/peterschrammel","followers_url":"https://api.github.com/users/peterschrammel/followers","following_url":"https://api.github.com/users/peterschrammel/following{/other_user}","gists_url":"https://api.github.com/users/peterschrammel/gists{/gist_id}","starred_url":"https://api.github.com/users/peterschrammel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/peterschrammel/subscriptions","organizations_url":"https://api.github.com/users/peterschrammel/orgs","repos_url":"https://api.github.com/users/peterschrammel/repos","events_url":"https://api.github.com/users/peterschrammel/events{/privacy}","received_events_url":"https://api.github.com/users/peterschrammel/received_events","type":"User","site_admin":false},"body":"remove blank lines","created_at":"2017-02-07T17:36:57Z","updated_at":"2017-02-07T17:50:12Z","html_url":"https://github.com/diffblue/cbmc/pull/506#discussion_r99881369","pull_request_url":"https://api.github.com/repos/diffblue/cbmc/pulls/506","_links":{"self":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/comments/99881369"},"html":{"href":"https://github.com/diffblue/cbmc/pull/506#discussion_r99881369"},"pull_request":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/506"}}},"pull_request":{"url":"https://api.github.com/repos/diffblue/cbmc/pulls/506","id":104811001,"html_url":"https://github.com/diffblue/cbmc/pull/506","diff_url":"https://github.com/diffblue/cbmc/pull/506.diff","patch_url":"https://github.com/diffblue/cbmc/pull/506.patch","issue_url":"https://api.github.com/repos/diffblue/cbmc/issues/506","number":506,"state":"open","locked":false,"title":"Java exception handling","user":{"login":"cristina-david","id":5973782,"avatar_url":"https://avatars.githubusercontent.com/u/5973782?v=3","gravatar_id":"","url":"https://api.github.com/users/cristina-david","html_url":"https://github.com/cristina-david","followers_url":"https://api.github.com/users/cristina-david/followers","following_url":"https://api.github.com/users/cristina-david/following{/other_user}","gists_url":"https://api.github.com/users/cristina-david/gists{/gist_id}","starred_url":"https://api.github.com/users/cristina-david/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cristina-david/subscriptions","organizations_url":"https://api.github.com/users/cristina-david/orgs","repos_url":"https://api.github.com/users/cristina-david/repos","events_url":"https://api.github.com/users/cristina-david/events{/privacy}","received_events_url":"https://api.github.com/users/cristina-david/received_events","type":"User","site_admin":false},"body":"Exceptions are handled by introducing exceptional return variables for program functions. In this PR, a function is added such a return variable if it contains a throw or a function call (as the function being called may escape exceptions). This is too permissive and will be improved in a subsequent PR which uses an uncaught exceptions analysis to get a better approximation of the set of exceptions escaped by a function.\r\n\r\n@mgu is currently testing this on datastax so I'm still in the process of fixing reported problems.","created_at":"2017-02-06T14:44:23Z","updated_at":"2017-02-07T17:50:12Z","closed_at":null,"merged_at":null,"merge_commit_sha":"43ef99ea7de75ebbf702592134cbbdf6605daeb6","assignee":null,"assignees":[],"milestone":null,"commits_url":"https://api.github.com/repos/diffblue/cbmc/pulls/506/commits","review_comments_url":"https://api.github.com/repos/diffblue/cbmc/pulls/506/comments","review_comment_url":"https://api.github.com/repos/diffblue/cbmc/pulls/comments{/number}","comments_url":"https://api.github.com/repos/diffblue/cbmc/issues/506/comments","statuses_url":"https://api.github.com/repos/diffblue/cbmc/statuses/2a98385ca083f47603bf1b076a5d27796bb36db4","head":{"label":"cristina-david:exception-handling","ref":"exception-handling","sha":"2a98385ca083f47603bf1b076a5d27796bb36db4","user":{"login":"cristina-david","id":5973782,"avatar_url":"https://avatars.githubusercontent.com/u/5973782?v=3","gravatar_id":"","url":"https://api.github.com/users/cristina-david","html_url":"https://github.com/cristina-david","followers_url":"https://api.github.com/users/cristina-david/followers","following_url":"https://api.github.com/users/cristina-david/following{/other_user}","gists_url":"https://api.github.com/users/cristina-david/gists{/gist_id}","starred_url":"https://api.github.com/users/cristina-david/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cristina-david/subscriptions","organizations_url":"https://api.github.com/users/cristina-david/orgs","repos_url":"https://api.github.com/users/cristina-david/repos","events_url":"https://api.github.com/users/cristina-david/events{/privacy}","received_events_url":"https://api.github.com/users/cristina-david/received_events","type":"User","site_admin":false},"repo":{"id":80735617,"name":"cbmc","full_name":"cristina-david/cbmc","owner":{"login":"cristina-david","id":5973782,"avatar_url":"https://avatars.githubusercontent.com/u/5973782?v=3","gravatar_id":"","url":"https://api.github.com/users/cristina-david","html_url":"https://github.com/cristina-david","followers_url":"https://api.github.com/users/cristina-david/followers","following_url":"https://api.github.com/users/cristina-david/following{/other_user}","gists_url":"https://api.github.com/users/cristina-david/gists{/gist_id}","starred_url":"https://api.github.com/users/cristina-david/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cristina-david/subscriptions","organizations_url":"https://api.github.com/users/cristina-david/orgs","repos_url":"https://api.github.com/users/cristina-david/repos","events_url":"https://api.github.com/users/cristina-david/events{/privacy}","received_events_url":"https://api.github.com/users/cristina-david/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/cristina-david/cbmc","description":"C Bounded Model Checker","fork":true,"url":"https://api.github.com/repos/cristina-david/cbmc","forks_url":"https://api.github.com/repos/cristina-david/cbmc/forks","keys_url":"https://api.github.com/repos/cristina-david/cbmc/keys{/key_id}","collaborators_url":"https://api.github.com/repos/cristina-david/cbmc/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/cristina-david/cbmc/teams","hooks_url":"https://api.github.com/repos/cristina-david/cbmc/hooks","issue_events_url":"https://api.github.com/repos/cristina-david/cbmc/issues/events{/number}","events_url":"https://api.github.com/repos/cristina-david/cbmc/events","assignees_url":"https://api.github.com/repos/cristina-david/cbmc/assignees{/user}","branches_url":"https://api.github.com/repos/cristina-david/cbmc/branches{/branch}","tags_url":"https://api.github.com/repos/cristina-david/cbmc/tags","blobs_url":"https://api.github.com/repos/cristina-david/cbmc/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/cristina-david/cbmc/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/cristina-david/cbmc/git/refs{/sha}","trees_url":"https://api.github.com/repos/cristina-david/cbmc/git/trees{/sha}","statuses_url":"https://api.github.com/repos/cristina-david/cbmc/statuses/{sha}","languages_url":"https://api.github.com/repos/cristina-david/cbmc/languages","stargazers_url":"https://api.github.com/repos/cristina-david/cbmc/stargazers","contributors_url":"https://api.github.com/repos/cristina-david/cbmc/contributors","subscribers_url":"https://api.github.com/repos/cristina-david/cbmc/subscribers","subscription_url":"https://api.github.com/repos/cristina-david/cbmc/subscription","commits_url":"https://api.github.com/repos/cristina-david/cbmc/commits{/sha}","git_commits_url":"https://api.github.com/repos/cristina-david/cbmc/git/commits{/sha}","comments_url":"https://api.github.com/repos/cristina-david/cbmc/comments{/number}","issue_comment_url":"https://api.github.com/repos/cristina-david/cbmc/issues/comments{/number}","contents_url":"https://api.github.com/repos/cristina-david/cbmc/contents/{+path}","compare_url":"https://api.github.com/repos/cristina-david/cbmc/compare/{base}...{head}","merges_url":"https://api.github.com/repos/cristina-david/cbmc/merges","archive_url":"https://api.github.com/repos/cristina-david/cbmc/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/cristina-david/cbmc/downloads","issues_url":"https://api.github.com/repos/cristina-david/cbmc/issues{/number}","pulls_url":"https://api.github.com/repos/cristina-david/cbmc/pulls{/number}","milestones_url":"https://api.github.com/repos/cristina-david/cbmc/milestones{/number}","notifications_url":"https://api.github.com/repos/cristina-david/cbmc/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/cristina-david/cbmc/labels{/name}","releases_url":"https://api.github.com/repos/cristina-david/cbmc/releases{/id}","deployments_url":"https://api.github.com/repos/cristina-david/cbmc/deployments","created_at":"2017-02-02T14:57:42Z","updated_at":"2017-02-02T14:57:51Z","pushed_at":"2017-02-07T02:19:41Z","git_url":"git://github.com/cristina-david/cbmc.git","ssh_url":"git@github.com:cristina-david/cbmc.git","clone_url":"https://github.com/cristina-david/cbmc.git","svn_url":"https://github.com/cristina-david/cbmc","homepage":"http://www.cprover.org/cbmc","size":16526,"stargazers_count":0,"watchers_count":0,"language":"C++","has_issues":false,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":0,"mirror_url":null,"open_issues_count":0,"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"diffblue:master","ref":"master","sha":"f747a29d95f0348a3e500d3d4c8e4b1121edf175","user":{"login":"diffblue","id":17216098,"avatar_url":"https://avatars.githubusercontent.com/u/17216098?v=3","gravatar_id":"","url":"https://api.github.com/users/diffblue","html_url":"https://github.com/diffblue","followers_url":"https://api.github.com/users/diffblue/followers","following_url":"https://api.github.com/users/diffblue/following{/other_user}","gists_url":"https://api.github.com/users/diffblue/gists{/gist_id}","starred_url":"https://api.github.com/users/diffblue/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/diffblue/subscriptions","organizations_url":"https://api.github.com/users/diffblue/orgs","repos_url":"https://api.github.com/users/diffblue/repos","events_url":"https://api.github.com/users/diffblue/events{/privacy}","received_events_url":"https://api.github.com/users/diffblue/received_events","type":"Organization","site_admin":false},"repo":{"id":51877056,"name":"cbmc","full_name":"diffblue/cbmc","owner":{"login":"diffblue","id":17216098,"avatar_url":"https://avatars.githubusercontent.com/u/17216098?v=3","gravatar_id":"","url":"https://api.github.com/users/diffblue","html_url":"https://github.com/diffblue","followers_url":"https://api.github.com/users/diffblue/followers","following_url":"https://api.github.com/users/diffblue/following{/other_user}","gists_url":"https://api.github.com/users/diffblue/gists{/gist_id}","starred_url":"https://api.github.com/users/diffblue/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/diffblue/subscriptions","organizations_url":"https://api.github.com/users/diffblue/orgs","repos_url":"https://api.github.com/users/diffblue/repos","events_url":"https://api.github.com/users/diffblue/events{/privacy}","received_events_url":"https://api.github.com/users/diffblue/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/diffblue/cbmc","description":"C Bounded Model Checker","fork":false,"url":"https://api.github.com/repos/diffblue/cbmc","forks_url":"https://api.github.com/repos/diffblue/cbmc/forks","keys_url":"https://api.github.com/repos/diffblue/cbmc/keys{/key_id}","collaborators_url":"https://api.github.com/repos/diffblue/cbmc/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/diffblue/cbmc/teams","hooks_url":"https://api.github.com/repos/diffblue/cbmc/hooks","issue_events_url":"https://api.github.com/repos/diffblue/cbmc/issues/events{/number}","events_url":"https://api.github.com/repos/diffblue/cbmc/events","assignees_url":"https://api.github.com/repos/diffblue/cbmc/assignees{/user}","branches_url":"https://api.github.com/repos/diffblue/cbmc/branches{/branch}","tags_url":"https://api.github.com/repos/diffblue/cbmc/tags","blobs_url":"https://api.github.com/repos/diffblue/cbmc/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/diffblue/cbmc/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/diffblue/cbmc/git/refs{/sha}","trees_url":"https://api.github.com/repos/diffblue/cbmc/git/trees{/sha}","statuses_url":"https://api.github.com/repos/diffblue/cbmc/statuses/{sha}","languages_url":"https://api.github.com/repos/diffblue/cbmc/languages","stargazers_url":"https://api.github.com/repos/diffblue/cbmc/stargazers","contributors_url":"https://api.github.com/repos/diffblue/cbmc/contributors","subscribers_url":"https://api.github.com/repos/diffblue/cbmc/subscribers","subscription_url":"https://api.github.com/repos/diffblue/cbmc/subscription","commits_url":"https://api.github.com/repos/diffblue/cbmc/commits{/sha}","git_commits_url":"https://api.github.com/repos/diffblue/cbmc/git/commits{/sha}","comments_url":"https://api.github.com/repos/diffblue/cbmc/comments{/number}","issue_comment_url":"https://api.github.com/repos/diffblue/cbmc/issues/comments{/number}","contents_url":"https://api.github.com/repos/diffblue/cbmc/contents/{+path}","compare_url":"https://api.github.com/repos/diffblue/cbmc/compare/{base}...{head}","merges_url":"https://api.github.com/repos/diffblue/cbmc/merges","archive_url":"https://api.github.com/repos/diffblue/cbmc/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/diffblue/cbmc/downloads","issues_url":"https://api.github.com/repos/diffblue/cbmc/issues{/number}","pulls_url":"https://api.github.com/repos/diffblue/cbmc/pulls{/number}","milestones_url":"https://api.github.com/repos/diffblue/cbmc/milestones{/number}","notifications_url":"https://api.github.com/repos/diffblue/cbmc/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/diffblue/cbmc/labels{/name}","releases_url":"https://api.github.com/repos/diffblue/cbmc/releases{/id}","deployments_url":"https://api.github.com/repos/diffblue/cbmc/deployments","created_at":"2016-02-16T23:03:52Z","updated_at":"2017-01-19T22:11:12Z","pushed_at":"2017-02-07T17:08:21Z","git_url":"git://github.com/diffblue/cbmc.git","ssh_url":"git@github.com:diffblue/cbmc.git","clone_url":"https://github.com/diffblue/cbmc.git","svn_url":"https://github.com/diffblue/cbmc","homepage":"http://www.cprover.org/cbmc","size":16498,"stargazers_count":32,"watchers_count":32,"language":"C++","has_issues":true,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":39,"mirror_url":null,"open_issues_count":153,"forks":39,"open_issues":153,"watchers":32,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/506"},"html":{"href":"https://github.com/diffblue/cbmc/pull/506"},"issue":{"href":"https://api.github.com/repos/diffblue/cbmc/issues/506"},"comments":{"href":"https://api.github.com/repos/diffblue/cbmc/issues/506/comments"},"review_comments":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/506/comments"},"review_comment":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/506/commits"},"statuses":{"href":"https://api.github.com/repos/diffblue/cbmc/statuses/2a98385ca083f47603bf1b076a5d27796bb36db4"}}}}
{"actor":{"display_login":"peterschrammel"}}