diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-20 18:38:08 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-20 18:38:08 +0200 |
| commit | 437e499c046fbf5f527c0a8442982382d02c6871 (patch) | |
| tree | aee7d41ffa334b94139df971798a382a934b6ece /mppa_k1c/Asmblockgenproof0.v | |
| parent | 455736d0fff5f4b9636e8433519fe18ebb3c196d (diff) | |
| download | compcert-kvx-437e499c046fbf5f527c0a8442982382d02c6871.tar.gz compcert-kvx-437e499c046fbf5f527c0a8442982382d02c6871.zip | |
return_address_exists -> done
Diffstat (limited to 'mppa_k1c/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof0.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index 2fd6e768..bd4266ce 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -200,9 +200,7 @@ Hypothesis transf_function_len: forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned. -(* NB: the hypothesis on [b] is not needed in the proof ! - It is strange, no ? - *) +(* NB: the hypothesis in comment on [b] is not needed in the proof ! *) Lemma return_address_exists: forall b f (* sg ros *) c, (* b.(MB.exit) = Some (MBcall sg ros) -> *) is_tail (b :: c) f.(MB.fn_code) -> exists ra, return_address_offset f c ra. |