diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/LlbcAst.ml | 13 | ||||
| -rw-r--r-- | src/LlbcOfJson.ml (renamed from src/CfimOfJson.ml) | 0 | ||||
| -rw-r--r-- | src/Logging.ml | 4 | ||||
| -rw-r--r-- | src/main.ml | 2 |
4 files changed, 16 insertions, 3 deletions
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml index f597cd27..149fb23d 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -186,3 +186,16 @@ type fun_decl = { * 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. *) + +(* +type fun_body = { arg_count : int; locals : var list; body : statement } +[@@deriving show] + +type fun_decl = { + def_id : FunDeclId.id; + name : fun_name; + signature : fun_sig; + body : fun_body option; +} +[@@deriving show] +*) diff --git a/src/CfimOfJson.ml b/src/LlbcOfJson.ml index e293b030..e293b030 100644 --- a/src/CfimOfJson.ml +++ b/src/LlbcOfJson.ml diff --git a/src/Logging.ml b/src/Logging.ml index 7f4152a5..6dca854c 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -9,8 +9,8 @@ let main_log = L.get_logger "MainLogger" (** Below, we create subgloggers for various submodules, so that we can precisely toggle logging on/off, depending on which information we need *) -(** Logger for CfimOfJson *) -let llbc_of_json_logger = L.get_logger "MainLogger.CfimOfJson" +(** Logger for LlbcOfJson *) +let llbc_of_json_logger = L.get_logger "MainLogger.LlbcOfJson" (** Logger for PrePasses *) let pre_passes_log = L.get_logger "MainLogger.PrePasses" diff --git a/src/main.ml b/src/main.ml index 4740f14c..577ba666 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,4 +1,4 @@ -open CfimOfJson +open LlbcOfJson open Logging open Print module T = Types |