Branching fix for adherence to gradual guarantee

gradual-verification / silicon-gv

Mozilla Public License 2.0

0 stars 3 forks source link

Branching fix for adherence to gradual guarantee #19

Closed jennalwise closed 2 years ago

jennalwise commented 2 years ago

This branch has implemented the fix outlined and discussed here: https://github.com/gradual-verification/recursive-predicates/issues/5 . Test files for both the backend and frontend for this fix have been created:

vpr file: https://github.com/gradual-verification/silver-gv/commit/91a39e3d72ec0c9c5ce72b476078727752a2a987
c0 file: https://github.com/gradual-verification/gvc0/commit/6776201da702e0ba0b1e81af328b2ab79564ccf8

hgouni commented 2 years ago

I've resolved the conflicts with the runtimeCheckInterface branch and updated the runtime checking to reflect our more conservative use of the translator. I've got some questions that we can probably discuss at our meeting tomorrow about the way positions are being obtained for the runtime checks (I'll leave a note here for documentation after we've talked about it).