The extensions to Silver that will be added to support obligation-style reasoning (quantification over local state, etc.) do not appear to have any .sil test cases; they can only be indirectly tested via chalice2silver. We should have test cases for the features to illustrate which syntactic restrictions are enforced and to test the basic functionality.
The extensions to Silver that will be added to support obligation-style reasoning (quantification over local state, etc.) do not appear to have any .sil test cases; they can only be indirectly tested via chalice2silver. We should have test cases for the features to illustrate which syntactic restrictions are enforced and to test the basic functionality.