diff --git a/flake.nix b/flake.nix
index 3c0b03ab..d9c00c09 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,30 +5,41 @@
     infuse-src.flake = false;
   };
   outputs =
-    { self
-    , nixpkgs
-    , infuse-src
+    {
+      self,
+      nixpkgs,
+      infuse-src,
     }@args:
     let
       inherit (nixpkgs) lib;
 
-      inherit (import ./nix/infuse-lib.nix {
-        lib = lib;
-        infuse-src = infuse-src;
-      }) infuse infuse-with;
+      inherit
+        (import ./nix/infuse-lib.nix {
+          lib = lib;
+          infuse-src = infuse-src;
+        })
+        infuse
+        infuse-with
+        ;
 
       inherit (import ./nix/flake-for-all-systems.nix { lib = lib; })
-        flake-for-all-systems;
+        flake-for-all-systems
+        ;
 
-    in flake-for-all-systems args {
-      systems = ["x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin"];
-      outputs = { self, nixpkgs, ... }:
+    in
+    flake-for-all-systems args {
+      systems = [
+        "x86_64-linux"
+        "aarch64-linux"
+        "aarch64-darwin"
+        "x86_64-darwin"
+      ];
+      outputs =
+        { self, nixpkgs, ... }:
         let
           pkgs = nixpkgs.legacyPackages;
-          selfOcamlPackages =
-            pkgs.ocamlPackages.overrideScope self.overlays.addBincamlPackages;
-          fpOcamlPackages =
-            selfOcamlPackages.overrideScope self.overlays.enableOcamlFramePointer;
+          selfOcamlPackages = pkgs.ocamlPackages.overrideScope self.overlays.addBincamlPackages;
+          fpOcamlPackages = selfOcamlPackages.overrideScope self.overlays.enableOcamlFramePointer;
         in
         {
           defaultPackage = selfOcamlPackages.bincaml;
@@ -40,17 +51,19 @@
               intPQueue = ofinal.callPackage ./nix/intpqueue.nix { };
             };
 
-            enableOcamlFramePointer = ofinal: infuse-with {
-              # https://github.com/NixOS/nixpkgs/blob/aca4d95fce4914b3892661bcb80b8087293536c6/pkgs/development/compilers/ocaml/generic.nix#L30
-              ocaml.__input.flambdaSupport.__assign = true;
-              ocaml.__input.framePointerSupport.__assign = true;
-              ocaml.__attrs.patches.__append = [
-                (pkgs.fetchpatch {
-                  url = "https://github.com/ocaml/ocaml/commit/c2eec4dd1de7d0da2d2f76e5e7f2b567901f4e2c.patch";
-                  hash = "sha256-qDx8saOLhFMYaK4PLsSvHnDBYKvRSMmPtdVa/IqkQSI=";
-                })
-              ];
-            };
+            enableOcamlFramePointer =
+              ofinal:
+              infuse-with {
+                # https://github.com/NixOS/nixpkgs/blob/aca4d95fce4914b3892661bcb80b8087293536c6/pkgs/development/compilers/ocaml/generic.nix#L30
+                ocaml.__input.flambdaSupport.__assign = true;
+                ocaml.__input.framePointerSupport.__assign = true;
+                ocaml.__attrs.patches.__append = [
+                  (pkgs.fetchpatch {
+                    url = "https://github.com/ocaml/ocaml/commit/c2eec4dd1de7d0da2d2f76e5e7f2b567901f4e2c.patch";
+                    hash = "sha256-qDx8saOLhFMYaK4PLsSvHnDBYKvRSMmPtdVa/IqkQSI=";
+                  })
+                ];
+              };
           };
 
           legacyPackages = {
@@ -68,8 +81,6 @@
             fp = fpOcamlPackages.callPackage ./nix/shell.nix { };
             no-fp = selfOcamlPackages.callPackage ./nix/shell.nix { };
           };
-        }
-      ;
-    }
-  ;
+        };
+    };
 }
diff --git a/lib/analysis/defuse_bool.ml b/lib/analysis/defuse_bool.ml
index 3f9cc038..7625901c 100644
--- a/lib/analysis/defuse_bool.ml
+++ b/lib/analysis/defuse_bool.ml
@@ -40,10 +40,17 @@ module IsZeroValueAbstraction = struct
     | `Bool true -> NonZero
     | `Bool false -> Zero
     | `Integer i -> if Z.equal Z.zero i then Zero else NonZero
-    | `Bitvector i ->
+    | `Bitvector i | `Pointer (i, _) ->
         if Bitvec.size i = 0 then Top
         else if Z.equal Z.zero (Bitvec.value i) then Zero
         else NonZero
+    | `Record fields ->
+        StringMap.fold
+          (fun _ ({ value = i; _ } : Lang.Ops.Record.field) acc ->
+            if Bitvec.size i = 0 then Top
+            else if Z.equal Z.zero (Bitvec.value i) then join acc Zero
+            else join acc NonZero)
+          fields Zero
 
   let eval_unop (op : Lang.Ops.AllOps.unary) a =
     match op with
@@ -58,13 +65,17 @@ module IsZeroValueAbstraction = struct
     | `Old -> Top
     | `Exists -> Top
     | `Forall | `Lambda | `Gamma | `Classification -> Top
+    (* NOTE: More effort would be needed to be able to say is this one field zero or not *)
+    | `FACCESS offset -> ( match a with Zero -> Zero | _ -> Top)
 
   let eval_binop (op : Lang.Ops.AllOps.binary) a b =
     match (op, a, b) with
     | `BVSREM, _, _ -> Top
     | `BVSDIV, _, _ -> Top
     | `BVADD, Zero, Zero -> Zero
+    | `PTRADD, Zero, Zero -> Zero
     | `BVADD, _, _ -> Top
+    | `PTRADD, _, _ -> Top
     | `NEQ, Zero, Zero -> Zero
     | `NEQ, _, _ -> Top
     | `BVASHR, _, _ -> Top
@@ -101,6 +112,10 @@ module IsZeroValueAbstraction = struct
     | `INTSUB, _, _ -> Top
     | `BVSLT, Zero, Zero -> Zero
     | `BVSLT, _, _ -> Top
+    | `FSET _, Zero, Zero -> Zero
+    | `FSET _, _, NonZero -> NonZero
+    (* Larger refactor would be needed to reason about individual fields *)
+    | `FSET _, _, _ -> Top
     | #Lang.Ops.Spec.binary, _, _ -> Top
 
   let eval_intrin (op : Lang.Ops.AllOps.intrin) (args : t list) =
diff --git a/lib/analysis/wrapped_intervals.ml b/lib/analysis/wrapped_intervals.ml
index f35a72f6..ae4f8e0b 100644
--- a/lib/analysis/wrapped_intervals.ml
+++ b/lib/analysis/wrapped_intervals.ml
@@ -697,7 +697,10 @@ module WrappedIntervalsValueAbstraction = struct
     match op with
     | `Bool _ -> top
     | `Integer _ -> top
-    | `Bitvector bv -> if size bv = 0 then top else interval bv bv
+    | `Bitvector bv | `Pointer (bv, _) ->
+        if size bv = 0 then top else interval bv bv
+    (* NOTE: This kind of thing happens frequently, should I go through all of the fields and make a intervals out of those bvs?*)
+    | `Record fields -> top
 
   let eval_unop (op : Lang.Ops.AllOps.unary) (a, t) rt =
     match t with
@@ -715,7 +718,7 @@ module WrappedIntervalsValueAbstraction = struct
     match (ta, ta) with
     | Types.Bitvector width, Types.Bitvector w2 when width = w2 -> (
         match op with
-        | `BVADD -> add ~width a b
+        | `BVADD | `PTRADD -> add ~width a b
         | `BVSUB -> sub ~width a b
         | `BVMUL -> mul ~width a b
         | `BVUDIV -> udiv ~width a b
diff --git a/lib/fe/AbsBasilIR.ml b/lib/fe/AbsBasilIR.ml
index 7e6d3e06..6851b539 100644
--- a/lib/fe/AbsBasilIR.ml
+++ b/lib/fe/AbsBasilIR.ml
@@ -1,8 +1,9 @@
-(* File generated by the BNF Converter (bnfc 2.9.6.2). *)
+(* File generated by the BNF Converter (bnfc 2.9.6.1). *)
 
 type bVTYPE = BVTYPE of ((int * int) * string)
 and iNTTYPE = INTTYPE of ((int * int) * string)
 and bOOLTYPE = BOOLTYPE of ((int * int) * string)
+and pOINTERTYPE = POINTERTYPE of ((int * int) * string)
 and bIdent = BIdent of ((int * int) * string)
 and localIdent = LocalIdent of ((int * int) * string)
 and globalIdent = GlobalIdent of ((int * int) * string)
@@ -48,12 +49,21 @@ and procDef =
    ProcDef_Empty
  | ProcDef_Some of beginList * block list * endList
 
+and field =
+   Field1 of openParen * str * typeT * closeParen
+
 and intType =
    IntType1 of iNTTYPE
 
 and boolType =
    BoolType1 of bOOLTYPE
 
+and recordType =
+   RecordType1 of beginRec * field list * endRec
+
+and pointerType =
+   PointerType1 of openParen * typeT * typeT * closeParen
+
 and bVType =
    BVType1 of bVTYPE
 
@@ -71,8 +81,10 @@ and typeT =
    TypeIntType of intType
  | TypeBoolType of boolType
  | TypeBVType of bVType
+ | TypePointerType of pointerType
+ | TypeRecordType of recordType
+ | TypeVarType of localIdent
  | TypeParen of openParen * typeT * closeParen
- | TypeSort of localIdent
  | TypeMapType of mapType
 
 and intVal =
@@ -82,6 +94,9 @@ and intVal =
 and bVVal =
    BVVal1 of intVal * bVType
 
+and fieldVal =
+   FieldVal1 of openParen * str * bVVal * typeT * closeParen
+
 and endian =
    Endian_Little
  | Endian_Big
@@ -186,6 +201,8 @@ and params =
 and value =
    Value_BV of bVVal
  | Value_Int of intVal
+ | Value_Record of openParen * fieldVal list * closeParen
+ | Value_Pointer of openParen * bVVal * pointerType * closeParen
  | Value_True
  | Value_False
 
@@ -207,6 +224,8 @@ and expr =
  | Expr_SignExtend of openParen * intVal * expr * closeParen
  | Expr_Extract of openParen * intVal * intVal * expr * closeParen
  | Expr_Concat of openParen * expr list * closeParen
+ | Expr_FSet of openParen * str * expr * expr * closeParen
+ | Expr_FAccess of openParen * str * expr * closeParen
  | Expr_Match of expr * openParen * case list * closeParen
  | Expr_Cases of openParen * case list * closeParen
  | Expr_Paren of openParen * expr * closeParen
@@ -220,6 +239,7 @@ and binOp =
  | BinOpIntLogicalBinOp of intLogicalBinOp
  | BinOpIntBinOp of intBinOp
  | BinOpEqOp of eqOp
+ | BinOpPointerBinOp of pointerBinOp
 
 and unOp =
    UnOpBVUnOp of bVUnOp
@@ -289,6 +309,9 @@ and boolBinOp =
  | BoolBinOp_boolor
  | BoolBinOp_boolimplies
 
+and pointerBinOp =
+   PointerBinOp_ptradd
+
 and requireTok =
    RequireTok_require
  | RequireTok_requires
diff --git a/lib/fe/BNFC_Util.ml b/lib/fe/BNFC_Util.ml
index 19303111..6d3bb604 100644
--- a/lib/fe/BNFC_Util.ml
+++ b/lib/fe/BNFC_Util.ml
@@ -1,4 +1,4 @@
-(* File generated by the BNF Converter (bnfc 2.9.6.2). *)
+(* File generated by the BNF Converter (bnfc 2.9.6.1). *)
 
 open Lexing
 
diff --git a/lib/fe/BasilIR.cf b/lib/fe/BasilIR.cf
index 6c375b16..799d1a25 100644
--- a/lib/fe/BasilIR.cf
+++ b/lib/fe/BasilIR.cf
@@ -7,6 +7,7 @@ terminator Decl ";";
 position token BVTYPE ('b' 'v' digit+) ;
 position token INTTYPE {"int"} ;
 position token BOOLTYPE {"bool"} ;
+position token POINTERTYPE {"ptr"} ;
 
 {- position token UserIdent '`' ((upper | letter | '_' | '#')(upper | letter | digit | ["_.$#"])*) '`'; -}
 position token BIdent '.'((upper | letter | '_')(upper | letter | digit | ["_.$#~"])*) ;
