diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-07 14:33:29 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-07 14:33:29 +0100 |
| commit | 65103cdcf96b8c0411c9a7fec62a00daf6b5cb2e (patch) | |
| tree | de9193d4afddfc7b9a12948c9c251c0a46239b0a /cparser/Ceval.ml | |
| parent | 178e71c74a034d7ea13645ab843f4dd0e23a3255 (diff) | |
| download | compcert-65103cdcf96b8c0411c9a7fec62a00daf6b5cb2e.tar.gz compcert-65103cdcf96b8c0411c9a7fec62a00daf6b5cb2e.zip | |
Revised, more precise implementation of control-flow analysis
The new implementation keeps track of goto labels that are actually branched to. It is less optimized than the previous implementation (no bit vectors) but perhaps easier to read.
Diffstat (limited to 'cparser/Ceval.ml')
0 files changed, 0 insertions, 0 deletions