diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-05-02 14:02:44 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-05-02 14:02:44 +0200 |
| commit | 25ea686abc4cce13aba92196dbeb284f727b6e0e (patch) | |
| tree | 95346bc265b109a0b1522b39ad09c1452996e84d /debug | |
| parent | 38898389f48baac4a319c973d77bb6e69f98d502 (diff) | |
| download | compcert-kvx-25ea686abc4cce13aba92196dbeb284f727b6e0e.tar.gz compcert-kvx-25ea686abc4cce13aba92196dbeb284f727b6e0e.zip | |
Tunnelingproof: Remove assumption destroyed_by_cond c = nil.
Since commit e5b37a6 (useless conditional branch elimination), the proof of the Tunneling pass was assuming forall c, destroyed_by_cond c = nil. This is not true for architecture variants that we will support soon. This commit rewrites the proof so as to remove this assumption. The old proof was by memory and value equalities, the new one is by memory extensions and "lessdef" values.
Diffstat (limited to 'debug')
0 files changed, 0 insertions, 0 deletions