aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorMaxime Dénès2014-08-04 17:42:47 -0400
committerMaxime Dénès2014-08-04 18:10:12 -0400
commitf128088974e9ba543ca51ab76a92ff085def9728 (patch)
tree5ecae8a8c21af1a9f8fb5d0595bffaf7d6d9c508 /plugins
parent7d3c337a3b9f0906de22ccfde02203b8fafd330d (diff)
More optimization in guard checking.
When dynamically computing the recarg tree, we now prune it according to the inferred tree. Compilation of CompCert is now ok.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions