{"action":"created","comment":{"url":"https://api.github.com/repos/diffblue/cbmc/pulls/comments/172544664","pull_request_review_id":101578187,"id":172544664,"diff_hunk":"@@ -0,0 +1,315 @@\n+/*******************************************************************\\\n+\n+ Module: String solver\n+\n+ Author: DiffBlue Limited. All rights reserved.\n+\n+\\*******************************************************************/\n+\n+#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H\n+#define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H\n+\n+#include <algorithm>\n+#include <iostream>\n+#include <util/ssa_expr.h>\n+#include \"string_constraint.h\"\n+#include \"string_constraint_generator.h\"\n+\n+/// For now, any unsigned bitvector type of width smaller or equal to 16 is\n+/// considered a character.\n+/// \\note type that are not characters maybe detected as characters (for\n+/// instance unsigned char in C), this will make dec_solve do unnecessary\n+/// steps for these, but should not affect correctness.\n+/// \\param type: a type\n+/// \\return true if the given type represents characters\n+bool is_char_type(const typet &type);\n+\n+/// Distinguish char array from other types.\n+/// For now, any unsigned bitvector type is considered a character.\n+/// \\param type: a type\n+/// \\param ns: namespace\n+/// \\return true if the given type is an array of characters\n+bool is_char_array_type(const typet &type, const namespacet &ns);\n+\n+/// For now, any unsigned bitvector type is considered a character.\n+/// \\param type: a type\n+/// \\return true if the given type represents a pointer to characters\n+bool is_char_pointer_type(const typet &type);\n+\n+/// \\param type: a type\n+/// \\param pred: a predicate\n+/// \\return true if one of the subtype of `type` satisfies predicate `pred`.\n+///         The meaning of \"subtype\" is in the algebraic datatype sense:\n+///         for example, the subtypes of a struct are the types of its\n+///         components, the subtype of a pointer is the type it points to,\n+///         etc...\n+///         For instance in the type `t` defined by\n+///         `{ int a; char[] b; double * c; { bool d} e}`, `int`, `char`,\n+///         `double` and `bool` are subtypes of `t`.\n+bool has_subtype(\n+  const typet &type,\n+  const std::function<bool(const typet &)> &pred);\n+\n+/// \\param type: a type\n+/// \\return true if a subtype of `type` is an pointer of characters.\n+///         The meaning of \"subtype\" is in the algebraic datatype sense:\n+///         for example, the subtypes of a struct are the types of its\n+///         components, the subtype of a pointer is the type it points to,\n+///         etc...\n+bool has_char_pointer_subtype(const typet &type);\n+\n+/// \\param type: a type\n+/// \\return true if a subtype of `type` is string_typet.\n+///         The meaning of \"subtype\" is in the algebraic datatype sense:\n+///         for example, the subtypes of a struct are the types of its\n+///         components, the subtype of a pointer is the type it points to,\n+///         etc...\n+bool has_string_subtype(const typet &type);\n+\n+/// \\param expr: an expression\n+/// \\param ns: namespace\n+/// \\return true if a subexpression of `expr` is an array of characters\n+bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);\n+\n+/// \\param expr: an expression\n+/// \\return a refined_string_exprt if expr is of type refined_string_type and\n+///   has the right structure for a refined_string_exprt\n+optionalt<refined_string_exprt> get_char_array_of_argument(const exprt &expr);\n+\n+/// \\param expr: an expression\n+/// \\return a refined_string_exprt, an invariant will fail if expr is of type\n+///   refined_string_type or cannot be cast to a refined_string_exprt\n+refined_string_exprt get_refined_string_expr_value(const exprt &expr);\n+\n+struct index_set_pairt\n+{\n+  std::map<exprt, std::set<exprt>> cumulative;\n+  std::map<exprt, std::set<exprt>> current;\n+};\n+\n+struct string_axiomst\n+{\n+  std::vector<string_constraintt> universal;\n+  std::vector<string_not_contains_constraintt> not_contains;\n+};\n+\n+/// Represents arrays of the form `array_of(x) with {i:=a} with {j:=b} ...`\n+/// by a default value `x` and a list of entries `(i,a)`, `(j,b)` etc.\n+class sparse_arrayt\n+{\n+public:\n+  /// Initialize a sparse array from an expression of the form\n+  /// `array_of(x) with {i:=a} with {j:=b} ...`\n+  /// This is the form in which array valuations coming from the underlying\n+  /// solver are given.\n+  explicit sparse_arrayt(const with_exprt &expr);\n+\n+  /// Creates an if_expr corresponding to the result of accessing the array\n+  /// at the given index\n+  virtual exprt to_if_expression(const exprt &index) const;\n+\n+protected:\n+  exprt default_value;\n+  std::vector<std::pair<std::size_t, exprt>> entries;\n+};\n+\n+/// Represents arrays by the indexes up to which the value remains the same.\n+/// For instance `{'a', 'a', 'a', 'b', 'b', 'c'}` would be represented by\n+/// by ('a', 2) ; ('b', 4), ('c', 5).\n+/// This is particularly useful when the array is constant on intervals.\n+class interval_sparse_arrayt final : public sparse_arrayt\n+{\n+public:\n+  /// An expression of the form `array_of(x) with {i:=a} with {j:=b}` is\n+  /// converted to an array `arr` where for all index `k` smaller than `i`,\n+  /// `arr[k]` is `a`, for all index between `i` (exclusive) and `j` it is `b`\n+  /// and for the others it is `x`.\n+  explicit interval_sparse_arrayt(const with_exprt &expr);\n+  exprt to_if_expression(const exprt &index) const override;\n+};\n+\n+/// Maps equation to expressions contained in them and conversely expressions to\n+/// equations that contain them. This can be used on a subset of expressions\n+/// which interests us, in particular strings. Equations are identified by an\n+/// index of type `std::size_t` for more efficient insertion and lookup.\n+class equation_symbol_mappingt\n+{\n+public:\n+  /// Record the fact that equation `i` contains expression `expr`\n+  void add(const std::size_t i, const exprt &expr);\n+\n+  /// \\param i: index corresponding to an equation\n+  /// \\return vector of expressions contained in the equation with the given\n+  ///   index `i`\n+  std::vector<exprt> find_expressions(const std::size_t i);\n+\n+  /// \\param expr: an expression\n+  /// \\return vector of equations containing the given expression `expr`\n+  std::vector<std::size_t> find_equations(const exprt &expr);\n+\n+private:\n+  /// Record index of the equations that contain a given expression\n+  std::map<exprt, std::vector<std::size_t>> equations_containing;\n+  /// Record expressions that are contained in the equation with the given index\n+  std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;\n+};\n+\n+/// Base class for string primitives\n+class string_primitivet\n+{\n+public:\n+  string_primitivet() = default;\n+  string_primitivet(const string_primitivet &) = delete;\n+\n+  virtual optionalt<array_string_exprt> string_result() const\n+  {\n+    return {};\n+  }\n+\n+  virtual std::vector<array_string_exprt> string_arguments() const\n+  {\n+    return {};\n+  }\n+};\n+\n+/// String primitive transforming one string into another\n+class string_transformation_primitivet : public string_primitivet\n+{\n+public:\n+  array_string_exprt result;\n+  array_string_exprt input;\n+  std::vector<exprt> args;\n+  exprt return_code;\n+  optionalt<array_string_exprt> string_result() const override\n+  {\n+    return result;\n+  }\n+  std::vector<array_string_exprt> string_arguments() const override\n+  {\n+    return {input};\n+  }\n+};\n+\n+/// String inserting a string into another one\n+class string_insertion_primitivet : public string_primitivet\n+{\n+public:\n+  array_string_exprt result;\n+  array_string_exprt input1;\n+  array_string_exprt input2;\n+  std::vector<exprt> args;\n+  exprt return_code;\n+\n+  /// Constructor from arguments of a function application\n+  string_insertion_primitivet(\n+    const std::vector<exprt> &fun_args,\n+    array_poolt &array_pool);\n+\n+  optionalt<array_string_exprt> string_result() const override\n+  {\n+    return result;\n+  }\n+  std::vector<array_string_exprt> string_arguments() const override\n+  {\n+    return {input1, input2};\n+  }\n+};\n+\n+/// String creation from other types\n+class string_creation_primitivet : public string_primitivet\n+{\n+public:\n+  array_string_exprt result;\n+  std::vector<exprt> args;\n+  exprt return_code;\n+\n+  optionalt<array_string_exprt> string_result() const override\n+  {\n+    return result;\n+  }\n+};\n+\n+/// String test\n+class string_test_primitivet : public string_primitivet\n+{\n+public:\n+  exprt result;\n+  std::vector<array_string_exprt> under_test;\n+  std::vector<exprt> args;\n+  std::vector<array_string_exprt> string_arguments() const override\n+  {\n+    return under_test;\n+  }\n+};\n+\n+/// Keep track of dependencies between strings.\n+/// Each string points to primitive calls on which it depends,","path":"src/solvers/refinement/string_refinement_util.h","position":243,"original_position":246,"commit_id":"98ee2225ce7a6459879d810fdf3b9e4e65a98cbd","original_commit_id":"badfd699bc39737e9eb0c49248a1de0c885d1652","user":{"login":"romainbrenguier","id":11854194,"avatar_url":"https://avatars2.githubusercontent.com/u/11854194?v=4","gravatar_id":"","url":"https://api.github.com/users/romainbrenguier","html_url":"https://github.com/romainbrenguier","followers_url":"https://api.github.com/users/romainbrenguier/followers","following_url":"https://api.github.com/users/romainbrenguier/following{/other_user}","gists_url":"https://api.github.com/users/romainbrenguier/gists{/gist_id}","starred_url":"https://api.github.com/users/romainbrenguier/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/romainbrenguier/subscriptions","organizations_url":"https://api.github.com/users/romainbrenguier/orgs","repos_url":"https://api.github.com/users/romainbrenguier/repos","events_url":"https://api.github.com/users/romainbrenguier/events{/privacy}","received_events_url":"https://api.github.com/users/romainbrenguier/received_events","type":"User","site_admin":false},"body":"@smowton What about \"builtin functions\" ? I would rename `string_primitivet` to `string_builtin_functiont` and so on.","created_at":"2018-03-06T15:04:17Z","updated_at":"2018-03-06T15:04:17Z","html_url":"https://github.com/diffblue/cbmc/pull/1895#discussion_r172544664","pull_request_url":"https://api.github.com/repos/diffblue/cbmc/pulls/1895","author_association":"MEMBER","_links":{"self":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/comments/172544664"},"html":{"href":"https://github.com/diffblue/cbmc/pull/1895#discussion_r172544664"},"pull_request":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/1895"}},"in_reply_to_id":171791478},"pull_request":{"url":"https://api.github.com/repos/diffblue/cbmc/pulls/1895","id":172165424,"html_url":"https://github.com/diffblue/cbmc/pull/1895","diff_url":"https://github.com/diffblue/cbmc/pull/1895.diff","patch_url":"https://github.com/diffblue/cbmc/pull/1895.patch","issue_url":"https://api.github.com/repos/diffblue/cbmc/issues/1895","number":1895,"state":"open","locked":false,"title":"Computation of dependency graph for strings [TG-2605]","user":{"login":"romainbrenguier","id":11854194,"avatar_url":"https://avatars2.githubusercontent.com/u/11854194?v=4","gravatar_id":"","url":"https://api.github.com/users/romainbrenguier","html_url":"https://github.com/romainbrenguier","followers_url":"https://api.github.com/users/romainbrenguier/followers","following_url":"https://api.github.com/users/romainbrenguier/following{/other_user}","gists_url":"https://api.github.com/users/romainbrenguier/gists{/gist_id}","starred_url":"https://api.github.com/users/romainbrenguier/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/romainbrenguier/subscriptions","organizations_url":"https://api.github.com/users/romainbrenguier/orgs","repos_url":"https://api.github.com/users/romainbrenguier/repos","events_url":"https://api.github.com/users/romainbrenguier/events{/privacy}","received_events_url":"https://api.github.com/users/romainbrenguier/received_events","type":"User","site_admin":false},"body":"This add a class to compute dependencies between strings:\r\nfor instance if we have `s1 = s2.concat(s3)` then s1 depends on s2 and s3.\r\nThis does not change the behaviour of the solver: the functionality is only used in a unit test and under `#ifdef DEBUG` in the solver for giving the graph as debug information.\r\nUltimately we want to use this dependency graph to minimise the number of `string_constraintst` that are created and instantiated in the underlying solver.\r\nFor now only `concat` and `insert` are implemented, and for all other functions we over-approximate the dependencies (for instance for `s1 = s2.substring(10)` the graph right now has both s1 depends on s2 and s2 depends on s1, though actually only s1 depends on s2).\r\n","created_at":"2018-03-01T07:53:28Z","updated_at":"2018-03-06T15:04:17Z","closed_at":null,"merged_at":null,"merge_commit_sha":"792fc7acc15c0c3d1b76748298b0346e77c2d487","assignee":null,"assignees":[],"requested_reviewers":[{"login":"kroening","id":1830565,"avatar_url":"https://avatars0.githubusercontent.com/u/1830565?v=4","gravatar_id":"","url":"https://api.github.com/users/kroening","html_url":"https://github.com/kroening","followers_url":"https://api.github.com/users/kroening/followers","following_url":"https://api.github.com/users/kroening/following{/other_user}","gists_url":"https://api.github.com/users/kroening/gists{/gist_id}","starred_url":"https://api.github.com/users/kroening/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kroening/subscriptions","organizations_url":"https://api.github.com/users/kroening/orgs","repos_url":"https://api.github.com/users/kroening/repos","events_url":"https://api.github.com/users/kroening/events{/privacy}","received_events_url":"https://api.github.com/users/kroening/received_events","type":"User","site_admin":false},{"login":"martin-cs","id":5333188,"avatar_url":"https://avatars0.githubusercontent.com/u/5333188?v=4","gravatar_id":"","url":"https://api.github.com/users/martin-cs","html_url":"https://github.com/martin-cs","followers_url":"https://api.github.com/users/martin-cs/followers","following_url":"https://api.github.com/users/martin-cs/following{/other_user}","gists_url":"https://api.github.com/users/martin-cs/gists{/gist_id}","starred_url":"https://api.github.com/users/martin-cs/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/martin-cs/subscriptions","organizations_url":"https://api.github.com/users/martin-cs/orgs","repos_url":"https://api.github.com/users/martin-cs/repos","events_url":"https://api.github.com/users/martin-cs/events{/privacy}","received_events_url":"https://api.github.com/users/martin-cs/received_events","type":"User","site_admin":false},{"login":"LAJW","id":11063742,"avatar_url":"https://avatars2.githubusercontent.com/u/11063742?v=4","gravatar_id":"","url":"https://api.github.com/users/LAJW","html_url":"https://github.com/LAJW","followers_url":"https://api.github.com/users/LAJW/followers","following_url":"https://api.github.com/users/LAJW/following{/other_user}","gists_url":"https://api.github.com/users/LAJW/gists{/gist_id}","starred_url":"https://api.github.com/users/LAJW/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/LAJW/subscriptions","organizations_url":"https://api.github.com/users/LAJW/orgs","repos_url":"https://api.github.com/users/LAJW/repos","events_url":"https://api.github.com/users/LAJW/events{/privacy}","received_events_url":"https://api.github.com/users/LAJW/received_events","type":"User","site_admin":false},{"login":"chrisr-diffblue","id":32060010,"avatar_url":"https://avatars2.githubusercontent.com/u/32060010?v=4","gravatar_id":"","url":"https://api.github.com/users/chrisr-diffblue","html_url":"https://github.com/chrisr-diffblue","followers_url":"https://api.github.com/users/chrisr-diffblue/followers","following_url":"https://api.github.com/users/chrisr-diffblue/following{/other_user}","gists_url":"https://api.github.com/users/chrisr-diffblue/gists{/gist_id}","starred_url":"https://api.github.com/users/chrisr-diffblue/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/chrisr-diffblue/subscriptions","organizations_url":"https://api.github.com/users/chrisr-diffblue/orgs","repos_url":"https://api.github.com/users/chrisr-diffblue/repos","events_url":"https://api.github.com/users/chrisr-diffblue/events{/privacy}","received_events_url":"https://api.github.com/users/chrisr-diffblue/received_events","type":"User","site_admin":false}],"requested_teams":[],"labels":[],"milestone":null,"commits_url":"https://api.github.com/repos/diffblue/cbmc/pulls/1895/commits","review_comments_url":"https://api.github.com/repos/diffblue/cbmc/pulls/1895/comments","review_comment_url":"https://api.github.com/repos/diffblue/cbmc/pulls/comments{/number}","comments_url":"https://api.github.com/repos/diffblue/cbmc/issues/1895/comments","statuses_url":"https://api.github.com/repos/diffblue/cbmc/statuses/98ee2225ce7a6459879d810fdf3b9e4e65a98cbd","head":{"label":"romainbrenguier:dependency-graph#TG-2582","ref":"dependency-graph#TG-2582","sha":"98ee2225ce7a6459879d810fdf3b9e4e65a98cbd","user":{"login":"romainbrenguier","id":11854194,"avatar_url":"https://avatars2.githubusercontent.com/u/11854194?v=4","gravatar_id":"","url":"https://api.github.com/users/romainbrenguier","html_url":"https://github.com/romainbrenguier","followers_url":"https://api.github.com/users/romainbrenguier/followers","following_url":"https://api.github.com/users/romainbrenguier/following{/other_user}","gists_url":"https://api.github.com/users/romainbrenguier/gists{/gist_id}","starred_url":"https://api.github.com/users/romainbrenguier/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/romainbrenguier/subscriptions","organizations_url":"https://api.github.com/users/romainbrenguier/orgs","repos_url":"https://api.github.com/users/romainbrenguier/repos","events_url":"https://api.github.com/users/romainbrenguier/events{/privacy}","received_events_url":"https://api.github.com/users/romainbrenguier/received_events","type":"User","site_admin":false},"repo":{"id":64766217,"name":"cbmc","full_name":"romainbrenguier/cbmc","owner":{"login":"romainbrenguier","id":11854194,"avatar_url":"https://avatars2.githubusercontent.com/u/11854194?v=4","gravatar_id":"","url":"https://api.github.com/users/romainbrenguier","html_url":"https://github.com/romainbrenguier","followers_url":"https://api.github.com/users/romainbrenguier/followers","following_url":"https://api.github.com/users/romainbrenguier/following{/other_user}","gists_url":"https://api.github.com/users/romainbrenguier/gists{/gist_id}","starred_url":"https://api.github.com/users/romainbrenguier/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/romainbrenguier/subscriptions","organizations_url":"https://api.github.com/users/romainbrenguier/orgs","repos_url":"https://api.github.com/users/romainbrenguier/repos","events_url":"https://api.github.com/users/romainbrenguier/events{/privacy}","received_events_url":"https://api.github.com/users/romainbrenguier/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/romainbrenguier/cbmc","description":"C Bounded Model Checker","fork":true,"url":"https://api.github.com/repos/romainbrenguier/cbmc","forks_url":"https://api.github.com/repos/romainbrenguier/cbmc/forks","keys_url":"https://api.github.com/repos/romainbrenguier/cbmc/keys{/key_id}","collaborators_url":"https://api.github.com/repos/romainbrenguier/cbmc/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/romainbrenguier/cbmc/teams","hooks_url":"https://api.github.com/repos/romainbrenguier/cbmc/hooks","issue_events_url":"https://api.github.com/repos/romainbrenguier/cbmc/issues/events{/number}","events_url":"https://api.github.com/repos/romainbrenguier/cbmc/events","assignees_url":"https://api.github.com/repos/romainbrenguier/cbmc/assignees{/user}","branches_url":"https://api.github.com/repos/romainbrenguier/cbmc/branches{/branch}","tags_url":"https://api.github.com/repos/romainbrenguier/cbmc/tags","blobs_url":"https://api.github.com/repos/romainbrenguier/cbmc/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/romainbrenguier/cbmc/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/romainbrenguier/cbmc/git/refs{/sha}","trees_url":"https://api.github.com/repos/romainbrenguier/cbmc/git/trees{/sha}","statuses_url":"https://api.github.com/repos/romainbrenguier/cbmc/statuses/{sha}","languages_url":"https://api.github.com/repos/romainbrenguier/cbmc/languages","stargazers_url":"https://api.github.com/repos/romainbrenguier/cbmc/stargazers","contributors_url":"https://api.github.com/repos/romainbrenguier/cbmc/contributors","subscribers_url":"https://api.github.com/repos/romainbrenguier/cbmc/subscribers","subscription_url":"https://api.github.com/repos/romainbrenguier/cbmc/subscription","commits_url":"https://api.github.com/repos/romainbrenguier/cbmc/commits{/sha}","git_commits_url":"https://api.github.com/repos/romainbrenguier/cbmc/git/commits{/sha}","comments_url":"https://api.github.com/repos/romainbrenguier/cbmc/comments{/number}","issue_comment_url":"https://api.github.com/repos/romainbrenguier/cbmc/issues/comments{/number}","contents_url":"https://api.github.com/repos/romainbrenguier/cbmc/contents/{+path}","compare_url":"https://api.github.com/repos/romainbrenguier/cbmc/compare/{base}...{head}","merges_url":"https://api.github.com/repos/romainbrenguier/cbmc/merges","archive_url":"https://api.github.com/repos/romainbrenguier/cbmc/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/romainbrenguier/cbmc/downloads","issues_url":"https://api.github.com/repos/romainbrenguier/cbmc/issues{/number}","pulls_url":"https://api.github.com/repos/romainbrenguier/cbmc/pulls{/number}","milestones_url":"https://api.github.com/repos/romainbrenguier/cbmc/milestones{/number}","notifications_url":"https://api.github.com/repos/romainbrenguier/cbmc/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/romainbrenguier/cbmc/labels{/name}","releases_url":"https://api.github.com/repos/romainbrenguier/cbmc/releases{/id}","deployments_url":"https://api.github.com/repos/romainbrenguier/cbmc/deployments","created_at":"2016-08-02T14:57:13Z","updated_at":"2017-06-22T09:24:59Z","pushed_at":"2018-03-05T14:06:30Z","git_url":"git://github.com/romainbrenguier/cbmc.git","ssh_url":"git@github.com:romainbrenguier/cbmc.git","clone_url":"https://github.com/romainbrenguier/cbmc.git","svn_url":"https://github.com/romainbrenguier/cbmc","homepage":"http://www.cprover.org/cbmc","size":34740,"stargazers_count":0,"watchers_count":0,"language":"C++","has_issues":false,"has_projects":true,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":0,"mirror_url":null,"archived":false,"open_issues_count":1,"license":{"key":"other","name":"Other","spdx_id":null,"url":null},"forks":0,"open_issues":1,"watchers":0,"default_branch":"string-solver-experiments"}},"base":{"label":"diffblue:develop","ref":"develop","sha":"fe34bf6b64250f4b029d583a703e7ac51bd9a91d","user":{"login":"diffblue","id":17216098,"avatar_url":"https://avatars0.githubusercontent.com/u/17216098?v=4","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://avatars0.githubusercontent.com/u/17216098?v=4","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":"2018-02-26T12:21:45Z","pushed_at":"2018-03-06T14:45:10Z","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":28721,"stargazers_count":102,"watchers_count":102,"language":"C++","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":90,"mirror_url":null,"archived":false,"open_issues_count":314,"license":{"key":"other","name":"Other","spdx_id":null,"url":null},"forks":90,"open_issues":314,"watchers":102,"default_branch":"develop"}},"_links":{"self":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/1895"},"html":{"href":"https://github.com/diffblue/cbmc/pull/1895"},"issue":{"href":"https://api.github.com/repos/diffblue/cbmc/issues/1895"},"comments":{"href":"https://api.github.com/repos/diffblue/cbmc/issues/1895/comments"},"review_comments":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/1895/comments"},"review_comment":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/diffblue/cbmc/pulls/1895/commits"},"statuses":{"href":"https://api.github.com/repos/diffblue/cbmc/statuses/98ee2225ce7a6459879d810fdf3b9e4e65a98cbd"}},"author_association":"MEMBER"}}
{"actor":{"display_login":"romainbrenguier"}}