diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-21 17:21:56 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-21 17:21:56 +0200 |
| commit | e342ebbfe9751639e6e0d87a69029661376060b0 (patch) | |
| tree | ce69fd271542f15447afff261eafc19ea35a4b51 /extraction | |
| parent | 58083528c9dec31cbc1405a236fc6e3dc7779438 (diff) | |
| download | compcert-kvx-e342ebbfe9751639e6e0d87a69029661376060b0.tar.gz compcert-kvx-e342ebbfe9751639e6e0d87a69029661376060b0.zip | |
Adding buitin_args lemmas
There was an issue with the register PC in the eval_BA constructor for builtin : we were not able to prove that the concerned reg was different from PC.
This commit modify the definitions in Asmgen and Asmblock to support this, by replacing the parameter with a dreg instead of a preg.
Diffstat (limited to 'extraction')
0 files changed, 0 insertions, 0 deletions