diff options
author | James Pollard <james@pollard.dev> | 2020-06-24 18:15:55 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-24 18:15:55 +0100 |
commit | c31d0037ba769f99f45edf3c02c82a71414a8d25 (patch) | |
tree | 758fe4e88ffd73f6cffb62a086007fea1ab92a34 /src/translation | |
parent | 0c7a19d7e1fc6ba980586292fc44fbec0dc6ce7e (diff) | |
parent | 9e29a351fd0928130fa0b67dc47b67cdf989e4b7 (diff) | |
download | vericert-kvx-c31d0037ba769f99f45edf3c02c82a71414a8d25.tar.gz vericert-kvx-c31d0037ba769f99f45edf3c02c82a71414a8d25.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/translation')
-rw-r--r-- | src/translation/HTLgen.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index dc82fb1..e637d6f 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -572,8 +572,7 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true. -(* +Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with | Some b => @@ -582,7 +581,7 @@ Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true. | _ => false end | _ => false - end. *) + end. Definition transl_program (p : RTL.program) : Errors.res HTL.program := if main_is_internal p |