diff options
Diffstat (limited to 'src/CfimAst.ml')
| -rw-r--r-- | src/CfimAst.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 192638cf..6c9b596e 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -86,3 +86,10 @@ type fun_def = { body : statement; } [@@deriving show] +(** TODO: the type and function definitions contain information like `divergent` + * or `copyable`. I wonder if this information should be stored directly inside + * the definitions or inside separate maps/sets. + * Of course, if everything is stored in separate maps/sets, nothing + * prevents us from computing this info in Charon (and thus exporting directly + * it with the type/function defs), in which case we just have to implement special + * treatment when deserializing, to move the info to a separate map. *) |