@@ -71,8 +72,13 @@ Decl_Type . Decl ::= "type" LocalIdent ;
 ProcDef_Empty . ProcDef ::= ;
 ProcDef_Some  . ProcDef ::= BeginList [Block] EndList ;
 
+separator Field "," ;
+Field1 . Field ::= OpenParen Str ":" Type CloseParen ;
+
 IntType1 . IntType ::= INTTYPE ;
 BoolType1. BoolType ::= BOOLTYPE ;
+RecordType1 . RecordType ::= BeginRec [Field] EndRec ;
+PointerType1 . PointerType ::= "ptr" OpenParen Type "," Type CloseParen ;
 BVType1 . BVType ::= BVTYPE ;
 -- map types are right associative. left of -> cannot be another MapType.
 MapType1 . MapType ::=  Type1 "->" Type ; 
@@ -86,13 +92,14 @@ VariantCase . SumCase    ::= LocalIdent "of" BeginRec [RecordField] EndRec;
 separator nonempty SumCase "|";
 
 
-TypeIntType  . Type1 ::= IntType ;
-TypeBoolType . Type1 ::= BoolType ;
-TypeBVType   . Type1 ::= BVType ;
-TypeParen    . Type1 ::= OpenParen Type CloseParen; 
-TypeSort . Type1 ::= LocalIdent;
-
-TypeMapType . Type ::= MapType;
+TypeIntType     . Type1 ::= IntType ;
+TypeBoolType    . Type1 ::= BoolType ;
+TypeBVType      . Type1 ::= BVType ;
+TypePointerType . Type1 ::= PointerType ;
+TypeRecordType  . Type1 ::= RecordType ;
+TypeVarType     . Type1 ::= LocalIdent ;
+TypeParen       . Type1 ::= OpenParen Type CloseParen; 
+TypeMapType     . Type ::= MapType;
 _ . Type ::= Type1;
 
 IntVal_Hex . IntVal ::= IntegerHex ;
@@ -100,6 +107,9 @@ IntVal_Dec . IntVal ::=  IntegerDec ;
 
 rules BVVal ::=  IntVal ":" BVType ;
 
+separator FieldVal "," ;
+rules FieldVal ::= OpenParen Str ":" BVVal "," Type CloseParen;
+
 Endian_Little . Endian ::= "le" ;
 Endian_Big . Endian ::= "be" ;
 
@@ -215,6 +225,8 @@ separator Params "," ;
 
 Value_BV . Value ::=  BVVal;
 Value_Int . Value ::= IntVal;
+Value_Record . Value ::= OpenParen [FieldVal] CloseParen;
+Value_Pointer . Value ::= "ptr" OpenParen BVVal "," PointerType CloseParen;
 Value_True . Value ::= "true" ;
 Value_False . Value ::= "false" ;
 
@@ -246,7 +258,7 @@ Expr_FunctionOp . Expr1       ::= Expr1 OpenParen [Expr] CloseParen;
 
 -- binary expr
 
-rules BinOp ::= BVBinOp | BVLogicalBinOp | IntLogicalBinOp | IntBinOp | EqOp ;
+rules BinOp ::= BVBinOp | BVLogicalBinOp | IntLogicalBinOp | IntBinOp | EqOp | PointerBinOp ;
 Expr_Binary . Expr2      ::= BinOp OpenParen Expr "," Expr CloseParen ;
 Expr_Assoc  . Expr2      ::= BoolBinOp OpenParen [Expr] CloseParen ;
 
@@ -260,6 +272,8 @@ Expr_ZeroExtend . Expr2 ::= "zero_extend" OpenParen IntVal "," Expr CloseParen ;
 Expr_SignExtend . Expr2 ::= "sign_extend" OpenParen IntVal "," Expr CloseParen ;
 Expr_Extract    . Expr2 ::= "extract" OpenParen IntVal "," IntVal "," Expr CloseParen ;
 Expr_Concat     . Expr2 ::= "bvconcat"  OpenParen [Expr]  CloseParen ;
+Expr_FSet       . Expr2 ::= "fset" OpenParen Str "," Expr "," Expr CloseParen ;
+Expr_FAccess    . Expr2 ::= "faccess" OpenParen Str "," Expr CloseParen ;
 
 CaseCase . Case ::= Expr "->" Expr  ;
 CaseDefault . Case ::=  "_" "->" Expr ;
@@ -280,7 +294,7 @@ rules BVLogicalBinOp ::= "bvule" |  "bvugt" |  "bvuge" | "bvult" | "bvslt" |  "b
 rules IntBinOp ::= "intadd" | "intmul" | "intsub" | "intdiv" | "intmod"  ;
 rules IntLogicalBinOp ::=  "intlt" | "intle" | "intgt" | "intge" ;
 rules BoolBinOp ::=  "booland" | "boolor" | "boolimplies" ;
-
+rules PointerBinOp ::= "ptradd" ;
 
 {- SPECIFICATION -}
 
diff --git a/lib/fe/LexBasilIR.mll b/lib/fe/LexBasilIR.mll
index d4f39668..0b86baa4 100644
--- a/lib/fe/LexBasilIR.mll
+++ b/lib/fe/LexBasilIR.mll
@@ -1,4 +1,4 @@
-(* File generated by the BNF Converter (bnfc 2.9.6.2). *)
+(* File generated by the BNF Converter (bnfc 2.9.6.1). *)
 
 (* Lexer definition for ocamllex. *)
 
@@ -11,9 +11,9 @@ let symbol_table = Hashtbl.create 10
 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add symbol_table kwd tok)
                   [(";", SYMB1);(",", SYMB2);("->", SYMB3);("::", SYMB4);(":", SYMB5);("=", SYMB6);("|", SYMB7);(":=", SYMB8);("mem:=", SYMB9);("_", SYMB10)]
 
-let resword_table = Hashtbl.create 101
+let resword_table = Hashtbl.create 105
 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add resword_table kwd tok)
-                  [("shared", KW_shared);("observable", KW_observable);("axiom", KW_axiom);("memory", KW_memory);("var", KW_var);("val", KW_val);("let", KW_let);("prog", KW_prog);("entry", KW_entry);("proc", KW_proc);("and", KW_and);("type", KW_type);("of", KW_of);("le", KW_le);("be", KW_be);("nop", KW_nop);("store", KW_store);("load", KW_load);("call", KW_call);("indirect", KW_indirect);("assume", KW_assume);("guard", KW_guard);("assert", KW_assert);("goto", KW_goto);("unreachable", KW_unreachable);("return", KW_return);("phi", KW_phi);("block", KW_block);("true", KW_true);("false", KW_false);("forall", KW_forall);("exists", KW_exists);("fun", KW_fun);("old", KW_old);("boolnot", KW_boolnot);("intneg", KW_intneg);("booltobv1", KW_booltobv1);("gamma", KW_gamma);("classification", KW_classification);("load_be", KW_load_be);("load_le", KW_load_le);("zero_extend", KW_zero_extend);("sign_extend", KW_sign_extend);("extract", KW_extract);("bvconcat", KW_bvconcat);("match", KW_match);("with", KW_with);("cases", KW_cases);("eq", KW_eq);("neq", KW_neq);("bvnot", KW_bvnot);("bvneg", KW_bvneg);("bvand", KW_bvand);("bvor", KW_bvor);("bvadd", KW_bvadd);("bvmul", KW_bvmul);("bvudiv", KW_bvudiv);("bvurem", KW_bvurem);("bvshl", KW_bvshl);("bvlshr", KW_bvlshr);("bvnand", KW_bvnand);("bvnor", KW_bvnor);("bvxor", KW_bvxor);("bvxnor", KW_bvxnor);("bvcomp", KW_bvcomp);("bvsub", KW_bvsub);("bvsdiv", KW_bvsdiv);("bvsrem", KW_bvsrem);("bvsmod", KW_bvsmod);("bvashr", KW_bvashr);("bvule", KW_bvule);("bvugt", KW_bvugt);("bvuge", KW_bvuge);("bvult", KW_bvult);("bvslt", KW_bvslt);("bvsle", KW_bvsle);("bvsgt", KW_bvsgt);("bvsge", KW_bvsge);("intadd", KW_intadd);("intmul", KW_intmul);("intsub", KW_intsub);("intdiv", KW_intdiv);("intmod", KW_intmod);("intlt", KW_intlt);("intle", KW_intle);("intgt", KW_intgt);("intge", KW_intge);("booland", KW_booland);("boolor", KW_boolor);("boolimplies", KW_boolimplies);("require", KW_require);("requires", KW_requires);("ensure", KW_ensure);("ensures", KW_ensures);("rely", KW_rely);("relies", KW_relies);("guarantee", KW_guarantee);("guarantees", KW_guarantees);("captures", KW_captures);("modifies", KW_modifies);("invariant", KW_invariant)]
+                  [("shared", KW_shared);("observable", KW_observable);("axiom", KW_axiom);("memory", KW_memory);("var", KW_var);("val", KW_val);("let", KW_let);("prog", KW_prog);("entry", KW_entry);("proc", KW_proc);("and", KW_and);("type", KW_type);("ptr", KW_ptr);("of", KW_of);("le", KW_le);("be", KW_be);("nop", KW_nop);("store", KW_store);("load", KW_load);("call", KW_call);("indirect", KW_indirect);("assume", KW_assume);("guard", KW_guard);("assert", KW_assert);("goto", KW_goto);("unreachable", KW_unreachable);("return", KW_return);("phi", KW_phi);("block", KW_block);("true", KW_true);("false", KW_false);("forall", KW_forall);("exists", KW_exists);("fun", KW_fun);("old", KW_old);("boolnot", KW_boolnot);("intneg", KW_intneg);("booltobv1", KW_booltobv1);("gamma", KW_gamma);("classification", KW_classification);("load_be", KW_load_be);("load_le", KW_load_le);("zero_extend", KW_zero_extend);("sign_extend", KW_sign_extend);("extract", KW_extract);("bvconcat", KW_bvconcat);("fset", KW_fset);("faccess", KW_faccess);("match", KW_match);("with", KW_with);("cases", KW_cases);("eq", KW_eq);("neq", KW_neq);("bvnot", KW_bvnot);("bvneg", KW_bvneg);("bvand", KW_bvand);("bvor", KW_bvor);("bvadd", KW_bvadd);("bvmul", KW_bvmul);("bvudiv", KW_bvudiv);("bvurem", KW_bvurem);("bvshl", KW_bvshl);("bvlshr", KW_bvlshr);("bvnand", KW_bvnand);("bvnor", KW_bvnor);("bvxor", KW_bvxor);("bvxnor", KW_bvxnor);("bvcomp", KW_bvcomp);("bvsub", KW_bvsub);("bvsdiv", KW_bvsdiv);("bvsrem", KW_bvsrem);("bvsmod", KW_bvsmod);("bvashr", KW_bvashr);("bvule", KW_bvule);("bvugt", KW_bvugt);("bvuge", KW_bvuge);("bvult", KW_bvult);("bvslt", KW_bvslt);("bvsle", KW_bvsle);("bvsgt", KW_bvsgt);("bvsge", KW_bvsge);("intadd", KW_intadd);("intmul", KW_intmul);("intsub", KW_intsub);("intdiv", KW_intdiv);("intmod", KW_intmod);("intlt", KW_intlt);("intle", KW_intle);("intgt", KW_intgt);("intge", KW_intge);("booland", KW_booland);("boolor", KW_boolor);("boolimplies", KW_boolimplies);("ptradd", KW_ptradd);("require", KW_require);("requires", KW_requires);("ensure", KW_ensure);("ensures", KW_ensures);("rely", KW_rely);("relies", KW_relies);("guarantee", KW_guarantee);("guarantees", KW_guarantees);("captures", KW_captures);("modifies", KW_modifies);("invariant", KW_invariant)]
 
 let unescapeInitTail (s:string) : string =
   let rec unesc s = match s with
