Skip to content

"low" changed to "lowElement", "high" changed to "highElement" - #46

Merged
jcp19 merged 5 commits into
viperproject:mainfrom
AkasakaJelos:feat/my-change
Jan 25, 2026
Merged

jcp19 merged 5 commits into
viperproject:mainfrom
AkasakaJelos:feat/my-change

Conversation

@AkasakaJelos

Copy link
Copy Markdown
Contributor

The keyword “low” in Gobra denotes low security in the non-interference model. Therefore, if “low” is defined as a variable, Gobra will produce the following compilation error due to a presumed keyword clash:

No changes detected in the antlr4 files. Skipping parser generation.
[info] running (fork) viper.gobra.GobraRunner -i /.../exercises/tutorial7.go
[info] Gobra 1.1-SNAPSHOT (351ad1fe@(detached))
[info] (c) Copyright ETH Zurich 2012 - 2024
[info] Verifying package .. - exercises [14:21:29]
[info] Error at: </.../exercises/tutorial7.go:14:5> no viable alternative at input 'low :='
[info] 	low := 0
[info]  ^^^^^^^^
[info] Gobra found 1 error.
[info]
[error] Nonzero exit code returned from runner: 1
[error] (Compile / run) Nonzero exit code returned from runner: 1
[error] Total time: 10 s, completed 25 Jan 2026, 14:21:30

The best approach is to rename "low" to "lowElement" and "high" to "highElement". I left "mid" unchanged, since it is already unambiguous :)

Updated binary search implementation to fix termination issues by changing variable names and adjusting the decreases condition for loop termination checking.
Refactor BinarySearchOverflow to prevent integer overflow during mid calculation by using lowElement and highElement.
@jcp19

jcp19 commented Jan 25, 2026

Copy link
Copy Markdown
Collaborator

Hi Kwok, thank you for the PR, it is much appreciated :)

@jcp19
jcp19 merged commit da504bc into viperproject:main Jan 25, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants