diff options
| author | James Pollard <james@pollard.dev> | 2020-06-03 15:29:54 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-03 15:29:54 +0100 |
| commit | 7e20d7bed643300605d9ff157d6dd206a7bb6b7b (patch) | |
| tree | 6139957c9b1f70715af635e99e713c621e403e6f /src/translation/HTLgen.v | |
| parent | 88553f08d8f2ad96ae615e9648b7c1417573247a (diff) | |
| parent | e9076031a8f759b10606e8507490ed8c68b16a43 (diff) | |
| download | vericert-kvx-7e20d7bed643300605d9ff157d6dd206a7bb6b7b.tar.gz vericert-kvx-7e20d7bed643300605d9ff157d6dd206a7bb6b7b.zip | |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 0fe6656..1a72261 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -410,7 +410,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. *) |