Treat r11 as caller-preserved in aes_hw_ctr32_encrypt_blocks

GaloisInc · Jan 7, 2021 · 7f648ff · 7f648ff
1 parent fe64788
commit 7f648ff
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/SAW/proof/AES/AES.saw b/SAW/proof/AES/AES.saw
@@ -173,6 +173,7 @@ aes_hw_decrypt_in_place_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_t
     w4_unint_yices ["AESInvRound", "AESFinalInvRound"];
   });
 
+add_x86_preserved_reg "r11";
 aes_hw_ctr32_encrypt_blocks_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aes_hw_ctr32_encrypt_blocks"
   []
   true
@@ -182,4 +183,5 @@ aes_hw_ctr32_encrypt_blocks_ov <- llvm_verify_x86 m "../../build/x86/crypto/cryp
     simplify (addsimps slice_384_thms basic_ss);
     w4_unint_yices ["AESRound", "AESFinalRound"];
   });
+default_x86_preserved_reg;