@@ -59,6 +59,7 @@ let rsyms = ";" | "," | "->" | "::" | ":" | "=" | "|" | ":=" | "mem:=" | "_"
 let bVTYPE = "bv" _digit +
 let iNTTYPE = "int"
 let bOOLTYPE = "bool"
+let pOINTERTYPE = "ptr"
 let bIdent = '.' ('_' | _letter)('#' | '$' | '.' | '_' | '~' | (_digit | _letter)) *
 let localIdent = ('#' | '_' | _letter)('#' | '$' | '.' | '_' | (_digit | _letter)) *
 let globalIdent = '$' ('#' | '$' | '.' | '_' | (_digit | _letter)) +
@@ -85,6 +86,8 @@ rule token =
       | iNTTYPE { let l = lexeme lexbuf in try Hashtbl.find resword_table l with Not_found -> TOK_INTTYPE ((lexeme_start lexbuf, lexeme_end lexbuf), l) }
       | bOOLTYPE
                 { let l = lexeme lexbuf in try Hashtbl.find resword_table l with Not_found -> TOK_BOOLTYPE ((lexeme_start lexbuf, lexeme_end lexbuf), l) }
+      | pOINTERTYPE
+                { let l = lexeme lexbuf in try Hashtbl.find resword_table l with Not_found -> TOK_POINTERTYPE ((lexeme_start lexbuf, lexeme_end lexbuf), l) }
       | bIdent  { let l = lexeme lexbuf in try Hashtbl.find resword_table l with Not_found -> TOK_BIdent ((lexeme_start lexbuf, lexeme_end lexbuf), l) }
       | localIdent
                 { let l = lexeme lexbuf in try Hashtbl.find resword_table l with Not_found -> TOK_LocalIdent ((lexeme_start lexbuf, lexeme_end lexbuf), l) }
diff --git a/lib/fe/ParBasilIR.mly b/lib/fe/ParBasilIR.mly
index 976469cf..85c60cab 100644
--- a/lib/fe/ParBasilIR.mly
+++ b/lib/fe/ParBasilIR.mly
@@ -1,4 +1,4 @@
-/* File generated by the BNF Converter (bnfc 2.9.6.2). */
+/* File generated by the BNF Converter (bnfc 2.9.6.1). */
 
 /* Parser definition for use with menhir */
 
@@ -7,7 +7,7 @@ open AbsBasilIR
 open Lexing
 %}
 
-%token KW_shared KW_observable KW_axiom KW_memory KW_var KW_val KW_let KW_prog KW_entry KW_proc KW_and KW_type KW_of KW_le KW_be KW_nop KW_store KW_load KW_call KW_indirect KW_assume KW_guard KW_assert KW_goto KW_unreachable KW_return KW_phi KW_block KW_true KW_false KW_forall KW_exists KW_fun KW_old KW_boolnot KW_intneg KW_booltobv1 KW_gamma KW_classification KW_load_be KW_load_le KW_zero_extend KW_sign_extend KW_extract KW_bvconcat KW_match KW_with KW_cases KW_eq KW_neq KW_bvnot KW_bvneg KW_bvand KW_bvor KW_bvadd KW_bvmul KW_bvudiv KW_bvurem KW_bvshl KW_bvlshr KW_bvnand KW_bvnor KW_bvxor KW_bvxnor KW_bvcomp KW_bvsub KW_bvsdiv KW_bvsrem KW_bvsmod KW_bvashr KW_bvule KW_bvugt KW_bvuge KW_bvult KW_bvslt KW_bvsle KW_bvsgt KW_bvsge KW_intadd KW_intmul KW_intsub KW_intdiv KW_intmod KW_intlt KW_intle KW_intgt KW_intge KW_booland KW_boolor KW_boolimplies KW_require KW_requires KW_ensure KW_ensures KW_rely KW_relies KW_guarantee KW_guarantees KW_captures KW_modifies KW_invariant
+%token KW_shared KW_observable KW_axiom KW_memory KW_var KW_val KW_let KW_prog KW_entry KW_proc KW_and KW_type KW_ptr KW_of KW_le KW_be KW_nop KW_store KW_load KW_call KW_indirect KW_assume KW_guard KW_assert KW_goto KW_unreachable KW_return KW_phi KW_block KW_true KW_false KW_forall KW_exists KW_fun KW_old KW_boolnot KW_intneg KW_booltobv1 KW_gamma KW_classification KW_load_be KW_load_le KW_zero_extend KW_sign_extend KW_extract KW_bvconcat KW_fset KW_faccess KW_match KW_with KW_cases KW_eq KW_neq KW_bvnot KW_bvneg KW_bvand KW_bvor KW_bvadd KW_bvmul KW_bvudiv KW_bvurem KW_bvshl KW_bvlshr KW_bvnand KW_bvnor KW_bvxor KW_bvxnor KW_bvcomp KW_bvsub KW_bvsdiv KW_bvsrem KW_bvsmod KW_bvashr KW_bvule KW_bvugt KW_bvuge KW_bvult KW_bvslt KW_bvsle KW_bvsgt KW_bvsge KW_intadd KW_intmul KW_intsub KW_intdiv KW_intmod KW_intlt KW_intle KW_intgt KW_intge KW_booland KW_boolor KW_boolimplies KW_ptradd KW_require KW_requires KW_ensure KW_ensures KW_rely KW_relies KW_guarantee KW_guarantees KW_captures KW_modifies KW_invariant
 
 %token SYMB1 /* ; */
 %token SYMB2 /* , */
@@ -29,6 +29,7 @@ open Lexing
 %token <(int * int) * string> TOK_BVTYPE
 %token <(int * int) * string> TOK_INTTYPE
 %token <(int * int) * string> TOK_BOOLTYPE
+%token <(int * int) * string> TOK_POINTERTYPE
 %token <(int * int) * string> TOK_BIdent
 %token <(int * int) * string> TOK_LocalIdent
 %token <(int * int) * string> TOK_GlobalIdent
@@ -44,7 +45,7 @@ open Lexing
 %token <(int * int) * string> TOK_IntegerHex
 %token <(int * int) * string> TOK_IntegerDec
 
-%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pTypeAssign pTypeAssign_list pProcDef pIntType pBoolType pBVType pMapType pRecordField pRecordField_list pSumCase pSumCase_list pType1 pTypeT pIntVal pBVVal pEndian pAssignment pStmt pAssignment_list pLocalVar pLocalVar_list pGlobalVar pGlobalVar_list pVar pLocalVarParen pGlobalVarParen pLocalVarParen_list pNamedCallReturn pNamedCallReturn_list pLVars pNamedCallArg pNamedCallArg_list pCallParams pJump pLVar pLVar_list pBlock_list pStmtWithAttrib pStmtWithAttrib_list pJumpWithAttrib pPhiExpr pPhiExpr_list pPhiAssign pPhiAssign_list pBlock pAttrKeyValue pAttrKeyValue_list pAttribSet pAttr_list pAttr pParams pParams_list pValue pExpr_list pExpr pExpr1 pExpr2 pLambdaDef pBinOp pUnOp pCase pCase_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pBoolBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list
+%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pTypeAssign pTypeAssign_list pProcDef pField_list pField pIntType pBoolType pRecordType pPointerType pBVType pMapType pRecordField pRecordField_list pSumCase pSumCase_list pType1 pTypeT pIntVal pBVVal pFieldVal_list pFieldVal pEndian pAssignment pStmt pAssignment_list pLocalVar pLocalVar_list pGlobalVar pGlobalVar_list pVar pLocalVarParen pGlobalVarParen pLocalVarParen_list pNamedCallReturn pNamedCallReturn_list pLVars pNamedCallArg pNamedCallArg_list pCallParams pJump pLVar pLVar_list pBlock_list pStmtWithAttrib pStmtWithAttrib_list pJumpWithAttrib pPhiExpr pPhiExpr_list pPhiAssign pPhiAssign_list pBlock pAttrKeyValue pAttrKeyValue_list pAttribSet pAttr_list pAttr pParams pParams_list pValue pExpr_list pExpr pExpr1 pExpr2 pLambdaDef pBinOp pUnOp pCase pCase_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pBoolBinOp pPointerBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list
 %type <AbsBasilIR.moduleT> pModuleT
 %type <AbsBasilIR.decl list> pDecl_list
 %type <AbsBasilIR.blockIdent list> pBlockIdent_list
@@ -56,8 +57,12 @@ open Lexing
 %type <AbsBasilIR.typeAssign> pTypeAssign
 %type <AbsBasilIR.typeAssign list> pTypeAssign_list
 %type <AbsBasilIR.procDef> pProcDef
+%type <AbsBasilIR.field list> pField_list
+%type <AbsBasilIR.field> pField
 %type <AbsBasilIR.intType> pIntType
 %type <AbsBasilIR.boolType> pBoolType
+%type <AbsBasilIR.recordType> pRecordType
+%type <AbsBasilIR.pointerType> pPointerType
 %type <AbsBasilIR.bVType> pBVType
 %type <AbsBasilIR.mapType> pMapType
 %type <AbsBasilIR.recordField> pRecordField
@@ -68,6 +73,8 @@ open Lexing
 %type <AbsBasilIR.typeT> pTypeT
 %type <AbsBasilIR.intVal> pIntVal
 %type <AbsBasilIR.bVVal> pBVVal
+%type <AbsBasilIR.fieldVal list> pFieldVal_list
+%type <AbsBasilIR.fieldVal> pFieldVal
 %type <AbsBasilIR.endian> pEndian
 %type <AbsBasilIR.assignment> pAssignment
 %type <AbsBasilIR.stmt> pStmt
@@ -122,6 +129,7 @@ open Lexing
 %type <AbsBasilIR.intBinOp> pIntBinOp
 %type <AbsBasilIR.intLogicalBinOp> pIntLogicalBinOp
 %type <AbsBasilIR.boolBinOp> pBoolBinOp
+%type <AbsBasilIR.pointerBinOp> pPointerBinOp
 %type <AbsBasilIR.requireTok> pRequireTok
 %type <AbsBasilIR.ensureTok> pEnsureTok
 %type <AbsBasilIR.relyTok> pRelyTok
@@ -143,8 +151,12 @@ open Lexing
 %type <AbsBasilIR.typeAssign> typeAssign
 %type <AbsBasilIR.typeAssign list> typeAssign_list
 %type <AbsBasilIR.procDef> procDef
+%type <AbsBasilIR.field list> field_list
+%type <AbsBasilIR.field> field
 %type <AbsBasilIR.intType> intType
 %type <AbsBasilIR.boolType> boolType
+%type <AbsBasilIR.recordType> recordType
+%type <AbsBasilIR.pointerType> pointerType
 %type <AbsBasilIR.bVType> bVType
 %type <AbsBasilIR.mapType> mapType
 %type <AbsBasilIR.recordField> recordField
@@ -155,6 +167,8 @@ open Lexing
 %type <AbsBasilIR.typeT> typeT
 %type <AbsBasilIR.intVal> intVal
 %type <AbsBasilIR.bVVal> bVVal
+%type <AbsBasilIR.fieldVal list> fieldVal_list
+%type <AbsBasilIR.fieldVal> fieldVal
 %type <AbsBasilIR.endian> endian
 %type <AbsBasilIR.assignment> assignment
 %type <AbsBasilIR.stmt> stmt
@@ -209,6 +223,7 @@ open Lexing
 %type <AbsBasilIR.intBinOp> intBinOp
 %type <AbsBasilIR.intLogicalBinOp> intLogicalBinOp
 %type <AbsBasilIR.boolBinOp> boolBinOp
+%type <AbsBasilIR.pointerBinOp> pointerBinOp
 %type <AbsBasilIR.requireTok> requireTok
 %type <AbsBasilIR.ensureTok> ensureTok
 %type <AbsBasilIR.relyTok> relyTok
@@ -222,6 +237,7 @@ open Lexing
 %type <AbsBasilIR.bVTYPE> bVTYPE
 %type <AbsBasilIR.iNTTYPE> iNTTYPE
 %type <AbsBasilIR.bOOLTYPE> bOOLTYPE
+%type <AbsBasilIR.pOINTERTYPE> pOINTERTYPE
 %type <AbsBasilIR.bIdent> bIdent
 %type <AbsBasilIR.localIdent> localIdent
 %type <AbsBasilIR.globalIdent> globalIdent
@@ -261,10 +277,18 @@ pTypeAssign_list : typeAssign_list TOK_EOF { $1 };
 
 pProcDef : procDef TOK_EOF { $1 };
 
+pField_list : field_list TOK_EOF { $1 };
+
+pField : field TOK_EOF { $1 };
+
 pIntType : intType TOK_EOF { $1 };
 
 pBoolType : boolType TOK_EOF { $1 };
 
+pRecordType : recordType TOK_EOF { $1 };
+
+pPointerType : pointerType TOK_EOF { $1 };
+
 pBVType : bVType TOK_EOF { $1 };
 
 pMapType : mapType TOK_EOF { $1 };
@@ -285,6 +309,10 @@ pIntVal : intVal TOK_EOF { $1 };
 
 pBVVal : bVVal TOK_EOF { $1 };
 
+pFieldVal_list : fieldVal_list TOK_EOF { $1 };
+
+pFieldVal : fieldVal TOK_EOF { $1 };
+
 pEndian : endian TOK_EOF { $1 };
 
 pAssignment : assignment TOK_EOF { $1 };
@@ -393,6 +421,8 @@ pIntLogicalBinOp : intLogicalBinOp TOK_EOF { $1 };
 
 pBoolBinOp : boolBinOp TOK_EOF { $1 };
 
+pPointerBinOp : pointerBinOp TOK_EOF { $1 };
+
 pRequireTok : requireTok TOK_EOF { $1 };
 
 pEnsureTok : ensureTok TOK_EOF { $1 };
@@ -464,12 +494,26 @@ procDef : /* empty */ { ProcDef_Empty  }
   | beginList block_list endList { ProcDef_Some ($1, $2, $3) }
   ;
 
+field_list : /* empty */ { []  }
+  | field { (fun x -> [x]) $1 }
+  | field SYMB2 field_list { (fun (x,xs) -> x::xs) ($1, $3) }
+  ;
+
+field : openParen str SYMB5 typeT closeParen { Field1 ($1, $2, $4, $5) }
+  ;
+
 intType : iNTTYPE { IntType1 $1 }
   ;
 
 boolType : bOOLTYPE { BoolType1 $1 }
   ;
 
+recordType : beginRec field_list endRec { RecordType1 ($1, $2, $3) }
+  ;
+
+pointerType : KW_ptr openParen typeT SYMB2 typeT closeParen { PointerType1 ($2, $3, $5, $6) }
+  ;
+
 bVType : bVTYPE { BVType1 $1 }
   ;
 
@@ -494,8 +538,10 @@ sumCase_list : sumCase { (fun x -> [x]) $1 }
 type1 : intType { TypeIntType $1 }
   | boolType { TypeBoolType $1 }
   | bVType { TypeBVType $1 }
+  | pointerType { TypePointerType $1 }
+  | recordType { TypeRecordType $1 }
+  | localIdent { TypeVarType $1 }
   | openParen typeT closeParen { TypeParen ($1, $2, $3) }
-  | localIdent { TypeSort $1 }
   ;
 
 typeT : mapType { TypeMapType $1 }
@@ -509,6 +555,14 @@ intVal : integerHex { IntVal_Hex $1 }
 bVVal : intVal SYMB5 bVType { BVVal1 ($1, $3) }
   ;
 
+fieldVal_list : /* empty */ { []  }
+  | fieldVal { (fun x -> [x]) $1 }
+  | fieldVal SYMB2 fieldVal_list { (fun (x,xs) -> x::xs) ($1, $3) }
+  ;
+
+fieldVal : openParen str SYMB5 bVVal SYMB2 typeT closeParen { FieldVal1 ($1, $2, $4, $6, $7) }
+  ;
+
 endian : KW_le { Endian_Little  }
   | KW_be { Endian_Big  }
   ;
@@ -677,6 +731,8 @@ params_list : /* empty */ { []  }
 
 value : bVVal { Value_BV $1 }
   | intVal { Value_Int $1 }
+  | openParen fieldVal_list closeParen { Value_Record ($1, $2, $3) }
+  | KW_ptr openParen bVVal SYMB2 pointerType closeParen { Value_Pointer ($2, $3, $5, $6) }
   | KW_true { Value_True  }
   | KW_false { Value_False  }
   ;
@@ -709,6 +765,8 @@ expr2 : value { Expr_Literal $1 }
   | KW_sign_extend openParen intVal SYMB2 expr closeParen { Expr_SignExtend ($2, $3, $5, $6) }
   | KW_extract openParen intVal SYMB2 intVal SYMB2 expr closeParen { Expr_Extract ($2, $3, $5, $7, $8) }
   | KW_bvconcat openParen expr_list closeParen { Expr_Concat ($2, $3, $4) }
+  | KW_fset openParen str SYMB2 expr SYMB2 expr closeParen { Expr_FSet ($2, $3, $5, $7, $8) }
+  | KW_faccess openParen str SYMB2 expr closeParen { Expr_FAccess ($2, $3, $5, $6) }
   | KW_match expr KW_with openParen case_list closeParen { Expr_Match ($2, $4, $5, $6) }
   | KW_cases openParen case_list closeParen { Expr_Cases ($2, $3, $4) }
   | openParen expr closeParen { Expr_Paren ($1, $2, $3) }
@@ -722,6 +780,7 @@ binOp : bVBinOp { BinOpBVBinOp $1 }
   | intLogicalBinOp { BinOpIntLogicalBinOp $1 }
   | intBinOp { BinOpIntBinOp $1 }
   | eqOp { BinOpEqOp $1 }
+  | pointerBinOp { BinOpPointerBinOp $1 }
   ;
 
 unOp : bVUnOp { UnOpBVUnOp $1 }
@@ -797,6 +856,9 @@ boolBinOp : KW_booland { BoolBinOp_booland  }
   | KW_boolimplies { BoolBinOp_boolimplies  }
   ;
 
+pointerBinOp : KW_ptradd { PointerBinOp_ptradd  }
+  ;
+
 requireTok : KW_require { RequireTok_require  }
   | KW_requires { RequireTok_requires  }
   ;
@@ -841,6 +903,7 @@ progSpec_list : progSpec { (fun x -> [x]) $1 }
 bVTYPE : TOK_BVTYPE { BVTYPE ($1)};
 iNTTYPE : TOK_INTTYPE { INTTYPE ($1)};
 bOOLTYPE : TOK_BOOLTYPE { BOOLTYPE ($1)};
+pOINTERTYPE : TOK_POINTERTYPE { POINTERTYPE ($1)};
 bIdent : TOK_BIdent { BIdent ($1)};
 localIdent : TOK_LocalIdent { LocalIdent ($1)};
 globalIdent : TOK_GlobalIdent { GlobalIdent ($1)};
diff --git a/lib/fe/PrintBasilIR.ml b/lib/fe/PrintBasilIR.ml
index 25ba97ea..5a4ad15c 100644
--- a/lib/fe/PrintBasilIR.ml
+++ b/lib/fe/PrintBasilIR.ml
@@ -1,4 +1,4 @@
-(* File generated by the BNF Converter (bnfc 2.9.6.2). *)
+(* File generated by the BNF Converter (bnfc 2.9.6.1). *)
 
 (* pretty-printer *)
 
@@ -90,6 +90,9 @@ let prtINTTYPE _ (AbsBasilIR.INTTYPE (_,i)) : doc = render i
 let prtBOOLTYPE _ (AbsBasilIR.BOOLTYPE (_,i)) : doc = render i
 
 
+let prtPOINTERTYPE _ (AbsBasilIR.POINTERTYPE (_,i)) : doc = render i
+
+
 let prtBIdent _ (AbsBasilIR.BIdent (_,i)) : doc = render i
 
 
@@ -180,6 +183,13 @@ and prtProcDef (i:int) (e : AbsBasilIR.procDef) : doc = match e with
   |    AbsBasilIR.ProcDef_Some (beginlist, blocks, endlist) -> prPrec i 0 (concatD [prtBeginList 0 beginlist ; prtBlockListBNFC 0 blocks ; prtEndList 0 endlist])
 
 
+and prtField (i:int) (e : AbsBasilIR.field) : doc = match e with
+       AbsBasilIR.Field1 (openparen, str, type_, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtStr 0 str ; render ":" ; prtTypeT 0 type_ ; prtCloseParen 0 closeparen])
+
+and prtFieldListBNFC i es : doc = match (i, es) with
+    (_,[]) -> (concatD [])
+  | (_,[x]) -> (concatD [prtField 0 x])
+  | (_,x::xs) -> (concatD [prtField 0 x ; render "," ; prtFieldListBNFC 0 xs])
 and prtIntType (i:int) (e : AbsBasilIR.intType) : doc = match e with
        AbsBasilIR.IntType1 inttype -> prPrec i 0 (concatD [prtINTTYPE 0 inttype])
 
@@ -188,6 +198,14 @@ and prtBoolType (i:int) (e : AbsBasilIR.boolType) : doc = match e with
        AbsBasilIR.BoolType1 booltype -> prPrec i 0 (concatD [prtBOOLTYPE 0 booltype])
 
 
+and prtRecordType (i:int) (e : AbsBasilIR.recordType) : doc = match e with
+       AbsBasilIR.RecordType1 (beginrec, fields, endrec) -> prPrec i 0 (concatD [prtBeginRec 0 beginrec ; prtFieldListBNFC 0 fields ; prtEndRec 0 endrec])
+
+
+and prtPointerType (i:int) (e : AbsBasilIR.pointerType) : doc = match e with
+       AbsBasilIR.PointerType1 (openparen, type_1, type_2, closeparen) -> prPrec i 0 (concatD [render "ptr" ; prtOpenParen 0 openparen ; prtTypeT 0 type_1 ; render "," ; prtTypeT 0 type_2 ; prtCloseParen 0 closeparen])
+
+
 and prtBVType (i:int) (e : AbsBasilIR.bVType) : doc = match e with
        AbsBasilIR.BVType1 bvtype -> prPrec i 0 (concatD [prtBVTYPE 0 bvtype])
 
@@ -215,8 +233,10 @@ and prtTypeT (i:int) (e : AbsBasilIR.typeT) : doc = match e with
        AbsBasilIR.TypeIntType inttype -> prPrec i 1 (concatD [prtIntType 0 inttype])
   |    AbsBasilIR.TypeBoolType booltype -> prPrec i 1 (concatD [prtBoolType 0 booltype])
   |    AbsBasilIR.TypeBVType bvtype -> prPrec i 1 (concatD [prtBVType 0 bvtype])
+  |    AbsBasilIR.TypePointerType pointertype -> prPrec i 1 (concatD [prtPointerType 0 pointertype])
+  |    AbsBasilIR.TypeRecordType recordtype -> prPrec i 1 (concatD [prtRecordType 0 recordtype])
+  |    AbsBasilIR.TypeVarType localident -> prPrec i 1 (concatD [prtLocalIdent 0 localident])
   |    AbsBasilIR.TypeParen (openparen, type_, closeparen) -> prPrec i 1 (concatD [prtOpenParen 0 openparen ; prtTypeT 0 type_ ; prtCloseParen 0 closeparen])
-  |    AbsBasilIR.TypeSort localident -> prPrec i 1 (concatD [prtLocalIdent 0 localident])
   |    AbsBasilIR.TypeMapType maptype -> prPrec i 0 (concatD [prtMapType 0 maptype])
 
 and prtTypeTListBNFC i es : doc = match (i, es) with
@@ -232,6 +252,13 @@ and prtBVVal (i:int) (e : AbsBasilIR.bVVal) : doc = match e with
        AbsBasilIR.BVVal1 (intval, bvtype) -> prPrec i 0 (concatD [prtIntVal 0 intval ; render ":" ; prtBVType 0 bvtype])
 
 
+and prtFieldVal (i:int) (e : AbsBasilIR.fieldVal) : doc = match e with
+       AbsBasilIR.FieldVal1 (openparen, str, bvval, type_, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtStr 0 str ; render ":" ; prtBVVal 0 bvval ; render "," ; prtTypeT 0 type_ ; prtCloseParen 0 closeparen])
+
+and prtFieldValListBNFC i es : doc = match (i, es) with
+    (_,[]) -> (concatD [])
+  | (_,[x]) -> (concatD [prtFieldVal 0 x])
+  | (_,x::xs) -> (concatD [prtFieldVal 0 x ; render "," ; prtFieldValListBNFC 0 xs])
 and prtEndian (i:int) (e : AbsBasilIR.endian) : doc = match e with
        AbsBasilIR.Endian_Little  -> prPrec i 0 (concatD [render "le"])
   |    AbsBasilIR.Endian_Big  -> prPrec i 0 (concatD [render "be"])
@@ -400,6 +427,8 @@ and prtParamsListBNFC i es : doc = match (i, es) with
 and prtValue (i:int) (e : AbsBasilIR.value) : doc = match e with
        AbsBasilIR.Value_BV bvval -> prPrec i 0 (concatD [prtBVVal 0 bvval])
   |    AbsBasilIR.Value_Int intval -> prPrec i 0 (concatD [prtIntVal 0 intval])
+  |    AbsBasilIR.Value_Record (openparen, fieldvals, closeparen) -> prPrec i 0 (concatD [prtOpenParen 0 openparen ; prtFieldValListBNFC 0 fieldvals ; prtCloseParen 0 closeparen])
+  |    AbsBasilIR.Value_Pointer (openparen, bvval, pointertype, closeparen) -> prPrec i 0 (concatD [render "ptr" ; prtOpenParen 0 openparen ; prtBVVal 0 bvval ; render "," ; prtPointerType 0 pointertype ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Value_True  -> prPrec i 0 (concatD [render "true"])
   |    AbsBasilIR.Value_False  -> prPrec i 0 (concatD [render "false"])
 
@@ -422,6 +451,8 @@ and prtExpr (i:int) (e : AbsBasilIR.expr) : doc = match e with
   |    AbsBasilIR.Expr_SignExtend (openparen, intval, expr, closeparen) -> prPrec i 2 (concatD [render "sign_extend" ; prtOpenParen 0 openparen ; prtIntVal 0 intval ; render "," ; prtExpr 0 expr ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Expr_Extract (openparen, intval1, intval2, expr, closeparen) -> prPrec i 2 (concatD [render "extract" ; prtOpenParen 0 openparen ; prtIntVal 0 intval1 ; render "," ; prtIntVal 0 intval2 ; render "," ; prtExpr 0 expr ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Expr_Concat (openparen, exprs, closeparen) -> prPrec i 2 (concatD [render "bvconcat" ; prtOpenParen 0 openparen ; prtExprListBNFC 0 exprs ; prtCloseParen 0 closeparen])
+  |    AbsBasilIR.Expr_FSet (openparen, str, expr1, expr2, closeparen) -> prPrec i 2 (concatD [render "fset" ; prtOpenParen 0 openparen ; prtStr 0 str ; render "," ; prtExpr 0 expr1 ; render "," ; prtExpr 0 expr2 ; prtCloseParen 0 closeparen])
+  |    AbsBasilIR.Expr_FAccess (openparen, str, expr, closeparen) -> prPrec i 2 (concatD [render "faccess" ; prtOpenParen 0 openparen ; prtStr 0 str ; render "," ; prtExpr 0 expr ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Expr_Match (expr, openparen, cases, closeparen) -> prPrec i 2 (concatD [render "match" ; prtExpr 0 expr ; render "with" ; prtOpenParen 0 openparen ; prtCaseListBNFC 0 cases ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Expr_Cases (openparen, cases, closeparen) -> prPrec i 2 (concatD [render "cases" ; prtOpenParen 0 openparen ; prtCaseListBNFC 0 cases ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Expr_Paren (openparen, expr, closeparen) -> prPrec i 2 (concatD [prtOpenParen 0 openparen ; prtExpr 0 expr ; prtCloseParen 0 closeparen])
@@ -440,6 +471,7 @@ and prtBinOp (i:int) (e : AbsBasilIR.binOp) : doc = match e with
   |    AbsBasilIR.BinOpIntLogicalBinOp intlogicalbinop -> prPrec i 0 (concatD [prtIntLogicalBinOp 0 intlogicalbinop])
   |    AbsBasilIR.BinOpIntBinOp intbinop -> prPrec i 0 (concatD [prtIntBinOp 0 intbinop])
   |    AbsBasilIR.BinOpEqOp eqop -> prPrec i 0 (concatD [prtEqOp 0 eqop])
+  |    AbsBasilIR.BinOpPointerBinOp pointerbinop -> prPrec i 0 (concatD [prtPointerBinOp 0 pointerbinop])
 
 
 and prtUnOp (i:int) (e : AbsBasilIR.unOp) : doc = match e with
@@ -522,6 +554,10 @@ and prtBoolBinOp (i:int) (e : AbsBasilIR.boolBinOp) : doc = match e with
   |    AbsBasilIR.BoolBinOp_boolimplies  -> prPrec i 0 (concatD [render "boolimplies"])
 
 
+and prtPointerBinOp (i:int) (e : AbsBasilIR.pointerBinOp) : doc = match e with
+       AbsBasilIR.PointerBinOp_ptradd  -> prPrec i 0 (concatD [render "ptradd"])
+
+
 and prtRequireTok (i:int) (e : AbsBasilIR.requireTok) : doc = match e with
        AbsBasilIR.RequireTok_require  -> prPrec i 0 (concatD [render "require"])
   |    AbsBasilIR.RequireTok_requires  -> prPrec i 0 (concatD [render "requires"])
diff --git a/lib/fe/ShowBasilIR.ml b/lib/fe/ShowBasilIR.ml
index d3d0cc0e..cd9e5579 100644
--- a/lib/fe/ShowBasilIR.ml
+++ b/lib/fe/ShowBasilIR.ml
@@ -1,4 +1,4 @@
-(* File generated by the BNF Converter (bnfc 2.9.6.2). *)
+(* File generated by the BNF Converter (bnfc 2.9.6.1). *)
 
 (* show functions *)
 
@@ -41,6 +41,7 @@ let showFloat (f:float) : showable = s2s (string_of_float f)
 let rec showBVTYPE (AbsBasilIR.BVTYPE (_,i)) : showable = s2s "BVTYPE " >> showString i
 let rec showINTTYPE (AbsBasilIR.INTTYPE (_,i)) : showable = s2s "INTTYPE " >> showString i
 let rec showBOOLTYPE (AbsBasilIR.BOOLTYPE (_,i)) : showable = s2s "BOOLTYPE " >> showString i
+let rec showPOINTERTYPE (AbsBasilIR.POINTERTYPE (_,i)) : showable = s2s "POINTERTYPE " >> showString i
 let rec showBIdent (AbsBasilIR.BIdent (_,i)) : showable = s2s "BIdent " >> showString i
 let rec showLocalIdent (AbsBasilIR.LocalIdent (_,i)) : showable = s2s "LocalIdent " >> showString i
 let rec showGlobalIdent (AbsBasilIR.GlobalIdent (_,i)) : showable = s2s "GlobalIdent " >> showString i
@@ -93,6 +94,10 @@ and showProcDef (e : AbsBasilIR.procDef) : showable = match e with
   |    AbsBasilIR.ProcDef_Some (beginlist, blocks, endlist) -> s2s "ProcDef_Some" >> c2s ' ' >> c2s '(' >> showBeginList beginlist  >> s2s ", " >>  showList showBlock blocks  >> s2s ", " >>  showEndList endlist >> c2s ')'
 
 
+and showField (e : AbsBasilIR.field) : showable = match e with
+       AbsBasilIR.Field1 (openparen, str, type', closeparen) -> s2s "Field1" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showStr str  >> s2s ", " >>  showTypeT type'  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
+
+
 and showIntType (e : AbsBasilIR.intType) : showable = match e with
        AbsBasilIR.IntType1 inttype -> s2s "IntType1" >> c2s ' ' >> c2s '(' >> showINTTYPE inttype >> c2s ')'
 
@@ -101,6 +106,14 @@ and showBoolType (e : AbsBasilIR.boolType) : showable = match e with
        AbsBasilIR.BoolType1 booltype -> s2s "BoolType1" >> c2s ' ' >> c2s '(' >> showBOOLTYPE booltype >> c2s ')'
 
 
+and showRecordType (e : AbsBasilIR.recordType) : showable = match e with
+       AbsBasilIR.RecordType1 (beginrec, fields, endrec) -> s2s "RecordType1" >> c2s ' ' >> c2s '(' >> showBeginRec beginrec  >> s2s ", " >>  showList showField fields  >> s2s ", " >>  showEndRec endrec >> c2s ')'
+
+
+and showPointerType (e : AbsBasilIR.pointerType) : showable = match e with
+       AbsBasilIR.PointerType1 (openparen, type'0, type', closeparen) -> s2s "PointerType1" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showTypeT type'0  >> s2s ", " >>  showTypeT type'  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
+
+
 and showBVType (e : AbsBasilIR.bVType) : showable = match e with
        AbsBasilIR.BVType1 bvtype -> s2s "BVType1" >> c2s ' ' >> c2s '(' >> showBVTYPE bvtype >> c2s ')'
 
@@ -122,8 +135,10 @@ and showTypeT (e : AbsBasilIR.typeT) : showable = match e with
        AbsBasilIR.TypeIntType inttype -> s2s "TypeIntType" >> c2s ' ' >> c2s '(' >> showIntType inttype >> c2s ')'
   |    AbsBasilIR.TypeBoolType booltype -> s2s "TypeBoolType" >> c2s ' ' >> c2s '(' >> showBoolType booltype >> c2s ')'
   |    AbsBasilIR.TypeBVType bvtype -> s2s "TypeBVType" >> c2s ' ' >> c2s '(' >> showBVType bvtype >> c2s ')'
+  |    AbsBasilIR.TypePointerType pointertype -> s2s "TypePointerType" >> c2s ' ' >> c2s '(' >> showPointerType pointertype >> c2s ')'
+  |    AbsBasilIR.TypeRecordType recordtype -> s2s "TypeRecordType" >> c2s ' ' >> c2s '(' >> showRecordType recordtype >> c2s ')'
+  |    AbsBasilIR.TypeVarType localident -> s2s "TypeVarType" >> c2s ' ' >> c2s '(' >> showLocalIdent localident >> c2s ')'
   |    AbsBasilIR.TypeParen (openparen, type', closeparen) -> s2s "TypeParen" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showTypeT type'  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
-  |    AbsBasilIR.TypeSort localident -> s2s "TypeSort" >> c2s ' ' >> c2s '(' >> showLocalIdent localident >> c2s ')'
   |    AbsBasilIR.TypeMapType maptype -> s2s "TypeMapType" >> c2s ' ' >> c2s '(' >> showMapType maptype >> c2s ')'
 
 
@@ -136,6 +151,10 @@ and showBVVal (e : AbsBasilIR.bVVal) : showable = match e with
        AbsBasilIR.BVVal1 (intval, bvtype) -> s2s "BVVal1" >> c2s ' ' >> c2s '(' >> showIntVal intval  >> s2s ", " >>  showBVType bvtype >> c2s ')'
 
 
+and showFieldVal (e : AbsBasilIR.fieldVal) : showable = match e with
+       AbsBasilIR.FieldVal1 (openparen, str, bvval, type', closeparen) -> s2s "FieldVal1" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showStr str  >> s2s ", " >>  showBVVal bvval  >> s2s ", " >>  showTypeT type'  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
+
+
 and showEndian (e : AbsBasilIR.endian) : showable = match e with
        AbsBasilIR.Endian_Little  -> s2s "Endian_Little"
   |    AbsBasilIR.Endian_Big  -> s2s "Endian_Big"
@@ -263,6 +282,8 @@ and showParams (e : AbsBasilIR.params) : showable = match e with
 and showValue (e : AbsBasilIR.value) : showable = match e with
        AbsBasilIR.Value_BV bvval -> s2s "Value_BV" >> c2s ' ' >> c2s '(' >> showBVVal bvval >> c2s ')'
   |    AbsBasilIR.Value_Int intval -> s2s "Value_Int" >> c2s ' ' >> c2s '(' >> showIntVal intval >> c2s ')'
+  |    AbsBasilIR.Value_Record (openparen, fieldvals, closeparen) -> s2s "Value_Record" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showList showFieldVal fieldvals  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
+  |    AbsBasilIR.Value_Pointer (openparen, bvval, pointertype, closeparen) -> s2s "Value_Pointer" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showBVVal bvval  >> s2s ", " >>  showPointerType pointertype  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Value_True  -> s2s "Value_True"
   |    AbsBasilIR.Value_False  -> s2s "Value_False"
 
@@ -285,6 +306,8 @@ and showExpr (e : AbsBasilIR.expr) : showable = match e with
   |    AbsBasilIR.Expr_SignExtend (openparen, intval, expr, closeparen) -> s2s "Expr_SignExtend" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showIntVal intval  >> s2s ", " >>  showExpr expr  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Expr_Extract (openparen, intval0, intval, expr, closeparen) -> s2s "Expr_Extract" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showIntVal intval0  >> s2s ", " >>  showIntVal intval  >> s2s ", " >>  showExpr expr  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Expr_Concat (openparen, exprs, closeparen) -> s2s "Expr_Concat" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showList showExpr exprs  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
+  |    AbsBasilIR.Expr_FSet (openparen, str, expr0, expr, closeparen) -> s2s "Expr_FSet" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showStr str  >> s2s ", " >>  showExpr expr0  >> s2s ", " >>  showExpr expr  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
+  |    AbsBasilIR.Expr_FAccess (openparen, str, expr, closeparen) -> s2s "Expr_FAccess" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showStr str  >> s2s ", " >>  showExpr expr  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Expr_Match (expr, openparen, cases, closeparen) -> s2s "Expr_Match" >> c2s ' ' >> c2s '(' >> showExpr expr  >> s2s ", " >>  showOpenParen openparen  >> s2s ", " >>  showList showCase cases  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Expr_Cases (openparen, cases, closeparen) -> s2s "Expr_Cases" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showList showCase cases  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Expr_Paren (openparen, expr, closeparen) -> s2s "Expr_Paren" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showExpr expr  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
@@ -300,6 +323,7 @@ and showBinOp (e : AbsBasilIR.binOp) : showable = match e with
   |    AbsBasilIR.BinOpIntLogicalBinOp intlogicalbinop -> s2s "BinOpIntLogicalBinOp" >> c2s ' ' >> c2s '(' >> showIntLogicalBinOp intlogicalbinop >> c2s ')'
   |    AbsBasilIR.BinOpIntBinOp intbinop -> s2s "BinOpIntBinOp" >> c2s ' ' >> c2s '(' >> showIntBinOp intbinop >> c2s ')'
   |    AbsBasilIR.BinOpEqOp eqop -> s2s "BinOpEqOp" >> c2s ' ' >> c2s '(' >> showEqOp eqop >> c2s ')'
+  |    AbsBasilIR.BinOpPointerBinOp pointerbinop -> s2s "BinOpPointerBinOp" >> c2s ' ' >> c2s '(' >> showPointerBinOp pointerbinop >> c2s ')'
 
 
 and showUnOp (e : AbsBasilIR.unOp) : showable = match e with
@@ -379,6 +403,10 @@ and showBoolBinOp (e : AbsBasilIR.boolBinOp) : showable = match e with
   |    AbsBasilIR.BoolBinOp_boolimplies  -> s2s "BoolBinOp_boolimplies"
 
 
+and showPointerBinOp (e : AbsBasilIR.pointerBinOp) : showable = match e with
+       AbsBasilIR.PointerBinOp_ptradd  -> s2s "PointerBinOp_ptradd"
+
+
 and showRequireTok (e : AbsBasilIR.requireTok) : showable = match e with
        AbsBasilIR.RequireTok_require  -> s2s "RequireTok_require"
   |    AbsBasilIR.RequireTok_requires  -> s2s "RequireTok_requires"
diff --git a/lib/fe/SkelBasilIR.ml b/lib/fe/SkelBasilIR.ml
index ddc2b377..06a8175f 100644
--- a/lib/fe/SkelBasilIR.ml
+++ b/lib/fe/SkelBasilIR.ml
@@ -1,4 +1,4 @@
-(* File generated by the BNF Converter (bnfc 2.9.6.2). *)
+(* File generated by the BNF Converter (bnfc 2.9.6.1). *)
 
 module SkelBasilIR = struct
 
@@ -20,6 +20,10 @@ and transBOOLTYPE (x : bOOLTYPE) : result = match x with
     BOOLTYPE string -> failure x
 
 
+and transPOINTERTYPE (x : pOINTERTYPE) : result = match x with
+    POINTERTYPE string -> failure x
+
+
 and transBIdent (x : bIdent) : result = match x with
     BIdent string -> failure x
 
@@ -113,6 +117,10 @@ and transProcDef (x : procDef) : result = match x with
   | ProcDef_Some (beginlist, blocks, endlist) -> failure x
 
 
+and transField (x : field) : result = match x with
+    Field1 (openparen, str, type', closeparen) -> failure x
+
+
 and transIntType (x : intType) : result = match x with
     IntType1 inttype -> failure x
 
@@ -121,6 +129,14 @@ and transBoolType (x : boolType) : result = match x with
     BoolType1 booltype -> failure x
 
 
+and transRecordType (x : recordType) : result = match x with
+    RecordType1 (beginrec, fields, endrec) -> failure x
+
+
+and transPointerType (x : pointerType) : result = match x with
+    PointerType1 (openparen, type'0, type', closeparen) -> failure x
+
+
 and transBVType (x : bVType) : result = match x with
     BVType1 bvtype -> failure x
 
@@ -142,8 +158,10 @@ and transType (x : typeT) : result = match x with
     TypeIntType inttype -> failure x
   | TypeBoolType booltype -> failure x
   | TypeBVType bvtype -> failure x
+  | TypePointerType pointertype -> failure x
+  | TypeRecordType recordtype -> failure x
+  | TypeVarType localident -> failure x
   | TypeParen (openparen, type', closeparen) -> failure x
-  | TypeSort localident -> failure x
   | TypeMapType maptype -> failure x
 
 
@@ -156,6 +174,10 @@ and transBVVal (x : bVVal) : result = match x with
     BVVal1 (intval, bvtype) -> failure x
 
 
+and transFieldVal (x : fieldVal) : result = match x with
+    FieldVal1 (openparen, str, bvval, type', closeparen) -> failure x
+
+
 and transEndian (x : endian) : result = match x with
     Endian_Little  -> failure x
   | Endian_Big  -> failure x
@@ -283,6 +305,8 @@ and transParams (x : params) : result = match x with
 and transValue (x : value) : result = match x with
     Value_BV bvval -> failure x
   | Value_Int intval -> failure x
+  | Value_Record (openparen, fieldvals, closeparen) -> failure x
+  | Value_Pointer (openparen, bvval, pointertype, closeparen) -> failure x
   | Value_True  -> failure x
   | Value_False  -> failure x
 
@@ -305,6 +329,8 @@ and transExpr (x : expr) : result = match x with
   | Expr_SignExtend (openparen, intval, expr, closeparen) -> failure x
   | Expr_Extract (openparen, intval0, intval, expr, closeparen) -> failure x
   | Expr_Concat (openparen, exprs, closeparen) -> failure x
+  | Expr_FSet (openparen, str, expr0, expr, closeparen) -> failure x
+  | Expr_FAccess (openparen, str, expr, closeparen) -> failure x
   | Expr_Match (expr, openparen, cases, closeparen) -> failure x
   | Expr_Cases (openparen, cases, closeparen) -> failure x
   | Expr_Paren (openparen, expr, closeparen) -> failure x
@@ -320,6 +346,7 @@ and transBinOp (x : binOp) : result = match x with
   | BinOpIntLogicalBinOp intlogicalbinop -> failure x
   | BinOpIntBinOp intbinop -> failure x
   | BinOpEqOp eqop -> failure x
+  | BinOpPointerBinOp pointerbinop -> failure x
 
 
 and transUnOp (x : unOp) : result = match x with
@@ -399,6 +426,10 @@ and transBoolBinOp (x : boolBinOp) : result = match x with
   | BoolBinOp_boolimplies  -> failure x
 
 
+and transPointerBinOp (x : pointerBinOp) : result = match x with
+    PointerBinOp_ptradd  -> failure x
+
+
 and transRequireTok (x : requireTok) : result = match x with
     RequireTok_require  -> failure x
   | RequireTok_requires  -> failure x
diff --git a/lib/fe/TestBasilIR.ml b/lib/fe/TestBasilIR.ml
index e3da9490..db9dbc6e 100644
--- a/lib/fe/TestBasilIR.ml
+++ b/lib/fe/TestBasilIR.ml
@@ -1,4 +1,4 @@
-(* File generated by the BNF Converter (bnfc 2.9.6.2). *)
+(* File generated by the BNF Converter (bnfc 2.9.6.1). *)
 
 open Lexing
 
diff --git a/lib/lang/attrib.ml b/lib/lang/attrib.ml
index 196d30de..60c67410 100644
--- a/lib/lang/attrib.ml
+++ b/lib/lang/attrib.ml
@@ -10,6 +10,8 @@ type 'e t =
   | `Integer of Z.t
   | `CamlInt of int
   | `Bitvector of Bitvec.t
+  | `Record of Ops.Record.t
+  | `Pointer of Bitvec.t * Types.pointer
   | `List of 'e t list ]
 [@@deriving eq, ord]
 
@@ -25,6 +27,9 @@ let rec attrib_pretty ?(internal = [ location_key ]) pretty_expr (e : 'e t) :
   | `Bool b -> bool b
   | `Expr e -> pretty_expr e
   | `Bitvector bv -> text @@ Bitvec.to_string bv
+  | `Pointer (bv, typ) ->
+      text (String.cat (Bitvec.to_string bv) @@ Types.show_pointer typ)
+  | `Record record -> text @@ Ops.Record.to_string record
   | `Integer bv -> text @@ Z.to_string bv
   | `List s ->
       nest 2
diff --git a/lib/lang/expr.ml b/lib/lang/expr.ml
index 3ba9b12c..639973f3 100644
--- a/lib/lang/expr.ml
+++ b/lib/lang/expr.ml
@@ -358,6 +358,17 @@ module BasilExpr = struct
           [ text "sign_extend" ^ a ^ (textpf "(%d") bits; arg ^ text ")" ]
     | UnaryExpr { op = `Extract (hi, lo); arg = e } ->
         fill nil [ text "extract" ^ a ^ textpf "(%d,%d, " hi lo ^ e ^ text ")" ]
+    | UnaryExpr { op = `FACCESS offset; arg } ->
+        fill
+          (text "," ^ newline)
+          [ text "faccess" ^ a ^ (textpf "(\"%s\"") offset; arg ^ text ")" ]
+    | BinaryExpr { op = `FSET offset; arg1; arg2 } ->
+        fill
+          (text "," ^ newline)
+          [
+            text "fset" ^ a ^ (textpf "(\"%s\"") offset;
+            arg1 ^ text ", " ^ arg2 ^ text ")";
+          ]
     | UnaryExpr { op; arg = e } ->
         text (AllOps.to_string op) ^ a ^ bracket "(" e ")"
     | BinaryExpr { op = `Load (endian, bits); arg1; arg2 } ->
@@ -544,6 +555,12 @@ module BasilExpr = struct
   let zero_extend ?attrib ~n_prefix_bits (e : t) : t =
     unexp ?attrib ~op:(`ZeroExtend n_prefix_bits) e
 
+  let fset ?attrib ~(offset : string) (record : t) (e : t) : t =
+    binexp ?attrib ~op:(`FSET offset) record e
+
+  let faccess ?attrib ~(offset : string) (record : t) : t =
+    unexp ?attrib ~op:(`FACCESS offset) record
+
   let sign_extend ?attrib ~n_prefix_bits (e : t) : t =
     unexp ?attrib ~op:(`SignExtend n_prefix_bits) e
 
diff --git a/lib/lang/expr_eval.ml b/lib/lang/expr_eval.ml
index 9867eceb..7eb45b14 100644
--- a/lib/lang/expr_eval.ml
+++ b/lib/lang/expr_eval.ml
@@ -7,8 +7,12 @@ let eval_expr_alg (e : Ops.AllOps.const option BasilExpr.abstract_expr) =
   let bool e = Some (`Bool e) in
   let bv e = `Bitvector e in
   let z e = Some (`Integer e) in
+  let record e = Some (`Record e) in
+  let pointer e = Some (`Pointer e) in
 
   let get_bv = function Some (`Bitvector b) -> Some b | _ -> None in
+  let get_record = function Some (`Record b) -> Some b | _ -> None in
+  let get_pointer = function Some (`Pointer b) -> Some b | _ -> None in
   let get_bool = function Some (`Bool b) -> Some b | _ -> None in
   let get_int = function Some (`Integer b) -> Some b | _ -> None in
 
@@ -33,6 +37,18 @@ let eval_expr_alg (e : Ops.AllOps.const option BasilExpr.abstract_expr) =
       get_bv b >|= BVOps.eval_unary_unif op >|= bv
   | UnaryExpr { op = #BVOps.unary_bool as op; arg = b } ->
       get_bool b >|= BVOps.eval_unary_bool op >|= bv
+  | BinaryExpr { op = `FSET offset; arg1 = a; arg2 = b } ->
+      let* a = get_record a in
+      let* b = get_bv b in
+      record (Record.set_field offset a b)
+  | UnaryExpr { op = `FACCESS offset; arg = a } ->
+      let* a = get_record a in
+      let { value; _ } : Record.field = Record.get_field offset a in
+      Some (bv value)
+  | BinaryExpr { op = `PTRADD; arg1 = a; arg2 = b } ->
+      let* a, typ = get_pointer a in
+      let* b = get_bv b in
+      pointer (BVOps.eval_binary_unif `BVADD a b, typ)
   | BinaryExpr { op = #BVOps.binary_unif as op; arg1 = a; arg2 = b } ->
       let* a = get_bv a in
       let* b = get_bv b in
diff --git a/lib/lang/interp.ml b/lib/lang/interp.ml
index dd732895..73b44193 100644
--- a/lib/lang/interp.ml
+++ b/lib/lang/interp.ml
@@ -34,6 +34,12 @@ module IValue = struct
     | `Integer v -> Bitvec.create ~size:int_size v
     | `Bool true -> Bitvec.create ~size:8 Z.one
     | `Bool false -> Bitvec.create ~size:8 Z.zero
+    | `Pointer (bv, _) -> bv
+    | `Record fields ->
+        StringMap.fold
+          (fun _ ({ value; _ } : Ops.Record.field) acc ->
+            Bitvec.concat acc value)
+          fields Bitvec.empty
 
   let of_constant (v : Ops.AllOps.const) =
     let open Expr.BasilExpr in
@@ -42,6 +48,8 @@ module IValue = struct
     | `Bitvector bv -> bv_value bv
     | `Integer v -> int_value v
     | `Bool b -> if b then true_value else false_value
+    | `Pointer (bv, _) -> bv_value bv
+    | `Record fields -> bv_value @@ bv_of_constant v
 
   (** conversion to basil values *)
 
diff --git a/lib/lang/ops.ml b/lib/lang/ops.ml
index 7f18a0f5..de25d802 100644
--- a/lib/lang/ops.ml
+++ b/lib/lang/ops.ml
@@ -1,6 +1,33 @@
 open Common
 open Containers
 
+module Record = struct
+  type t = field StringMap.t [@@deriving eq, ord]
+  and field = { value : Bitvec.t; typ : Types.t }
+
+  let get_field offset record : field =
+    match StringMap.find_opt offset record with
+    | None -> failwith @@ "No field at offset " ^ offset
+    | Some f -> f
+
+  let set_field offset record value =
+    let { typ; _ } = get_field offset record in
+    StringMap.add offset { typ; value } record
+
+  let show_field { value; typ } =
+    Printf.sprintf "(%s, %s)" (Bitvec.to_string value) @@ Types.to_string typ
+
+  let show (record : t) =
+    "{"
+    ^ (StringMap.bindings record
+      |> List.map (fun (k, v) -> "(\"" ^ k ^ "\": " ^ show_field v ^ ")")
+      |> String.concat ", ")
+    ^ "}"
+
+  let to_string v = show v
+  let pp fmt b = Format.pp_print_string fmt (show b)
+end
+
 module Maps = struct
   (* map, value -> result *)
 
@@ -194,6 +221,40 @@ module IntOps = struct
     | #binary as b -> show_binary b
 end
 
+module RecordOps = struct
+  type const = [ `Record of Record.t ]
+  [@@deriving show { with_path = false }, eq, ord]
+
+  type unary = [ `FACCESS of string ]
+  [@@deriving show { with_path = false }, eq, ord]
+
+  type binary = [ `FSET of string ]
+  [@@deriving show { with_path = false }, eq, ord]
+
+  let eval_unary (u : unary) record =
+    match u with
+    | `FACCESS offset ->
+        let { value; _ } : Record.field = Record.get_field offset record in
+        value
+
+  let eval_binary (u : binary) =
+    match u with `FSET offset -> Record.set_field offset
+
+  let show = function
+    | #unary as u -> show_unary u
+    | #binary as b -> show_binary b
+end
+
+module PointerOps = struct
+  type const = [ `Pointer of Bitvec.t * Types.pointer ]
+  [@@deriving show { with_path = false }, eq, ord]
+
+  type binary = [ `PTRADD ] [@@deriving show { with_path = false }, eq, ord]
+
+  let eval_binary (u : binary) (bv, _) = match u with `PTRADD -> Bitvec.add bv
+  let show = function #binary as u -> show_binary u
+end
+
 module Spec = struct
   type endian = [ `Big | `Little ]
   [@@deriving show { with_path = false }, eq, ord]
@@ -217,14 +278,29 @@ module Spec = struct
 end
 
 module AllOps = struct
-  type const = [ IntOps.const | BVOps.const | LogicalOps.const ]
+  type const =
+    [ IntOps.const
+    | BVOps.const
+    | LogicalOps.const
+    | RecordOps.const
+    | PointerOps.const ]
   [@@deriving show { with_path = false }, eq, ord]
 
-  type unary = [ IntOps.unary | BVOps.unary | Spec.unary | LogicalOps.unary ]
+  type unary =
+    [ IntOps.unary
+    | BVOps.unary
+    | Spec.unary
+    | LogicalOps.unary
+    | RecordOps.unary ]
   [@@deriving show { with_path = false }, eq, ord]
 
   type binary =
-    [ IntOps.binary | BVOps.binary | LogicalOps.binary | Spec.binary ]
+    [ IntOps.binary
+    | BVOps.binary
+    | LogicalOps.binary
+    | Spec.binary
+    | RecordOps.binary
+    | PointerOps.binary ]
   [@@deriving show { with_path = false }, eq, ord]
 
   type intrin = [ BVOps.intrin | LogicalOps.intrin | Spec.intrin ]
@@ -243,6 +319,11 @@ module AllOps = struct
     | `Bool _ -> return Boolean
     | `Integer _ -> return Integer
     | `Bitvector v -> return (Bitvector (Bitvec.size v))
+    | `Pointer (v, ty) -> return (Pointer ty)
+    | `Record fields ->
+        return
+        @@ Record
+             (StringMap.map (fun ({ value; typ } : Record.field) -> typ) fields)
 
   let ret_type_unary (o : [< unary ]) a =
     let open Types in
@@ -256,6 +337,7 @@ module AllOps = struct
         match a with
         | Bitvector s -> return @@ Bitvector (sz + s)
         | o -> Conflict [ (o, "<bitvector") ])
+    | `FACCESS offset -> return @@ get_field offset a
     | `Forall -> return Boolean
     | `BVNEG -> return a
     | `INTNEG -> return Integer
@@ -288,6 +370,8 @@ module AllOps = struct
     | `BVAND | `BVOR | `BVADD | `BVMUL | `BVUDIV | `BVUREM | `BVSHL | `BVLSHR
     | `BVNAND | `BVXOR | `BVSUB | `BVSDIV | `BVSREM | `BVSMOD | `BVASHR ->
         return l
+    | `FSET _ -> return r
+    | `PTRADD -> return l
     | `MapAccess ->
         let m, r = Types.uncurry l in
         return r
@@ -346,6 +430,9 @@ module AllOps = struct
     | `Exists -> "exists"
     | `SignExtend n -> Printf.sprintf "sign_extend_%d" n
     | `ZeroExtend n -> Printf.sprintf "zero_extend_%d" n
+    | `FSET offset -> Printf.sprintf "fset_%s" offset
+    | `FACCESS offset -> Printf.sprintf "asdfaccess_%s" offset
+    | `PTRADD -> "ptradd"
     | `EQ -> "eq"
     | `INTADD -> "intadd"
     | `BVNAND -> "bvnand"
@@ -363,6 +450,10 @@ module AllOps = struct
     | `BVAND -> "bvand"
     | `INTMUL -> "intmul"
     | `Bitvector z -> Bitvec.to_string z
+    | `Pointer (value, typ) ->
+        Printf.sprintf "ptr(%s, %s)" (Bitvec.show value)
+          (Types.show_pointer typ)
+    | `Record record -> Record.to_string record
     | `BVSMOD -> "bvsmod"
     | `INTLT -> "intlt"
     | `IMPLIES -> "implies"
diff --git a/lib/loadir.ml b/lib/loadir.ml
index 438c18bb..5dc8999a 100644
--- a/lib/loadir.ml
+++ b/lib/loadir.ml
@@ -437,6 +437,16 @@ module BasilASTLoader = struct
     | RecordField1 (id, ty) ->
         Types.mk_field (unsafe_unsigil (`Local id)) (trans_type ty)
 
+  and transRECORDTYPE (fields : field list) =
+    Types.Record
+      (StringMap.of_list
+         ((List.map (function Field1 (_, offset, t, _) ->
+              (transStr offset, trans_type t)))
+            fields))
+
+  and transPOINTERTYPE (l : typeT) (u : typeT) =
+    Types.Pointer { lower = trans_type l; upper = trans_type u }
+
   and trans_type (x : typeT) : Types.t =
     match x with
     | TypeIntType inttype -> Integer
@@ -444,7 +454,9 @@ module BasilASTLoader = struct
     | TypeMapType maptype -> transMapType maptype
     | TypeBVType (BVType1 bvtype) -> transBVTYPE bvtype
     | TypeParen (_, typeT, _) -> trans_type typeT
-    | TypeSort t -> Types.Sort (unsafe_unsigil (`Local t), [])
+    | TypeVarType name -> Types.Variable (unsafe_unsigil (`Local name))
+    | TypeRecordType (RecordType1 (_, fields, _)) -> transRECORDTYPE fields
+    | TypePointerType (PointerType1 (_, l, u, _)) -> transPOINTERTYPE l u
 
   and transIntVal (x : intVal) : PrimInt.t =
     match x with
@@ -857,6 +869,18 @@ module BasilASTLoader = struct
     | Value_Int intval -> `Integer (transIntVal intval)
     | Value_True -> `Bool true
     | Value_False -> `Bool false
+    | Value_Pointer (_, v, PointerType1 (_, l, u, _), _) ->
+        `Pointer (trans_bv_val v, { lower = trans_type l; upper = trans_type u })
+    | Value_Record (_, fields, _) ->
+        `Record
+          (StringMap.of_list
+             (List.map
+                (function
+                  | FieldVal1 (_, offset, value, typ, _) ->
+                      ( transStr offset,
+                        ({ value = trans_bv_val value; typ = trans_type typ }
+                          : Ops.Record.field) ))
+                fields))
 
   and unsafe_unsigil g : string =
     match g with
@@ -965,6 +989,12 @@ module BasilASTLoader = struct
           ~hi_excl:(transIntVal ival0 |> Z.to_int)
           ~lo_incl:(transIntVal intval |> Z.to_int)
           (trans_expr expr)
+    | Expr_FAccess (o, offset, record, c) ->
+        BasilExpr.faccess ~attrib:(expr_range_attr o c)
+          ~offset:(transStr offset) (trans_expr record)
+    | Expr_FSet (o, offset, record, expr, c) ->
+        BasilExpr.fset ~attrib:(expr_range_attr o c) ~offset:(transStr offset)
+          (trans_expr record) (trans_expr expr)
     | Expr_LoadLe (o, intval, a1, a2, c) ->
         BasilExpr.load ~attrib:(expr_range_attr o c)
           ~bits:(Z.to_int @@ transIntVal intval)
@@ -1014,6 +1044,7 @@ module BasilASTLoader = struct
         transIntLogicalBinOp intlogicalbinop
     | BinOpIntBinOp intbinop -> transIntBinOp intbinop
     | BinOpEqOp equop -> transEqOp equop
+    | BinOpPointerBinOp pointerBinOp -> transPointerBinOp pointerBinOp
 
   and transUnOp (x : BasilIR.AbsBasilIR.unOp) =
     match x with
@@ -1069,6 +1100,9 @@ module BasilASTLoader = struct
     | IntBinOp_intdiv -> `INTDIV
     | IntBinOp_intmod -> `INTMOD
 
+  and transPointerBinOp (x : pointerBinOp) =
+    match x with PointerBinOp_ptradd -> `PTRADD
+
   and transIntLogicalBinOp (x : intLogicalBinOp) =
     match x with
     | IntLogicalBinOp_intlt -> `INTLT
diff --git a/lib/transforms/type_check.ml b/lib/transforms/type_check.ml
index 86ea006c..224cec71 100644
--- a/lib/transforms/type_check.ml
+++ b/lib/transforms/type_check.ml
@@ -27,6 +27,12 @@ let type_check stmt_id block_id expr =
     match op with
     | `Classification -> []
     | `Gamma -> []
+    | `Old -> []
+    | `Forall | `Exists | `Lambda -> []
+    | `FACCESS _ -> (
+        match arg with
+        | Record _ -> []
+        | _ -> [ type_err "FACCESS body is not a record type" ])
     | `BoolNOT | `BOOLTOBV1 ->
         if Types.equal arg Types.Boolean then []
         else [ type_err "%s body is not a boolean" @@ AllOps.to_string op ]
@@ -49,8 +55,6 @@ let type_check stmt_id block_id expr =
                   @@ AllOps.to_string op;
                 ])
         | _ -> [ type_err "%s body is not a bitvector" @@ AllOps.to_string op ])
-    | `Old -> []
-    | `Forall | `Exists | `Lambda -> []
   in
 
   let check_binary (op : Ops.AllOps.binary) (arg1 : Types.t) (arg2 : Types.t) :
@@ -86,6 +90,33 @@ let type_check stmt_id block_id expr =
     let binary_bool_types = binary_same_types Types.Boolean in
     let open Ops in
     match op with
+    | `PTRADD -> (
+        let err =
+          match arg2 with
+          | Bitvector _ -> []
+          | _ ->
+              [ type_err "%s is not of bitvector type" @@ Types.to_string arg1 ]
+        in
+        match arg1 with
+        | Pointer _ -> err
+        | _ ->
+            err
+            @ [ type_err "%s is not of pointer type" @@ Types.to_string arg2 ])
+    | `FSET offset ->
+        let err =
+          match arg1 with
+          | Record _ -> []
+          | _ -> [ type_err "%s is not of record type" @@ Types.to_string arg1 ]
+        in
+        if
+          List.length err = 1
+          || (Types.equal arg2 @@ Types.get_field offset arg1)
+        then err
+        else
+          [
+            type_err "%s is not of %s type" (Types.to_string arg1)
+              (Types.to_string @@ Types.get_field offset arg1);
+          ]
     | `INTADD | `INTMUL | `INTSUB | `INTDIV | `INTMOD | `INTLT | `INTLE ->
         binary_int_types arg1 arg2
     | (`EQ | `NEQ) as op ->
diff --git a/lib/util/types.ml b/lib/util/types.ml
index 19e7d5a6..4b3f9f67 100644
--- a/lib/util/types.ml
+++ b/lib/util/types.ml
@@ -1,4 +1,5 @@
 open Containers
+module StringMap = Map.Make (String)
 
 (** This represents type right expressions (i.e. not declarations), we expand
     this in the future to allow declarations to be polymorphic.
@@ -33,10 +34,19 @@ type t =
   | Nothing
   | Map of t * t
   | Sort of string * variant list
+  | Record of t StringMap.t
+  | Pointer of pointer
+  | Variable of string (* Possibly a name of a type declartion *)
 
 and variant = { variant : string; fields : field list }
 and field = { field : string; typ : t } [@@deriving eq, ord]
 
+(*
+  Lower type represents types the pointer could load
+  Upper type represents types the pointer could store
+*)
+and pointer = { lower : t; upper : t } [@@deriving eq, ord]
+
 let bv i = Bitvector i
 let int = Integer
 let bool = Boolean
@@ -48,15 +58,18 @@ let bit_width = function Boolean -> Some 1 | Bitvector n -> Some n | _ -> None
 (** Get the type for an opaque sort *)
 let mk_sort name = Sort (name, [])
 
+(* ADT not Record type *)
 let mk_field field typ = { field; typ }
 let mk_variant name fields = { variant = name; fields }
 
 let mk_enum name (cases : string list) =
   Sort (name, List.map (fun variant -> { variant; fields = [] }) cases)
 
+(* ADT not Record type *)
 let mk_record name (fields : field list) =
   Sort (name, [ mk_variant ("Record" ^ name) fields ])
 
+(* ADT not Record type *)
 let record_field name t =
   match t with
   | Sort (sort_name, [ { variant; fields } ])
@@ -71,8 +84,16 @@ let mk_adt name (variants : (string * field list) list) =
   Sort
     (name, variants |> List.map (fun (variant, fields) -> { variant; fields }))
 
+let get_field field_name record : t =
+  match record with
+  | Record fields -> (
+      match StringMap.find_opt field_name fields with
+      | None -> failwith @@ "No field at offset " ^ field_name
+      | Some t -> t)
+  | _ -> failwith "Not record type"
+
 (*
-  Nothing < Unit < {boolean, integer, bitvector} < Top
+  Nothing < Unit < {boolean, integer, bitvector, record, pointer} < Top
   *)
 let rec compare_partial (a : t) (b : t) =
   match (a, b) with
@@ -84,13 +105,16 @@ let rec compare_partial (a : t) (b : t) =
   | _, Nothing -> Some 1
   | Unit, _ -> Some (-1)
   | _, Unit -> Some 1
-  | Boolean, Integer -> None
-  | Integer, Boolean -> None
-  | Boolean, Bitvector _ -> None
-  | Bitvector _, Boolean -> None
-  | Boolean, Boolean -> None
-  | Integer, Bitvector _ -> None
-  | Bitvector _, Integer -> None
+  | Pointer { lower; upper }, Pointer { lower = lower1; upper = upper1 } -> (
+      compare_partial lower lower1 |> function
+      | Some 0 -> compare_partial upper upper1
+      | o -> o)
+  | Record fields, Record fields2 ->
+      Some
+        (StringMap.compare
+           (fun a b ->
+             match compare_partial a b with Some a -> a | None -> -1)
+           fields fields2)
   | Bitvector a, Bitvector b -> Some (Int.compare a b)
   | Sort (n1, _), Sort (n2, _) -> if String.equal n1 n2 then Some 0 else None
   | Integer, Integer -> Some 0
@@ -118,6 +142,15 @@ let rec to_string = function
   | Unit -> "()"
   | Top -> "⊤"
   | Nothing -> "⊥"
+  | Variable name -> name
+  | Pointer { lower; upper } ->
+      Printf.sprintf "ptr(%s, %s)" (to_string lower) (to_string upper)
+  | Record record ->
+      "{"
+      ^ (StringMap.bindings record
+        |> List.map (fun (k, v) -> "(\"" ^ k ^ "\": " ^ to_string v ^ ")")
+        |> String.concat ", ")
+      ^ "}"
   | Map ((Map _ as a), (Map _ as b)) ->
       "(" ^ "(" ^ to_string a ^ ")" ^ "->" ^ "(" ^ to_string b ^ ")" ^ ")"
   | Map ((Map _ as a), b) ->
@@ -162,10 +195,18 @@ let%expect_test "dtp" =
   in
   print_endline @@ to_string lst;
   print_endline @@ to_string rc;
-  [%expect {|
+  [%expect
+    {|
     list = cons of {head: E; tail: list} | nil
     recs = Recordrecs of {a: bv12; b: bool}
     |}]
 
 let show (b : t) = to_string b
+
+let show_pointer { lower; upper } =
+  Printf.sprintf "{ lower = %s; upper = %s }" (show lower) (show upper)
+
 let pp fmt b = Format.pp_print_string fmt (show b)
+
+let pp_pointer fmt { lower; upper } =
+  Format.fprintf fmt "{ lower = %s; upper = %s }" (show lower) (show upper)
diff --git a/test/cram/dune b/test/cram/dune
index 0ce781a2..09509e42 100644
--- a/test/cram/dune
+++ b/test/cram/dune
@@ -15,6 +15,7 @@
   %{bin:bincaml}
   ssa-multi-deps.il
   memassign.il
+  ptrrec1.il
   ../../examples/irreducible_loop_1.il
   ../../examples/cat.il
   ../../examples/cntlm-output.il
diff --git a/test/cram/ptrrec1.il b/test/cram/ptrrec1.il
new file mode 100644
index 00000000..4ff0fb67
--- /dev/null
+++ b/test/cram/ptrrec1.il
@@ -0,0 +1,23 @@
+var $rec:{("0": bv32)};
+prog entry @main_4196164;
+proc @main_4196164(R0_in:bv64, R10_in:bv64, R11_in:bv64, R12_in:bv64, R13_in:bv64,
+   R14_in:bv64, R15_in:bv64, R16_in:bv64, R17_in:bv64, R18_in:bv64, R1_in:bv64,
+   R29_in:bv64, R2_in:bv64, R30_in:bv64, R31_in:bv64, R3_in:bv64, R4_in:bv64,
+   R5_in:bv64, R6_in:bv64, R7_in:bv64, R8_in:bv64, R9_in:bv64, _PC_in:bv64)
+   -> (R0_out:bv64, R1_out:bv64) { .address = 4196164; .name = "main";
+    .returnBlock = "main_return" }
+  modifies $rec:{("0": bv32)}
+  captures $rec:{("0": bv32)}
+
+[
+   block %main_entry [
+     var as:ptr(bv64, bv64) := ptradd(R31_in:bv64, R0_in:bv64);
+     var af:bv32 := faccess("0", $rec:{("0": bv32)});
+     $rec:{("0": bv32)} := fset("0", $rec:{("0": bv32)}, af:bv32);
+     goto (%main_return);
+   ];
+   block %main_return [
+     (var R0_out:bv64 := 0x0:bv64, var R1_out:bv64 := 0x2a:bv64);
+     return;
+   ]
+];
\ No newline at end of file
diff --git a/test/cram/roundtrip.sexp b/test/cram/roundtrip.sexp
index 8ae5bb5a..545d40b3 100644
--- a/test/cram/roundtrip.sexp
+++ b/test/cram/roundtrip.sexp
@@ -11,3 +11,8 @@
 (dump-il "beforemem.il")
 (load-il "beforemem.il")
 (dump-il "aftermem.il")
+
+(load-il "ptrrec1.il")
+(dump-il "ptrrec2.il")
+(load-il "ptrrec2.il")
+(dump-il "ptrrec3.il")
diff --git a/test/cram/roundtrip.t b/test/cram/roundtrip.t
index dc4a8888..f8eb95bc 100644
--- a/test/cram/roundtrip.t
+++ b/test/cram/roundtrip.t
@@ -32,4 +32,8 @@ The serialise -> parse serialise loop should be idempotent
 Memassign repr
 
   $ diff beforemem.il aftermem.il
+Record and Pointer
+
+  $ diff ptrrec1.il ptrrec2.il
+  $ diff ptrrec2.il ptrrec3.il