diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-03-25 23:44:19 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-03-25 23:44:19 +0000 |
| commit | f96332369cbb2420e29a588d0ad9cd9810315423 (patch) | |
| tree | 7c422fd26b33588901f8d71cc29464bcdca98d9e /src/translation/HTLgen.v | |
| parent | 539177f4675398e72d59e03c04aa0ec907d7c08b (diff) | |
| download | vericert-kvx-f96332369cbb2420e29a588d0ad9cd9810315423.tar.gz vericert-kvx-f96332369cbb2420e29a588d0ad9cd9810315423.zip | |
Create HTLgen
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 705f9ad..9c2e168 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -179,6 +179,11 @@ Definition transf_function (f: function) : Errors.res module := | Error err => Errors.Error err end. +Definition example : mon HTL.code := PTree.traverse transf_instr + (PTree.set 2%positive (RTL.Icall sig ros args res n) (PTree.set 1%positive (RTL.Iop (Op.Omove) nil 1%positive 2%positive) (PTree.empty RTL.instruction))). + +Compute example. + Definition transf_fundef (fd: fundef) : Errors.res moddecl := transf_partial_fundef transf_function fd. |