Commit 6bcd2f58 authored by Cyril SIX's avatar Cyril SIX
Browse files

Some comment clean on RTLpath

parent fc9d9ffc
......@@ -91,8 +91,7 @@ Record path_info := {
Definition path_map: Type := PTree.t path_info.
Definition path_entry (*c:code*) (pm: path_map) (n: node): Prop
:= pm!n <> None (*/\ c!n <> None*).
Definition path_entry (pm: path_map) (n: node): Prop := pm!n <> None.
Inductive wellformed_path (c:code) (pm: path_map): nat -> node -> Prop :=
| wf_last_node i pc:
......@@ -119,7 +118,7 @@ Record function : Type :=
{ fn_RTL:> RTL.function;
fn_path: path_map;
(* condition 1 below: the entry-point of the code is an entry-point of a path *)
fn_entry_point_wf: path_entry (*fn_RTL.(fn_code)*) fn_path fn_RTL.(fn_entrypoint);
fn_entry_point_wf: path_entry fn_path fn_RTL.(fn_entrypoint);
(* condition 2 below: the path_map is well-formed *)
fn_path_wf: wellformed_path_map fn_RTL.(fn_code) fn_path
}.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment