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/process_file.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/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 1c133ce8..6a3fc24c 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -225,8 +225,6 @@ let output libpath out_arg files = files let rewrite_step defs rewriter = - (* print_endline "=============================== REWRITE STEP"; - Pretty_print.pp_defs stdout defs; *) let defs = rewriter defs in let _ = match !(opt_ddump_rewrite_ast) with | Some (f, i) -> |