summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/LlbcAst.ml13
-rw-r--r--src/LlbcOfJson.ml (renamed from src/CfimOfJson.ml)0
-rw-r--r--src/Logging.ml4
-rw-r--r--src/main.ml2
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