diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-10 11:37:06 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-10 11:37:06 +0200 |
| commit | 3795aaf024d8585a6050ca16c4ea634dcb1f36cd (patch) | |
| tree | 2c59be63cdeb8437394337ddbd5c62a76132bd17 /aarch64/Asmblock.v | |
| parent | 250f2d6bebadec8b9079282edd5be61876214faf (diff) | |
| download | compcert-kvx-3795aaf024d8585a6050ca16c4ea634dcb1f36cd.tar.gz compcert-kvx-3795aaf024d8585a6050ca16c4ea634dcb1f36cd.zip | |
Change definition of match_states
Introduce agree which says that all registers *except* the PC return the
same values.
The idea behind this change is that agree can be preserved across e.g.
an Asmblock basic step, which does not update the PC.
In addition to agree, the simualation relation requires the PC to agree.
Right now the memory needs to be exactly the same which could be a
problem.
Since Asmblock's and Asm's set_pair is defined with preg it is more
difficult to show that set_pair preserves the agree relation since SP is
a preg and must not be Vundef. This commit does not solve the problem.
Diffstat (limited to 'aarch64/Asmblock.v')
0 files changed, 0 insertions, 0 deletions