Release 2.10.0#830
Merged
Merged
Conversation
Starting from LLVM 13, there isn't a `toString` method for APInt that returns a std::string. Instead, it forces users to pass in a small vector of chars to hold the results. So I change all the old `toString` calls to a sequence of statements where a `SmallString` is created ,passed to new `to*String` calls, and finally gets converted to std::string using explicit conversions.
Bumped version number to 2.9.0
Update GitHub Actions versions
- bin/build.sh: install on 24.04 -- LLVM 14 comes from the Ubuntu universe repo (apt.llvm.org has no noble-14 feed, which also avoids the removed apt-key), and .NET 6 comes from ppa:dotnet/backports so Corral/Boogie keep running on the same .NET 6 runtime as 22.04. - share/smack/top.py: build the --check choices from VProperty.__members__ instead of iterating the Flag directly. Since Python 3.11 (24.04 ships 3.12) Flag iteration omits the zero member (none) and composite members (memory-safety), which silently dropped them from the valid choices and made those tests report UNKNOWN. - share/smack/svcomp/toSVCOMPformat.py: use a raw string for a regex to silence a Python 3.12 SyntaxWarning about an invalid escape sequence. - Dockerfile, .github/workflows/smack-ci.yaml: bump base image/runners to ubuntu 24.04. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The comment added for the Python 3.12 Flag-iteration fix had an 80-char line; reflow it under the 79-char E501 limit. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add Ubuntu 24.04 (noble) support
Fix MergeGEP for LLVM 14
Handle constrained FP intrinsics conservatively
Fix README CI badge endpoints
Handle LLVM copysign intrinsic
Include assert.h in rise4fun examples
Make NormalizeLoops a loop pass
Move rounding mode initialization to fenv model
Fix vector bitwise and comparison translation
…checks Avoid redundant split aggregate memory checks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Release SMACK 2.10.0 from the current develop branch.
This release moves SMACK to the LLVM 14 toolchain and includes the accumulated fixes on develop since v2.9.0.
Highlights:
Release mechanics: