Fix backend proofs broken by adding FMA instruction

CakeML · Apr 30, 2019 · 0a1d60d · 0a1d60d
1 parent 4f52c41
commit 0a1d60d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml b/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml
@@ -1125,6 +1125,7 @@ Theorem arm6_encoder_correct
          >- (print_tac "FPSub"  \\ next_tac)
          >- (print_tac "FPMul"  \\ next_tac)
          >- (print_tac "FPDiv"  \\ next_tac)
+         >- (print_tac "FPFma"  \\ next_tac)
          >- (print_tac "FPMov"  \\ next_tac)
          >- (print_tac "FPMovToReg"   \\ next_tac)
          >- (print_tac "FPMovFromReg" \\ next_tac)

diff --git a/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml b/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml
@@ -1125,6 +1125,7 @@ Theorem arm7_encoder_correct
          >- (print_tac "FPSub"  \\ next_tac)
          >- (print_tac "FPMul"  \\ next_tac)
          >- (print_tac "FPDiv"  \\ next_tac)
+         >- (print_tac "FPFma"  \\ next_tac)
          >- (print_tac "FPMov"  \\ next_tac)
          >- (print_tac "FPMovToReg"   \\ next_tac)
          >- (print_tac "FPMovFromReg" \\ next_tac)