As discussed last meeting, this allows to set a "bound" for the ranges in error reports, so that a wrongly-computed range cannot just escape to anywhere in the file, or even worse to other files.
This is not currently set by F*, but will be used by Pulse.
As discussed last meeting, this allows to set a "bound" for the ranges in error reports, so that a wrongly-computed range cannot just escape to anywhere in the file, or even worse to other files.
This is not currently set by F*, but will be used by Pulse.