diff options
| author | Alasdair Armstrong | 2017-08-21 16:57:23 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-08-21 16:57:23 +0100 |
| commit | 8f9f30172204d75ff36d4c491802f460472cfa85 (patch) | |
| tree | 8f6848d36c365dad36e31e1556afa668bd8636bd /src/reporting_basic.ml | |
| parent | c310ad77dee2bec75c272556e4ec843f5d9f2715 (diff) | |
Modified sizeof rewriting pass so it can correctly deal with existentials.
Basically we needed to make the rewriting step for E_sizeof and
E_constraint more aggressively try to rewrite those expressions from
variables in scope, without adding new parameters to pass the type
variables at runtime, as this can break in the presence of existential
quantification. Still some cleanup to do in this code, but tests on
the arm spec show that it now introduces the minimal amount of new
parameters.
Diffstat (limited to 'src/reporting_basic.ml')
0 files changed, 0 insertions, 0 deletions
