Skip to content

Update to Boogie 2.15.9 #441

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gauravpartha merged 9 commits into from
Dec 22, 2022
Merged

Update to Boogie 2.15.9 #441

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
a58d5bd
add new Boogie reserved keyword is
gauravpartha Nov 21, 2022
afe5bbe
update to Boogie 2.15.9 in CI
gauravpartha Nov 21, 2022
9317e1d
output Boogie version in CI
gauravpartha Nov 21, 2022
6ab496e
Try Boogie SMT name normalization option
gauravpartha Dec 19, 2022
7d9543f
Try Boogie emitDebugInformation:0 option
gauravpartha Dec 19, 2022
5463c0f
do not change options for Boogie 12.15.9
gauravpartha Dec 21, 2022
27cfbc2
Merge branch 'master' into boogie_dotnet6
gauravpartha Dec 21, 2022
b5ee3db
update Silver dependency
gauravpartha Dec 21, 2022
5b25c71
Merge branch 'master' of https://github.com/viperproject/carbon into …
gauravpartha Dec 21, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ jobs:
container: gobraverifier/gobra-base:v5_z3_4.8.7 # Thank you, Gobra team
env:
BOOGIE_EXE: "boogie/Boogie"
LINUX_BOOGIE_URL: "https://github.com/viperproject/boogie-builder/releases/download/bae82d3a7b383161/boogie-linux.zip"
LINUX_BOOGIE_URL: "https://github.com/viperproject/boogie-builder/releases/download/7449a7a899c02c95/boogie-linux.zip"
steps:
- name: Checkout Carbon
uses: actions/checkout@v2
Expand Down Expand Up @@ -57,6 +57,7 @@ jobs:
unzip boogie-linux.zip
rm -rf boogie-linux.zip
mv binaries-linux boogie
boogie/Boogie /version
pwd

- name: Test Carbon
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ class BoogieNameGenerator extends DefaultNameGenerator {
"invariant", "goto", "break", "return", "call", "forall", "assert", "havoc", "assume", "returns", "var", "implementation",
"axiom", "exists", "old", "false", "real", "int", "true", "bool", "finite", "ensures", "requires", "modifies", "where", "par", "lambda",
"uses", "RTP", "RTZ", "yield", "async", "roundNearestTiesToAway", "roundNearestTiesToEven", "extends", "roundTowardPositive",
"roundTowardZero", "RNA", "RTN", "roundTowardNegative", "RNE") ++
"roundTowardZero", "RNA", "RTN", "roundTowardNegative", "RNE", "is") ++
Set("Set", "MultiSet", "Seq")
val SMTreservedNames: Set[String] = Set(
// Basic symbols:
Expand Down
⚡