{"action":"created","comment":{"url":"https://api.github.com/repos/smackers/smack/pulls/comments/23719595","id":23719595,"diff_hunk":"@@ -766,28 +948,38 @@ string SmackRep::memcpyProc(int dstReg, int srcReg) {\n \n   if (SmackOptions::MemoryModelImpls) {\n     s << \"procedure $memcpy.\" << dstReg << \".\" << srcReg;\n-    s << \"(dest: int, src: int, len: int, align: int, isvolatile: bool)\" << endl;\n-    s << \"modifies \" << memReg(dstReg) << \";\" << endl;\n+    s << \"(dest: ref, src: ref, len: size, align: i32, isvolatile: bool)\" << endl;\n+    for (int i = 0; i < (SmackOptions::InferFieldOverlap? 4 : 1); ++i) {\n+      unsigned size = 8 << i;\n+      s << \"modifies \" << memPath(dstReg, size) << \";\" << endl;\n+    }\n+\n     s << \"{\" << endl;\n-    s << \"  var $oldSrc: [\" << getPtrType() << \"] \" << getPtrType() << \";\" << endl;\n-    s << \"  var $oldDst: [\" << getPtrType() << \"] \" << getPtrType() << \";\" << endl;\n-    s << \"  $oldSrc := \" << memReg(srcReg) << \";\" << endl;\n-    s << \"  $oldDst := \" << memReg(dstReg) << \";\" << endl;\n-    s << \"  havoc \" << memReg(dstReg) << \";\" << endl;\n-    s << \"  assume (forall x:int :: dest <= x && x < dest + len ==> \"\n-      << memReg(dstReg) << \"[x] == $oldSrc[src - dest + x]);\" << endl;\n-    s << \"  assume (forall x:int :: !(dest <= x && x < dest + len) ==> \"\n-      << memReg(dstReg) << \"[x] == $oldDst[x]);\" << endl;\n+    for (int i = 0; i < (SmackOptions::InferFieldOverlap? 4 : 1); ++i) {\n+      unsigned size = 8 << i;\n+      s << \"  var $oldSrc\" << \".i\" << size << \" : [\" << getPtrType() << \"] \" << int_type(size) << \";\" << endl;\n+      s << \"  var $oldDst\" << \".i\" << size << \" : [\" << getPtrType() << \"] \" << int_type(size) << \";\" << endl;\n+    }\n+    for (int i = 0; i < (SmackOptions::InferFieldOverlap? 4 : 1); ++i) {\n+      unsigned size = 8 << i;\n+      s << \"  $oldSrc\" << \".i\" << size << \" := \" << memPath(srcReg, size) << \";\" << endl;\n+      s << \"  $oldDst\" << \".i\" << size << \" := \" << memPath(dstReg, size) << \";\" << endl;\n+      s << \"  havoc \" << memPath(dstReg, size) << \";\" << endl;\n+      s << \"  assume (forall x:ref :: $ule.ref(dest, x) && $ult.ref(x, $add.ref(dest, len)) ==> \"\n+\t<< memPath(dstReg, size) << \"[x] == $oldSrc\" << \".i\" << size << \"[$add.ref($sub.ref(src, dest), x)]);\" << endl;\n+      s << \"  assume (forall x:ref :: !($ule.ref(dest, x) && $ult.ref(x, $add.ref(dest, len))) ==> \"\n+\t<< memPath(dstReg, size) << \"[x] == $oldDst\" << \".i\" << size << \"[x]);\" << endl;\n+    }\n     s << \"}\" << endl;\n   } else {\n-    s << \"procedure $memcpy.\" << dstReg << \".\" << srcReg;\n-    s << \"(dest: int, src: int, len: int, align: int, isvolatile: bool);\" << endl;\n-    s << \"modifies \" << memReg(dstReg) << \";\" << endl;\n-    s << \"ensures (forall x:int :: dest <= x && x < dest + len ==> \"\n-      << memReg(dstReg) << \"[x] == old(\" << memReg(srcReg) << \")[src - dest + x]);\" \n-      << endl;\n-    s << \"ensures (forall x:int :: !(dest <= x && x < dest + len) ==> \"\n-      << memReg(dstReg) << \"[x] == old(\" << memReg(dstReg) << \")[x]);\" << endl;\n+      s << \"procedure $memcpy.\" << dstReg << \".\" << srcReg;","path":"lib/smack/SmackRep.cpp","position":665,"original_position":665,"commit_id":"df75fdab6e3c3d87d392710b7e34883e0977b4db","original_commit_id":"df75fdab6e3c3d87d392710b7e34883e0977b4db","user":{"login":"michael-emmi","id":1457498,"avatar_url":"https://avatars.githubusercontent.com/u/1457498?v=3","gravatar_id":"","url":"https://api.github.com/users/michael-emmi","html_url":"https://github.com/michael-emmi","followers_url":"https://api.github.com/users/michael-emmi/followers","following_url":"https://api.github.com/users/michael-emmi/following{/other_user}","gists_url":"https://api.github.com/users/michael-emmi/gists{/gist_id}","starred_url":"https://api.github.com/users/michael-emmi/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/michael-emmi/subscriptions","organizations_url":"https://api.github.com/users/michael-emmi/orgs","repos_url":"https://api.github.com/users/michael-emmi/repos","events_url":"https://api.github.com/users/michael-emmi/events{/privacy}","received_events_url":"https://api.github.com/users/michael-emmi/received_events","type":"User","site_admin":false},"body":"Extra column space should not be added.","created_at":"2015-01-28T20:18:30Z","updated_at":"2015-01-28T20:18:30Z","html_url":"https://github.com/smackers/smack/pull/56#discussion_r23719595","pull_request_url":"https://api.github.com/repos/smackers/smack/pulls/56","_links":{"self":{"href":"https://api.github.com/repos/smackers/smack/pulls/comments/23719595"},"html":{"href":"https://github.com/smackers/smack/pull/56#discussion_r23719595"},"pull_request":{"href":"https://api.github.com/repos/smackers/smack/pulls/56"}}},"pull_request":{"url":"https://api.github.com/repos/smackers/smack/pulls/56","id":26634159,"html_url":"https://github.com/smackers/smack/pull/56","diff_url":"https://github.com/smackers/smack/pull/56.diff","patch_url":"https://github.com/smackers/smack/pull/56.patch","issue_url":"https://api.github.com/repos/smackers/smack/issues/56","number":56,"state":"open","locked":false,"title":"Bit-vector extension for SMACK","user":{"login":"Guoanshisb","id":5892703,"avatar_url":"https://avatars.githubusercontent.com/u/5892703?v=3","gravatar_id":"","url":"https://api.github.com/users/Guoanshisb","html_url":"https://github.com/Guoanshisb","followers_url":"https://api.github.com/users/Guoanshisb/followers","following_url":"https://api.github.com/users/Guoanshisb/following{/other_user}","gists_url":"https://api.github.com/users/Guoanshisb/gists{/gist_id}","starred_url":"https://api.github.com/users/Guoanshisb/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Guoanshisb/subscriptions","organizations_url":"https://api.github.com/users/Guoanshisb/orgs","repos_url":"https://api.github.com/users/Guoanshisb/repos","events_url":"https://api.github.com/users/Guoanshisb/events{/privacy}","received_events_url":"https://api.github.com/users/Guoanshisb/received_events","type":"User","site_admin":false},"body":"Please help me improve the code :)\r\n\r\nShaobo","created_at":"2014-12-29T07:11:11Z","updated_at":"2015-01-28T20:18:30Z","closed_at":null,"merged_at":null,"merge_commit_sha":null,"assignee":null,"milestone":null,"commits_url":"https://api.github.com/repos/smackers/smack/pulls/56/commits","review_comments_url":"https://api.github.com/repos/smackers/smack/pulls/56/comments","review_comment_url":"https://api.github.com/repos/smackers/smack/pulls/comments/{number}","comments_url":"https://api.github.com/repos/smackers/smack/issues/56/comments","statuses_url":"https://api.github.com/repos/smackers/smack/statuses/df75fdab6e3c3d87d392710b7e34883e0977b4db","head":{"label":"smackers:bitvector","ref":"bitvector","sha":"df75fdab6e3c3d87d392710b7e34883e0977b4db","user":{"login":"smackers","id":3064612,"avatar_url":"https://avatars.githubusercontent.com/u/3064612?v=3","gravatar_id":"","url":"https://api.github.com/users/smackers","html_url":"https://github.com/smackers","followers_url":"https://api.github.com/users/smackers/followers","following_url":"https://api.github.com/users/smackers/following{/other_user}","gists_url":"https://api.github.com/users/smackers/gists{/gist_id}","starred_url":"https://api.github.com/users/smackers/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/smackers/subscriptions","organizations_url":"https://api.github.com/users/smackers/orgs","repos_url":"https://api.github.com/users/smackers/repos","events_url":"https://api.github.com/users/smackers/events{/privacy}","received_events_url":"https://api.github.com/users/smackers/received_events","type":"Organization","site_admin":false},"repo":{"id":5234086,"name":"smack","full_name":"smackers/smack","owner":{"login":"smackers","id":3064612,"avatar_url":"https://avatars.githubusercontent.com/u/3064612?v=3","gravatar_id":"","url":"https://api.github.com/users/smackers","html_url":"https://github.com/smackers","followers_url":"https://api.github.com/users/smackers/followers","following_url":"https://api.github.com/users/smackers/following{/other_user}","gists_url":"https://api.github.com/users/smackers/gists{/gist_id}","starred_url":"https://api.github.com/users/smackers/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/smackers/subscriptions","organizations_url":"https://api.github.com/users/smackers/orgs","repos_url":"https://api.github.com/users/smackers/repos","events_url":"https://api.github.com/users/smackers/events{/privacy}","received_events_url":"https://api.github.com/users/smackers/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/smackers/smack","description":"SMACK: A Modular Software Verification Infrastructure","fork":false,"url":"https://api.github.com/repos/smackers/smack","forks_url":"https://api.github.com/repos/smackers/smack/forks","keys_url":"https://api.github.com/repos/smackers/smack/keys{/key_id}","collaborators_url":"https://api.github.com/repos/smackers/smack/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/smackers/smack/teams","hooks_url":"https://api.github.com/repos/smackers/smack/hooks","issue_events_url":"https://api.github.com/repos/smackers/smack/issues/events{/number}","events_url":"https://api.github.com/repos/smackers/smack/events","assignees_url":"https://api.github.com/repos/smackers/smack/assignees{/user}","branches_url":"https://api.github.com/repos/smackers/smack/branches{/branch}","tags_url":"https://api.github.com/repos/smackers/smack/tags","blobs_url":"https://api.github.com/repos/smackers/smack/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/smackers/smack/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/smackers/smack/git/refs{/sha}","trees_url":"https://api.github.com/repos/smackers/smack/git/trees{/sha}","statuses_url":"https://api.github.com/repos/smackers/smack/statuses/{sha}","languages_url":"https://api.github.com/repos/smackers/smack/languages","stargazers_url":"https://api.github.com/repos/smackers/smack/stargazers","contributors_url":"https://api.github.com/repos/smackers/smack/contributors","subscribers_url":"https://api.github.com/repos/smackers/smack/subscribers","subscription_url":"https://api.github.com/repos/smackers/smack/subscription","commits_url":"https://api.github.com/repos/smackers/smack/commits{/sha}","git_commits_url":"https://api.github.com/repos/smackers/smack/git/commits{/sha}","comments_url":"https://api.github.com/repos/smackers/smack/comments{/number}","issue_comment_url":"https://api.github.com/repos/smackers/smack/issues/comments/{number}","contents_url":"https://api.github.com/repos/smackers/smack/contents/{+path}","compare_url":"https://api.github.com/repos/smackers/smack/compare/{base}...{head}","merges_url":"https://api.github.com/repos/smackers/smack/merges","archive_url":"https://api.github.com/repos/smackers/smack/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/smackers/smack/downloads","issues_url":"https://api.github.com/repos/smackers/smack/issues{/number}","pulls_url":"https://api.github.com/repos/smackers/smack/pulls{/number}","milestones_url":"https://api.github.com/repos/smackers/smack/milestones{/number}","notifications_url":"https://api.github.com/repos/smackers/smack/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/smackers/smack/labels{/name}","releases_url":"https://api.github.com/repos/smackers/smack/releases{/id}","created_at":"2012-07-30T15:32:57Z","updated_at":"2015-01-08T13:41:38Z","pushed_at":"2015-01-28T19:22:43Z","git_url":"git://github.com/smackers/smack.git","ssh_url":"git@github.com:smackers/smack.git","clone_url":"https://github.com/smackers/smack.git","svn_url":"https://github.com/smackers/smack","homepage":"","size":4858,"stargazers_count":75,"watchers_count":75,"language":"C","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":6,"mirror_url":null,"open_issues_count":15,"forks":6,"open_issues":15,"watchers":75,"default_branch":"master"}},"base":{"label":"smackers:develop","ref":"develop","sha":"f4c68b1fa05b297a2cb8fb78ed54c69a507d34d8","user":{"login":"smackers","id":3064612,"avatar_url":"https://avatars.githubusercontent.com/u/3064612?v=3","gravatar_id":"","url":"https://api.github.com/users/smackers","html_url":"https://github.com/smackers","followers_url":"https://api.github.com/users/smackers/followers","following_url":"https://api.github.com/users/smackers/following{/other_user}","gists_url":"https://api.github.com/users/smackers/gists{/gist_id}","starred_url":"https://api.github.com/users/smackers/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/smackers/subscriptions","organizations_url":"https://api.github.com/users/smackers/orgs","repos_url":"https://api.github.com/users/smackers/repos","events_url":"https://api.github.com/users/smackers/events{/privacy}","received_events_url":"https://api.github.com/users/smackers/received_events","type":"Organization","site_admin":false},"repo":{"id":5234086,"name":"smack","full_name":"smackers/smack","owner":{"login":"smackers","id":3064612,"avatar_url":"https://avatars.githubusercontent.com/u/3064612?v=3","gravatar_id":"","url":"https://api.github.com/users/smackers","html_url":"https://github.com/smackers","followers_url":"https://api.github.com/users/smackers/followers","following_url":"https://api.github.com/users/smackers/following{/other_user}","gists_url":"https://api.github.com/users/smackers/gists{/gist_id}","starred_url":"https://api.github.com/users/smackers/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/smackers/subscriptions","organizations_url":"https://api.github.com/users/smackers/orgs","repos_url":"https://api.github.com/users/smackers/repos","events_url":"https://api.github.com/users/smackers/events{/privacy}","received_events_url":"https://api.github.com/users/smackers/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/smackers/smack","description":"SMACK: A Modular Software Verification Infrastructure","fork":false,"url":"https://api.github.com/repos/smackers/smack","forks_url":"https://api.github.com/repos/smackers/smack/forks","keys_url":"https://api.github.com/repos/smackers/smack/keys{/key_id}","collaborators_url":"https://api.github.com/repos/smackers/smack/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/smackers/smack/teams","hooks_url":"https://api.github.com/repos/smackers/smack/hooks","issue_events_url":"https://api.github.com/repos/smackers/smack/issues/events{/number}","events_url":"https://api.github.com/repos/smackers/smack/events","assignees_url":"https://api.github.com/repos/smackers/smack/assignees{/user}","branches_url":"https://api.github.com/repos/smackers/smack/branches{/branch}","tags_url":"https://api.github.com/repos/smackers/smack/tags","blobs_url":"https://api.github.com/repos/smackers/smack/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/smackers/smack/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/smackers/smack/git/refs{/sha}","trees_url":"https://api.github.com/repos/smackers/smack/git/trees{/sha}","statuses_url":"https://api.github.com/repos/smackers/smack/statuses/{sha}","languages_url":"https://api.github.com/repos/smackers/smack/languages","stargazers_url":"https://api.github.com/repos/smackers/smack/stargazers","contributors_url":"https://api.github.com/repos/smackers/smack/contributors","subscribers_url":"https://api.github.com/repos/smackers/smack/subscribers","subscription_url":"https://api.github.com/repos/smackers/smack/subscription","commits_url":"https://api.github.com/repos/smackers/smack/commits{/sha}","git_commits_url":"https://api.github.com/repos/smackers/smack/git/commits{/sha}","comments_url":"https://api.github.com/repos/smackers/smack/comments{/number}","issue_comment_url":"https://api.github.com/repos/smackers/smack/issues/comments/{number}","contents_url":"https://api.github.com/repos/smackers/smack/contents/{+path}","compare_url":"https://api.github.com/repos/smackers/smack/compare/{base}...{head}","merges_url":"https://api.github.com/repos/smackers/smack/merges","archive_url":"https://api.github.com/repos/smackers/smack/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/smackers/smack/downloads","issues_url":"https://api.github.com/repos/smackers/smack/issues{/number}","pulls_url":"https://api.github.com/repos/smackers/smack/pulls{/number}","milestones_url":"https://api.github.com/repos/smackers/smack/milestones{/number}","notifications_url":"https://api.github.com/repos/smackers/smack/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/smackers/smack/labels{/name}","releases_url":"https://api.github.com/repos/smackers/smack/releases{/id}","created_at":"2012-07-30T15:32:57Z","updated_at":"2015-01-08T13:41:38Z","pushed_at":"2015-01-28T19:22:43Z","git_url":"git://github.com/smackers/smack.git","ssh_url":"git@github.com:smackers/smack.git","clone_url":"https://github.com/smackers/smack.git","svn_url":"https://github.com/smackers/smack","homepage":"","size":4858,"stargazers_count":75,"watchers_count":75,"language":"C","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":6,"mirror_url":null,"open_issues_count":15,"forks":6,"open_issues":15,"watchers":75,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/smackers/smack/pulls/56"},"html":{"href":"https://github.com/smackers/smack/pull/56"},"issue":{"href":"https://api.github.com/repos/smackers/smack/issues/56"},"comments":{"href":"https://api.github.com/repos/smackers/smack/issues/56/comments"},"review_comments":{"href":"https://api.github.com/repos/smackers/smack/pulls/56/comments"},"review_comment":{"href":"https://api.github.com/repos/smackers/smack/pulls/comments/{number}"},"commits":{"href":"https://api.github.com/repos/smackers/smack/pulls/56/commits"},"statuses":{"href":"https://api.github.com/repos/smackers/smack/statuses/df75fdab6e3c3d87d392710b7e34883e0977b4db"}}}}