Skip to content
Navigation Menu
Sign in
Products
Platform
GitHub
Repository hosting, code review, and collaboration
Copilot
AI coding agent for tasks, projects, and automated work
Build & Ship
Actions
CI/CD and automation
Code Quality
Quality analysis, fixes, and enforcement
Codespaces
Cloud development environments
Secure
Code Security
Vulnerability detection and remediation
Secret Protection
Secret scanning and leak prevention
All Features
Developers
Learn
Documentation
Training
Certifications
Build
Build with Copilot
Customize Copilot
Integrations
Explore
Trending repos
GitHub Sponsors
Developer articles
Changelog
Changelog
Your source for the latest features, improvements, and fixes across GitHub products, all in one place.
Businesses
By Stage
Enterprises
Team
Startups
Nonprofits
By Industry
Healthcare
Financial services
Manufacturing
Government
See all industries
Evaluate GitHub
Why GitHub
Customer Stories
Business insights
Trust Center
Add-ons
GitHub Advanced Security
Enterprise-grade code security
Copilot for business
Enterprise-grade AI features
Premium Support
Enterprise-grade 24/7 support
Resources
Learn & Connect
Documentation
Resource center
Blog
Events & webinars
Community Forum
Customer Stories
Integrations
Support
Customer support
Training
GitHub Status
Company
About
Partners
Changelog
GitHub Universe
GitHub Universe
The event for developers, by developers — talks, workshops, and what’s next for GitHub.
Pricing
Search
/
Sign in
Sign up
Appearance settings
You signed in with another tab or window.
Reload
to refresh your session.
You signed out in another tab or window.
Reload
to refresh your session.
You switched accounts on another tab or window.
Reload
to refresh your session.
Dismiss alert
{{ message }}
SwayamInSync
cpp-verify
Repository navigation
Code
Issues
Pull requests
7
(7)
Actions
Projects
Security and quality
Insights
More
items
Global records and arrays
- #127
#127
Merged
SwayamInSync
merged 21 commits into
main
SwayamInSync/cpp-verify:main
from
fix/global-objects
SwayamInSync/cpp-verify:fix/global-objects
Copy head branch name to clipboard
Oct 29, 2026
Conversation
Commits
21
(21)
Checks
Files changed
Merged
Global records and arrays
#127
SwayamInSync
merged 21 commits into
main
SwayamInSync/cpp-verify:main
from
fix/global-objects
SwayamInSync/cpp-verify:fix/global-objects
Copy head branch name to clipboard
Commits
Commits on Oct 28, 2026
verify: Declare global objects, their roots, and their places.
SwayamInSync
committed
b28c7cb
View commit details
Copy full SHA for b28c7cb
Browse repository at this point
verify: Read, write, and point into global records and arrays through places at their addresses.
SwayamInSync
committed
1afeed2
View commit details
Copy full SHA for 1afeed2
Browse repository at this point
verify: Count the global objects a pointer's origins name as valid storage.
SwayamInSync
committed
b55b2bd
View commit details
Copy full SHA for b55b2bd
Browse repository at this point
test: Check global records and arrays as objects at their addresses.
SwayamInSync
committed
d8973a9
View commit details
Copy full SHA for d8973a9
Browse repository at this point
test: Expect a mutable global array's element to be any value at entry.
SwayamInSync
committed
8653167
View commit details
Copy full SHA for 8653167
Browse repository at this point
test: Verify a range-based for loop over a global array.
SwayamInSync
committed
a4ec726
View commit details
Copy full SHA for a4ec726
Browse repository at this point
test: Verify the elements of global arrays in pointer_subobjects.cpp.
SwayamInSync
committed
df51173
View commit details
Copy full SHA for df51173
Browse repository at this point
test: Verify a global array indexed by a value loaded from dynamic storage.
SwayamInSync
committed
11476fc
View commit details
Copy full SHA for 11476fc
Browse repository at this point
test: Expect a proof writing a global to be rejected as such.
SwayamInSync
committed
394b187
View commit details
Copy full SHA for 394b187
Browse repository at this point
test: Expect the message for a pointer global in z3_calls_fail_closed.cpp.
SwayamInSync
committed
5a25863
View commit details
Copy full SHA for 5a25863
Browse repository at this point
test: Use a pointer global as the unsupported construct of a contract.
SwayamInSync
committed
8027fa2
View commit details
Copy full SHA for 8027fa2
Browse repository at this point
test: Expect the message for a pointer global in per_function_errors.test.
SwayamInSync
committed
88f1335
View commit details
Copy full SHA for 88f1335
Browse repository at this point
docs: Describe global records and arrays.
SwayamInSync
committed
9406e0f
View commit details
Copy full SHA for 9406e0f
Browse repository at this point
docs: Allow a range-based for loop over a global array.
SwayamInSync
committed
666e872
View commit details
Copy full SHA for 666e872
Browse repository at this point
docs: Move global records and arrays to the supported column.
SwayamInSync
committed
eb25573
View commit details
Copy full SHA for eb25573
Browse repository at this point
docs: Add global records and arrays to the pointers chapter.
SwayamInSync
committed
157561f
View commit details
Copy full SHA for 157561f
Browse repository at this point
docs: Add global records and arrays to the release notes.
SwayamInSync
committed
fd7a0e1
View commit details
Copy full SHA for fd7a0e1
Browse repository at this point
docs: Describe global objects in DESIGN.md.
SwayamInSync
committed
83adcdc
View commit details
Copy full SHA for 83adcdc
Browse repository at this point
docs: Describe global objects in ARCHITECTURE.md.
SwayamInSync
committed
62c5cef
View commit details
Copy full SHA for 62c5cef
Browse repository at this point
Merge fix/inline-helpers into fix/global-objects.
SwayamInSync
committed
b651128
View commit details
Copy full SHA for b651128
Browse repository at this point
Commits on Oct 29, 2026
Merge main into fix/global-objects.
SwayamInSync
committed
589ff5d
View commit details
Copy full SHA for 589ff5d
Browse repository at this point
You can’t perform that action at this time.
