Add functionality to run counter-models in gdb #25
Labels
enhancement
New feature or request
good first issue
Good for newcomers
WP
Involves the Weakest Precondition computation
We can generate GDB command files (https://sourceware.org/gdb/onlinedocs/gdb/Command-Files.html) to set breakpoints and register values to attempt to exercise concrete counter models of properties in a run-time environment.
With more work, we can extend this to memory values as well.
I don't expect this to be extraordinarily scalable, since the target function needs to be reached in the first place, and there are many constraints on valid memory values which we are not tracking, etc.
It'll be good for debugging and exploration though.
The text was updated successfully, but these errors were encountered: