diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-20 21:04:47 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-20 21:04:47 +0100 |
| commit | e8803586c36512b8fe65ec58de1f1eec990ce1d0 (patch) | |
| tree | 96c41b8ef0a03d9d61ca1ee2d823b8ba9b728853 /aarch64/Asmblock.v | |
| parent | 61b41b4f2e46ecd4a023ce72e72f697b5f1e2637 (diff) | |
| download | compcert-kvx-e8803586c36512b8fe65ec58de1f1eec990ce1d0.tar.gz compcert-kvx-e8803586c36512b8fe65ec58de1f1eec990ce1d0.zip | |
Trying to finish the bisimu reduce proof for builtin (last case admitted)
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index bdcead0b..da45324b 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -1481,7 +1481,7 @@ Definition incrPC size_b (rs: regset) := Definition estep (f: function) oc size_b (rs: regset) (m: mem) := match oc with | Some (PCtlFlow cfi) => exec_cfi f cfi (incrPC size_b rs) m - | Some (Pbuiltin ef args res) => None + | Some (Pbuiltin ef args res) => Next (incrPC size_b rs) m | None => Next (incrPC size_b rs) m end. |