diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index ee18e5e3..f97a71b1 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -2088,6 +2088,7 @@ Local Transparent destroyed_at_function_entry. unfold loc_external_result.
apply agree_set_other; auto.
apply agree_set_pair; auto.
+ apply agree_undef_caller_save_regs; auto.
- (* return *)
inv MS.
|