From 537857a59def9c9fb16035ac81c121b1ae176b66 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 3 Oct 2019 11:32:56 +0200 Subject: Duplicate - Proof of verificator for Inop --- backend/Duplicate.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backend/Duplicate.v') 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 *) -- cgit