I want to make C program that solves the 3rd problem of Project Euler (find the largest prime divisor of given number) and then formally verify/prove its correctness using VST.
The current state of the C program can be found here: https://github.com/LessnessRandomness/PE/blob/main/EulerProject3.c
(I took the code of Altinak at codereview.stackexchange.com)
I don't like the fact that the program uses global variable "highest" because I worry that it makes formal verification harder... Is it correct? Or am I wrong?
If I'm correct then how can I rewrite this little program in some better way to avoid difficulties caused by global variable?
I haven't used VST specifically, but I've used other separation logics. You could make highest local to find, and have it pass &highest to factorize; or you could try to pass highest as an input, and have find return a struct as an output. But I don't know if VST supports the last option, and I wouldn't expect the first two to be very different, since VST is a separation logic and manipulating mutable state is well-supported; you should probably try writing specs for the existing code before choosing to refactor things.
Last updated: Mar 02 2024 at 16:01 UTC