diff options
Diffstat (limited to 'backend/RTL.v')
| -rw-r--r-- | backend/RTL.v | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index 8e313700..fe350adf 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -84,18 +84,12 @@ 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_untrusted_analysis: untrusted_analysis + fn_entrypoint: node }. (** A function description comprises a control-flow graph (CFG) [fn_code] @@ -394,8 +388,7 @@ Definition transf_function (f: function) : function := f.(fn_params) f.(fn_stacksize) (PTree.map transf f.(fn_code)) - f.(fn_entrypoint) - (mkuntrustedanalysis None None). + f.(fn_entrypoint). End TRANSF. |