From 2b0c8766b4e99772777763e96e13747454672814 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Jun 2020 17:21:06 +0100 Subject: Add proof for initial state --- src/translation/HTLgen.v | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'src/translation/HTLgen.v') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index aa965fc..78b1864 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -371,7 +371,13 @@ Definition max_state (f: function) : state := Definition transl_module (f : function) : Errors.res module := run_mon (max_state f) (transf_module f). -Definition transl_fundef := transf_partial_fundef transl_module. +Definition transl_fundef (f : RTL.fundef) : Errors.res HTL.fundef := + match f with + | Internal f' => + Errors.bind (transl_module f') + (fun f'' => Errors.OK (Internal f'')) + | _ => Errors.Error (Errors.msg "External function could not be translated.") + end. (** Translation of a whole program. *) -- cgit