diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-03 11:32:56 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-03 11:32:56 +0200 |
| commit | 537857a59def9c9fb16035ac81c121b1ae176b66 (patch) | |
| tree | a7355e612cf563cd5650bdce034af499647e0bb1 /backend/Duplicate.v | |
| parent | 57fce9febbd616becc8f120447de9c40318bcbfa (diff) | |
| download | compcert-kvx-537857a59def9c9fb16035ac81c121b1ae176b66.tar.gz compcert-kvx-537857a59def9c9fb16035ac81c121b1ae176b66.zip | |
Duplicate - Proof of verificator for Inop
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 07577704..ce6c436f 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -74,7 +74,8 @@ Definition verify_mapping_match_nodes (f: function) (xf: xfunction) : res unit : (** Verifies that the [fn_revmap] of the translated function [xf] is giving correct information in regards to [f] *) Definition verify_mapping (f: function) (xf: xfunction) : res unit := - do u <- verify_mapping_entrypoint f xf; OK tt. + do u <- verify_mapping_entrypoint f xf; + do v <- verify_mapping_match_nodes f xf; OK tt. (* TODO - verify the other axiom *) (** * Entry points *) |