search

gradual-verification / silicon-gv

Mozilla Public License 2.0
0 stars 3 forks source link

Backend not printing run-time checks #31

Closed jennalwise closed 2 years ago

jennalwise commented 2 years ago

https://github.com/gradual-verification/gvc0/blob/master/src/test/resources/bugs/condition_version.c0 when run through the frontend and full pipeline produces a .c0 file with the correct run-time check injected. The full pipeline also reports the correct run-time check is being given to the frontend by the backend. Also, the backend reports the correct number of statically verified conjuncts. However, when looking at the debugging output of the file when run in the backend only, the printed run-time checks map is empty. This doesn’t happen for files where more than 1 run-time check is produced or at least I haven’t witnessed this issue for c0 programs that produce 0 or more than 1 run-time check.

hgouni commented 2 years ago

I've resolved this in commit 745a4c29798ba827fb29991aef847ca2ee607518.