diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-17 18:28:55 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-17 18:28:55 +0100 |
| commit | a1c401a4eba5fc9fcf42933f70005ecb679a4c1c (patch) | |
| tree | 26637fca5d1da9b3d049234721d593a60b03a6d3 /arm/Asm.v | |
| parent | c49caca4b5f0239b43610fbfe012d6ba0211b364 (diff) | |
| parent | 1daf96cdca4d828c333cea5c9a314ef861342984 (diff) | |
| download | compcert-dev/michalis.tar.gz compcert-dev/michalis.zip | |
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'arm/Asm.v')
| -rw-r--r-- | arm/Asm.v | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -696,7 +696,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfsubd r1 r2 r3 => Next (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m | Pflid r1 f => - Next (nextinstr (rs#r1 <- (Vfloat f))) m + Next (nextinstr (rs#IR14 <- Vundef #r1 <- (Vfloat f))) m | Pfcmpd r1 r2 => Next (nextinstr (compare_float rs rs#r1 rs#r2)) m | Pfcmpzd r1 => @@ -923,7 +923,7 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge vargs m t vres m' -> rs' = nextinstr (set_res res vres - (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> + (undef_regs (IR IR14 :: map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', @@ -1004,7 +1004,7 @@ Ltac Equalities := split. auto. intros. destruct B; auto. subst. auto. (* trace length *) red; intros; inv H; simpl. - omega. + lia. inv H3; eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. (* initial states *) |