diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-06 20:32:28 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-06 20:32:28 +0200 |
| commit | f855402a10148047e449073ae6c32d269275cdf4 (patch) | |
| tree | e382084b0819b7ad97460777ef51ccbc94d8c18c /scheduling/BTLroadmap.md | |
| parent | 322192e944a099c004dc8e71df0b1da975ec680c (diff) | |
| download | compcert-kvx-f855402a10148047e449073ae6c32d269275cdf4.tar.gz compcert-kvx-f855402a10148047e449073ae6c32d269275cdf4.zip | |
m
Diffstat (limited to 'scheduling/BTLroadmap.md')
| -rw-r--r-- | scheduling/BTLroadmap.md | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index bfbc1e03..9dd21be9 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -393,7 +393,9 @@ exécution symbolique que le bloc `ib1` est simulé par `ib2` modulo `TRANSFER` sur l'entrée `pc` se ramène à montrer `ib1[TRANSFER]` avec `TRANSFER(pc); ib2` pour la simulation symbolique usuelle. - Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des sorties `pc'` de `ib1`. +Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des sorties `pc'` de `ib1`. + +**REM** pour que ce soit correct, il faut sans doute vérifier une condition du style `ok(ib1) => ok(ib1[TRANSFER])`... ## Support of SSA-optimizations |