diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-24 10:46:29 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-24 10:46:29 +0100 |
commit | e60d6c39dd960da14383a823a382e55f88258588 (patch) | |
tree | 8bfb0d4c185c3bccd896ab82589426dabd56f656 /src/translation/HTLgen.v | |
parent | 8c48e9e1094f037835698c88782772c8b3250a76 (diff) | |
parent | 624f1ee6ed054db89abc0c0a8bb58566119fadae (diff) | |
download | vericert-kvx-e60d6c39dd960da14383a823a382e55f88258588.tar.gz vericert-kvx-e60d6c39dd960da14383a823a382e55f88258588.zip |
Merge branch 'master' into develop
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r-- | src/translation/HTLgen.v | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 44b2937..66170bc 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -542,7 +542,7 @@ Definition transl_module (f : function) : Errors.res module := Definition transl_fundef := transf_partial_fundef transl_module. -Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. +(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *) (*Definition transl_main_fundef f : Errors.res HTL.fundef := match f with @@ -559,11 +559,18 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -(*Definition main_is_internal (p : RTL.program): Prop := +Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := let ge := Globalenvs.Genv.globalenv p in - forall b m, - Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> - Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m). + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal _) => true + | _ => false + end + | _ => false + end. -Definition tranls_program_with_proof (p : RTL.program) : Errors.res { p' : HTL.program | main_is_internal p }. -*) +Definition transl_program (p : RTL.program) : Errors.res HTL.program := + if main_is_internal p + then transform_partial_program transl_fundef p + else Errors.Error (Errors.msg "Main function is not Internal."). |