| Version 1 (modified by , 10 years ago) ( diff ) |
|---|
Here is the plan
- In quantified expressions, contracts: no functions and arguments to % and / should be non-negative (otherwise it will be an undefined behavior);
- IntDivTransformer will skip quantifiers, contracts; (no need for transformation)
- work on static analysis for intervals
- repeal (1) and (2)
Note:
See TracWiki
for help on using the wiki.
