diff options
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. |