search

gradual-verification / silicon-gv

Mozilla Public License 2.0
0 stars 3 forks source link

Translating run-time checks from asserts with wrong state #40

Closed jennalwise closed 2 years ago

jennalwise commented 2 years ago

Need to look more closely at condition_version.c0 in gvc0 bug folder, because it looks like the run-time check translation happening in that example is occurring with the incorrect state. The run-time check ends up being correct, however it seems like the wrong state is being used to translate it. As it comes from an assert statement, the run-time check is not produced until the end of the static verification in main and I think this is the reason for the incorrectness. I.e. this only applies to assert statements.

jennalwise commented 2 years ago

The state seems to be from the correct point, but the path conditions are definitely incorrect (from the wrong evaluation point).

jennalwise commented 2 years ago

The solution is a one liner, to create a duplicate/copy of the path condition rather than pass a pointer to the path condition.

jennalwise commented 2 years ago

Fixed in commit https://github.com/gradual-verification/silicon-gv/commit/f6b4c2680db5f81f11999241b4e1166c619b72d9 .