{"action":"created","comment":{"url":"https://api.github.com/repos/epfl-lara/stainless/pulls/comments/225895729","pull_request_review_id":165592613,"id":225895729,"node_id":"MDI0OlB1bGxSZXF1ZXN0UmV2aWV3Q29tbWVudDIyNTg5NTcyOQ==","diff_hunk":"@@ -0,0 +1,286 @@\n+/* Copyright 2009-2018 EPFL, Lausanne */\n+\n+package stainless\n+package extraction\n+package methods\n+\n+import scala.language.existentials\n+\n+trait Sealing extends oo.CachingPhase\n+  with IdentitySorts\n+  with MutabilityAnalyzer { self =>\n+\n+\n+  /* ====================================\n+   *       Context and caches setup\n+   * ==================================== */\n+\n+  import s._\n+  import s.exprOps._\n+\n+  protected class TransformerContext(implicit symbols: Symbols) extends MutabilityAnalysis()(symbols) {\n+    def mustDuplicate(fd: FunDef): Boolean = {\n+      !fd.isAbstract &&\n+      !fd.isFinal &&\n+      !fd.isAccessor &&\n+      !fd.isField &&","path":"core/src/main/scala/stainless/extraction/methods/Sealing.scala","position":26,"original_position":26,"commit_id":"5bf62690b09e0f849419c811869a9c6af004d3ab","original_commit_id":"5bf62690b09e0f849419c811869a9c6af004d3ab","user":{"login":"jad-hamza","id":2743954,"node_id":"MDQ6VXNlcjI3NDM5NTQ=","avatar_url":"https://avatars0.githubusercontent.com/u/2743954?v=4","gravatar_id":"","url":"https://api.github.com/users/jad-hamza","html_url":"https://github.com/jad-hamza","followers_url":"https://api.github.com/users/jad-hamza/followers","following_url":"https://api.github.com/users/jad-hamza/following{/other_user}","gists_url":"https://api.github.com/users/jad-hamza/gists{/gist_id}","starred_url":"https://api.github.com/users/jad-hamza/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jad-hamza/subscriptions","organizations_url":"https://api.github.com/users/jad-hamza/orgs","repos_url":"https://api.github.com/users/jad-hamza/repos","events_url":"https://api.github.com/users/jad-hamza/events{/privacy}","received_events_url":"https://api.github.com/users/jad-hamza/received_events","type":"User","site_admin":false},"body":"The definitions of `isSetter` and `isGetter` also take into account `isField`, should that not be the case? This was merged in my last pull request:\r\nhttps://github.com/epfl-lara/stainless/blob/76f641ce6d475c8a2f375139f5541b0a46c1a901/core/src/main/scala/stainless/extraction/methods/Trees.scala#L163-L166","created_at":"2018-10-17T12:04:31Z","updated_at":"2018-10-17T12:04:31Z","html_url":"https://github.com/epfl-lara/stainless/pull/370#discussion_r225895729","pull_request_url":"https://api.github.com/repos/epfl-lara/stainless/pulls/370","author_association":"COLLABORATOR","_links":{"self":{"href":"https://api.github.com/repos/epfl-lara/stainless/pulls/comments/225895729"},"html":{"href":"https://github.com/epfl-lara/stainless/pull/370#discussion_r225895729"},"pull_request":{"href":"https://api.github.com/repos/epfl-lara/stainless/pulls/370"}},"in_reply_to_id":225829419},"pull_request":{"url":"https://api.github.com/repos/epfl-lara/stainless/pulls/370","id":220939333,"node_id":"MDExOlB1bGxSZXF1ZXN0MjIwOTM5MzMz","html_url":"https://github.com/epfl-lara/stainless/pull/370","diff_url":"https://github.com/epfl-lara/stainless/pull/370.diff","patch_url":"https://github.com/epfl-lara/stainless/pull/370.patch","issue_url":"https://api.github.com/repos/epfl-lara/stainless/issues/370","number":370,"state":"open","locked":false,"title":"Sealing phase","user":{"login":"jad-hamza","id":2743954,"node_id":"MDQ6VXNlcjI3NDM5NTQ=","avatar_url":"https://avatars0.githubusercontent.com/u/2743954?v=4","gravatar_id":"","url":"https://api.github.com/users/jad-hamza","html_url":"https://github.com/jad-hamza","followers_url":"https://api.github.com/users/jad-hamza/followers","following_url":"https://api.github.com/users/jad-hamza/following{/other_user}","gists_url":"https://api.github.com/users/jad-hamza/gists{/gist_id}","starred_url":"https://api.github.com/users/jad-hamza/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jad-hamza/subscriptions","organizations_url":"https://api.github.com/users/jad-hamza/orgs","repos_url":"https://api.github.com/users/jad-hamza/repos","events_url":"https://api.github.com/users/jad-hamza/events{/privacy}","received_events_url":"https://api.github.com/users/jad-hamza/received_events","type":"User","site_admin":false},"body":"### Sealing\r\n\r\n* For every abstract and non-sealed class, we add a dummy subclass\r\n* The dummy subclass preserves the mutability flag of the superclass\r\n* The dummy subclass gets a dummy val or a dummy var depending on the mutable flag\r\n* Every non-final and non-invariant and non-accessor method gets overridden by an @extern method with an empty body in the new subclass \r\n* Every accessor gets a field in the subclass with concrete setters and getters\r\n* In non-sealed classes, concrete methods which are not accessors/fields/invariants get duplicated so that their bodies survives the pipeline (`MethodLifting` for instance) if they contain code that must generates verification conditions.\r\n\r\n### EffectsAnalyzer\r\n\r\n* Every non-pure annotated method with no-body has effect on every variable\r\n* Change `isMutableType` for sorts to just lookup the mutable flag instead of looking for vars\r\n\r\n### MethodLifting\r\n\r\n* Add `ClassKey` to `classCache` to avoid corrupt cache\r\n\r\n### ensureWellFormed\r\n\r\n* `isAbstract` now just looks up the abstract flag (an extern method with no body is no longer considered abstract)\r\n* Ensure that final methods are not overridden\r\n* Ensure that concrete classes are not extended\r\n* Ensure that setters only appear in mutable classes\r\n\r\n### AdtSpecialization\r\n\r\n* Remove the code that adds \"Open\" subclasses\r\n\r\n### TypeEncoding\r\n\r\n* The code that adds \"Open\" subclasses is still there. Otherwise `Object` has sometimes no children.\r\n\r\n### Supercalls\r\n\r\n* Fix `funCache` by adding ValueKey with the `context.mustDuplicate(fd)` boolean \r\n* Removed `IsAbstract` flag when creating a copy of a method, since the copy won't get overridden\r\n\r\n### Laws\r\n\r\n* Add `LawProp` flag to the `$prop` methods that are generated to prevent them from being overridden in the Sealing phase\r\n\r\n### Benchmarks\r\n\r\n* Added new benchmarks and fixed some benchmarks\r\n\r\n### ImperativeCleanup\r\n\r\n* Remove imperative flags when transforming sorts\r\n\r\n### GhostRewriteSuite\r\n\r\n* Ignore exhaustiveness checks in `GhostRewriteSuite` (for some reason this is not needed in the current master?)\r\n","created_at":"2018-10-07T10:24:19Z","updated_at":"2018-10-17T12:04:31Z","closed_at":null,"merged_at":null,"merge_commit_sha":"3e4eef9a9c6d988b08757f09e71ddd3f838c65d6","assignee":null,"assignees":[],"requested_reviewers":[],"requested_teams":[],"labels":[{"id":1002339820,"node_id":"MDU6TGFiZWwxMDAyMzM5ODIw","url":"https://api.github.com/repos/epfl-lara/stainless/labels/in%20progress","name":"in progress","color":"fbca04","default":false}],"milestone":null,"commits_url":"https://api.github.com/repos/epfl-lara/stainless/pulls/370/commits","review_comments_url":"https://api.github.com/repos/epfl-lara/stainless/pulls/370/comments","review_comment_url":"https://api.github.com/repos/epfl-lara/stainless/pulls/comments{/number}","comments_url":"https://api.github.com/repos/epfl-lara/stainless/issues/370/comments","statuses_url":"https://api.github.com/repos/epfl-lara/stainless/statuses/5bf62690b09e0f849419c811869a9c6af004d3ab","head":{"label":"jad-hamza:sealing-phase","ref":"sealing-phase","sha":"5bf62690b09e0f849419c811869a9c6af004d3ab","user":{"login":"jad-hamza","id":2743954,"node_id":"MDQ6VXNlcjI3NDM5NTQ=","avatar_url":"https://avatars0.githubusercontent.com/u/2743954?v=4","gravatar_id":"","url":"https://api.github.com/users/jad-hamza","html_url":"https://github.com/jad-hamza","followers_url":"https://api.github.com/users/jad-hamza/followers","following_url":"https://api.github.com/users/jad-hamza/following{/other_user}","gists_url":"https://api.github.com/users/jad-hamza/gists{/gist_id}","starred_url":"https://api.github.com/users/jad-hamza/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jad-hamza/subscriptions","organizations_url":"https://api.github.com/users/jad-hamza/orgs","repos_url":"https://api.github.com/users/jad-hamza/repos","events_url":"https://api.github.com/users/jad-hamza/events{/privacy}","received_events_url":"https://api.github.com/users/jad-hamza/received_events","type":"User","site_admin":false},"repo":{"id":87923771,"node_id":"MDEwOlJlcG9zaXRvcnk4NzkyMzc3MQ==","name":"stainless","full_name":"jad-hamza/stainless","private":false,"owner":{"login":"jad-hamza","id":2743954,"node_id":"MDQ6VXNlcjI3NDM5NTQ=","avatar_url":"https://avatars0.githubusercontent.com/u/2743954?v=4","gravatar_id":"","url":"https://api.github.com/users/jad-hamza","html_url":"https://github.com/jad-hamza","followers_url":"https://api.github.com/users/jad-hamza/followers","following_url":"https://api.github.com/users/jad-hamza/following{/other_user}","gists_url":"https://api.github.com/users/jad-hamza/gists{/gist_id}","starred_url":"https://api.github.com/users/jad-hamza/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jad-hamza/subscriptions","organizations_url":"https://api.github.com/users/jad-hamza/orgs","repos_url":"https://api.github.com/users/jad-hamza/repos","events_url":"https://api.github.com/users/jad-hamza/events{/privacy}","received_events_url":"https://api.github.com/users/jad-hamza/received_events","type":"User","site_admin":false},"html_url":"https://github.com/jad-hamza/stainless","description":"Verification framework for higher-order functional programs","fork":true,"url":"https://api.github.com/repos/jad-hamza/stainless","forks_url":"https://api.github.com/repos/jad-hamza/stainless/forks","keys_url":"https://api.github.com/repos/jad-hamza/stainless/keys{/key_id}","collaborators_url":"https://api.github.com/repos/jad-hamza/stainless/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/jad-hamza/stainless/teams","hooks_url":"https://api.github.com/repos/jad-hamza/stainless/hooks","issue_events_url":"https://api.github.com/repos/jad-hamza/stainless/issues/events{/number}","events_url":"https://api.github.com/repos/jad-hamza/stainless/events","assignees_url":"https://api.github.com/repos/jad-hamza/stainless/assignees{/user}","branches_url":"https://api.github.com/repos/jad-hamza/stainless/branches{/branch}","tags_url":"https://api.github.com/repos/jad-hamza/stainless/tags","blobs_url":"https://api.github.com/repos/jad-hamza/stainless/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/jad-hamza/stainless/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/jad-hamza/stainless/git/refs{/sha}","trees_url":"https://api.github.com/repos/jad-hamza/stainless/git/trees{/sha}","statuses_url":"https://api.github.com/repos/jad-hamza/stainless/statuses/{sha}","languages_url":"https://api.github.com/repos/jad-hamza/stainless/languages","stargazers_url":"https://api.github.com/repos/jad-hamza/stainless/stargazers","contributors_url":"https://api.github.com/repos/jad-hamza/stainless/contributors","subscribers_url":"https://api.github.com/repos/jad-hamza/stainless/subscribers","subscription_url":"https://api.github.com/repos/jad-hamza/stainless/subscription","commits_url":"https://api.github.com/repos/jad-hamza/stainless/commits{/sha}","git_commits_url":"https://api.github.com/repos/jad-hamza/stainless/git/commits{/sha}","comments_url":"https://api.github.com/repos/jad-hamza/stainless/comments{/number}","issue_comment_url":"https://api.github.com/repos/jad-hamza/stainless/issues/comments{/number}","contents_url":"https://api.github.com/repos/jad-hamza/stainless/contents/{+path}","compare_url":"https://api.github.com/repos/jad-hamza/stainless/compare/{base}...{head}","merges_url":"https://api.github.com/repos/jad-hamza/stainless/merges","archive_url":"https://api.github.com/repos/jad-hamza/stainless/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/jad-hamza/stainless/downloads","issues_url":"https://api.github.com/repos/jad-hamza/stainless/issues{/number}","pulls_url":"https://api.github.com/repos/jad-hamza/stainless/pulls{/number}","milestones_url":"https://api.github.com/repos/jad-hamza/stainless/milestones{/number}","notifications_url":"https://api.github.com/repos/jad-hamza/stainless/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/jad-hamza/stainless/labels{/name}","releases_url":"https://api.github.com/repos/jad-hamza/stainless/releases{/id}","deployments_url":"https://api.github.com/repos/jad-hamza/stainless/deployments","created_at":"2017-04-11T10:57:58Z","updated_at":"2018-10-17T08:06:15Z","pushed_at":"2018-10-17T11:49:32Z","git_url":"git://github.com/jad-hamza/stainless.git","ssh_url":"git@github.com:jad-hamza/stainless.git","clone_url":"https://github.com/jad-hamza/stainless.git","svn_url":"https://github.com/jad-hamza/stainless","homepage":null,"size":58951,"stargazers_count":1,"watchers_count":1,"language":"Scala","has_issues":false,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":1,"mirror_url":null,"archived":false,"open_issues_count":0,"license":{"key":"agpl-3.0","name":"GNU Affero General Public License v3.0","spdx_id":"AGPL-3.0","url":"https://api.github.com/licenses/agpl-3.0","node_id":"MDc6TGljZW5zZTE="},"forks":1,"open_issues":0,"watchers":1,"default_branch":"master"}},"base":{"label":"epfl-lara:master","ref":"master","sha":"76f641ce6d475c8a2f375139f5541b0a46c1a901","user":{"login":"epfl-lara","id":3035238,"node_id":"MDEyOk9yZ2FuaXphdGlvbjMwMzUyMzg=","avatar_url":"https://avatars1.githubusercontent.com/u/3035238?v=4","gravatar_id":"","url":"https://api.github.com/users/epfl-lara","html_url":"https://github.com/epfl-lara","followers_url":"https://api.github.com/users/epfl-lara/followers","following_url":"https://api.github.com/users/epfl-lara/following{/other_user}","gists_url":"https://api.github.com/users/epfl-lara/gists{/gist_id}","starred_url":"https://api.github.com/users/epfl-lara/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/epfl-lara/subscriptions","organizations_url":"https://api.github.com/users/epfl-lara/orgs","repos_url":"https://api.github.com/users/epfl-lara/repos","events_url":"https://api.github.com/users/epfl-lara/events{/privacy}","received_events_url":"https://api.github.com/users/epfl-lara/received_events","type":"Organization","site_admin":false},"repo":{"id":65912716,"node_id":"MDEwOlJlcG9zaXRvcnk2NTkxMjcxNg==","name":"stainless","full_name":"epfl-lara/stainless","private":false,"owner":{"login":"epfl-lara","id":3035238,"node_id":"MDEyOk9yZ2FuaXphdGlvbjMwMzUyMzg=","avatar_url":"https://avatars1.githubusercontent.com/u/3035238?v=4","gravatar_id":"","url":"https://api.github.com/users/epfl-lara","html_url":"https://github.com/epfl-lara","followers_url":"https://api.github.com/users/epfl-lara/followers","following_url":"https://api.github.com/users/epfl-lara/following{/other_user}","gists_url":"https://api.github.com/users/epfl-lara/gists{/gist_id}","starred_url":"https://api.github.com/users/epfl-lara/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/epfl-lara/subscriptions","organizations_url":"https://api.github.com/users/epfl-lara/orgs","repos_url":"https://api.github.com/users/epfl-lara/repos","events_url":"https://api.github.com/users/epfl-lara/events{/privacy}","received_events_url":"https://api.github.com/users/epfl-lara/received_events","type":"Organization","site_admin":false},"html_url":"https://github.com/epfl-lara/stainless","description":"Verification framework for higher-order functional programs","fork":false,"url":"https://api.github.com/repos/epfl-lara/stainless","forks_url":"https://api.github.com/repos/epfl-lara/stainless/forks","keys_url":"https://api.github.com/repos/epfl-lara/stainless/keys{/key_id}","collaborators_url":"https://api.github.com/repos/epfl-lara/stainless/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/epfl-lara/stainless/teams","hooks_url":"https://api.github.com/repos/epfl-lara/stainless/hooks","issue_events_url":"https://api.github.com/repos/epfl-lara/stainless/issues/events{/number}","events_url":"https://api.github.com/repos/epfl-lara/stainless/events","assignees_url":"https://api.github.com/repos/epfl-lara/stainless/assignees{/user}","branches_url":"https://api.github.com/repos/epfl-lara/stainless/branches{/branch}","tags_url":"https://api.github.com/repos/epfl-lara/stainless/tags","blobs_url":"https://api.github.com/repos/epfl-lara/stainless/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/epfl-lara/stainless/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/epfl-lara/stainless/git/refs{/sha}","trees_url":"https://api.github.com/repos/epfl-lara/stainless/git/trees{/sha}","statuses_url":"https://api.github.com/repos/epfl-lara/stainless/statuses/{sha}","languages_url":"https://api.github.com/repos/epfl-lara/stainless/languages","stargazers_url":"https://api.github.com/repos/epfl-lara/stainless/stargazers","contributors_url":"https://api.github.com/repos/epfl-lara/stainless/contributors","subscribers_url":"https://api.github.com/repos/epfl-lara/stainless/subscribers","subscription_url":"https://api.github.com/repos/epfl-lara/stainless/subscription","commits_url":"https://api.github.com/repos/epfl-lara/stainless/commits{/sha}","git_commits_url":"https://api.github.com/repos/epfl-lara/stainless/git/commits{/sha}","comments_url":"https://api.github.com/repos/epfl-lara/stainless/comments{/number}","issue_comment_url":"https://api.github.com/repos/epfl-lara/stainless/issues/comments{/number}","contents_url":"https://api.github.com/repos/epfl-lara/stainless/contents/{+path}","compare_url":"https://api.github.com/repos/epfl-lara/stainless/compare/{base}...{head}","merges_url":"https://api.github.com/repos/epfl-lara/stainless/merges","archive_url":"https://api.github.com/repos/epfl-lara/stainless/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/epfl-lara/stainless/downloads","issues_url":"https://api.github.com/repos/epfl-lara/stainless/issues{/number}","pulls_url":"https://api.github.com/repos/epfl-lara/stainless/pulls{/number}","milestones_url":"https://api.github.com/repos/epfl-lara/stainless/milestones{/number}","notifications_url":"https://api.github.com/repos/epfl-lara/stainless/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/epfl-lara/stainless/labels{/name}","releases_url":"https://api.github.com/repos/epfl-lara/stainless/releases{/id}","deployments_url":"https://api.github.com/repos/epfl-lara/stainless/deployments","created_at":"2016-08-17T14:08:38Z","updated_at":"2018-10-17T08:04:59Z","pushed_at":"2018-10-17T11:34:04Z","git_url":"git://github.com/epfl-lara/stainless.git","ssh_url":"git@github.com:epfl-lara/stainless.git","clone_url":"https://github.com/epfl-lara/stainless.git","svn_url":"https://github.com/epfl-lara/stainless","homepage":null,"size":58801,"stargazers_count":125,"watchers_count":125,"language":"Scala","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":true,"forks_count":26,"mirror_url":null,"archived":false,"open_issues_count":43,"license":{"key":"agpl-3.0","name":"GNU Affero General Public License v3.0","spdx_id":"AGPL-3.0","url":"https://api.github.com/licenses/agpl-3.0","node_id":"MDc6TGljZW5zZTE="},"forks":26,"open_issues":43,"watchers":125,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/epfl-lara/stainless/pulls/370"},"html":{"href":"https://github.com/epfl-lara/stainless/pull/370"},"issue":{"href":"https://api.github.com/repos/epfl-lara/stainless/issues/370"},"comments":{"href":"https://api.github.com/repos/epfl-lara/stainless/issues/370/comments"},"review_comments":{"href":"https://api.github.com/repos/epfl-lara/stainless/pulls/370/comments"},"review_comment":{"href":"https://api.github.com/repos/epfl-lara/stainless/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/epfl-lara/stainless/pulls/370/commits"},"statuses":{"href":"https://api.github.com/repos/epfl-lara/stainless/statuses/5bf62690b09e0f849419c811869a9c6af004d3ab"}},"author_association":"COLLABORATOR"}}
{"actor":{"display_login":"jad-hamza"}}