From 0a1d60de5801cc53e17a621e3615279e88e7c790 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Tue, 30 Apr 2019 13:13:42 +0200 Subject: [PATCH] Fix backend proofs broken by adding FMA instruction --- compiler/encoders/arm6/proofs/arm6_targetProofScript.sml | 1 + compiler/encoders/arm7/proofs/arm7_targetProofScript.sml | 1 + 2 files changed, 2 insertions(+) diff --git a/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml b/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml index 07c47f5fea..dc4d02596f 100644 --- 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 index 43c76bfbdf..1b7eb2c0a8 100644 --- 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)