diff options
Diffstat (limited to 'backend/RTL.v')
| -rw-r--r-- | backend/RTL.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index fe350adf..8e313700 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -84,12 +84,18 @@ Inductive instruction: Type := Definition code: Type := PTree.t instruction. +Record untrusted_analysis: Type := mkuntrustedanalysis { + answer_to_life_the_universe_and_everything : option Z; + staged_header_dup : option (PTree.t positive * PTree.t instruction) +}. + Record function: Type := mkfunction { fn_sig: signature; fn_params: list reg; fn_stacksize: Z; fn_code: code; - fn_entrypoint: node + fn_entrypoint: node; + fn_untrusted_analysis: untrusted_analysis }. (** A function description comprises a control-flow graph (CFG) [fn_code] @@ -388,7 +394,8 @@ Definition transf_function (f: function) : function := f.(fn_params) f.(fn_stacksize) (PTree.map transf f.(fn_code)) - f.(fn_entrypoint). + f.(fn_entrypoint) + (mkuntrustedanalysis None None). End TRANSF. |