summaryrefslogtreecommitdiff
path: root/src/reporting_basic.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-08-21 16:57:23 +0100
committerAlasdair Armstrong2017-08-21 16:57:23 +0100
commit8f9f30172204d75ff36d4c491802f460472cfa85 (patch)
tree8f6848d36c365dad36e31e1556afa668bd8636bd /src/reporting_basic.ml
parentc310ad77dee2bec75c272556e4ec843f5d9f2715 (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