summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r--src/expr/node_manager.h6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7d2b13e4c..dcd7005f8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -332,7 +332,7 @@ class NodeManager {
/** Create a variable with the given type. */
Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
+
public:
explicit NodeManager(ExprManager* exprManager);
@@ -486,6 +486,10 @@ public:
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
+
+ /** Create nil reference for separation logic with the given type. */
+ Node mkSepNil(const TypeNode& type);
+ Node* mkSepNilPtr(const TypeNode& type);
/** Make a new abstract value with the given type. */
Node mkAbstractValue(const TypeNode& type);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback