| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-22 | Added rewriter that specializes all function calls in a specification. | Alasdair Armstrong | |
| This removes all type polymorphism, so we can generate optimized bitvector code and compile to languages without parametric polymorphism. | |||
| 2018-01-18 | Modified unification so Type_check.instantiation_of works after sizeof rewriting | Alasdair Armstrong | |
| This change allows the AST to be type-checked after sizeof re-writing. It modifies the unification algorithm to better support checking multiplication in constraints, by using division and modulus SMT operators if they are defined. Also made sure the typechecker doesn't re-introduce E_constraint nodes, otherwise re-checking after sizeof-rewriting will re-introduce constraint nodes. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |