From e8803586c36512b8fe65ec58de1f1eec990ce1d0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 20 Nov 2020 21:04:47 +0100 Subject: Trying to finish the bisimu reduce proof for builtin (last case admitted) --- aarch64/Asmblock.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/Asmblock.v') 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. -- cgit