Skip to content
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.

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

single variable assignment #82

Open
nkrusch opened this issue Aug 19, 2022 · 1 comment
Open

single variable assignment #82

nkrusch opened this issue Aug 19, 2022 · 1 comment

Comments

@nkrusch
Copy link
Contributor

nkrusch commented Aug 19, 2022

Analyzing single variable assignment

int foo(int x, int y){
x = y;
}

gives the matrix below and choices [0], [1], [2].

x y
x o o
y m m

I don't think the choice applies here? This is by rule E1.

@aubertc
Copy link
Contributor

aubertc commented Aug 22, 2022

Yes, this is by rule E^S in our paper, and indeed there should be no choice here. I am guessing that axioms are very much hard-coded into thinking they need a choice, and so that the implementation just says in this case "Whatever choice you make will work". It is a bit un-necessary, I agree, but I don't think it is an issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

No branches or pull requests

2 participants