diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2021-01-06 16:35:07 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2021-01-06 16:35:07 +0100 |
| commit | 6a77f39a8e8ea383ddfa76cbe444b93ef5501429 (patch) | |
| tree | 6c056bb38ece5eabcfdd8fd420ac91abe25776fa /backend/Duplicateproof.v | |
| parent | 75bee70a6481c6bcf5bfa85f2558b08f5387db9c (diff) | |
| download | compcert-kvx-6a77f39a8e8ea383ddfa76cbe444b93ef5501429.tar.gz compcert-kvx-6a77f39a8e8ea383ddfa76cbe444b93ef5501429.zip | |
Solving a stack overflow issue (was failing in yarpgen ran000089 for armhf)
Note : the issue is still present later in Duplicateproof. This is
because I am examining an "identity ptree" which is way too big. I am
having a look to see if I could make this ptree less big - to not
include nodes that are identity
Diffstat (limited to 'backend/Duplicateproof.v')
0 files changed, 0 insertions, 0 deletions