diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2021-01-19 11:56:01 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2021-01-19 11:56:01 +0100 |
| commit | 6bcd2f58d0cef23fb1314fc678657c00a7a0d1e8 (patch) | |
| tree | 5b243a0c6865b89e1f2f878f5ba40acb35cd2e1d | |
| parent | fc9d9ffcf9157d4e84473a209e360ddc2210f95d (diff) | |
| download | compcert-kvx-6bcd2f58d0cef23fb1314fc678657c00a7a0d1e8.tar.gz compcert-kvx-6bcd2f58d0cef23fb1314fc678657c00a7a0d1e8.zip | |
Some comment clean on RTLpath
| -rw-r--r-- | scheduling/RTLpath.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v index 35512652..cccc8147 100644 --- a/scheduling/RTLpath.v +++ b/scheduling/RTLpath.v @@ -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 }. |