-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathstp.AddVcDeleteExprAndDecl.patch
More file actions
36 lines (33 loc) · 1.09 KB
/
stp.AddVcDeleteExprAndDecl.patch
File metadata and controls
36 lines (33 loc) · 1.09 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
Index: src/c_interface/c_interface.cpp
===================================================================
--- src/c_interface/c_interface.cpp (revision 1668)
+++ src/c_interface/c_interface.cpp (working copy)
@@ -1759,6 +1759,17 @@
delete input;
}
+void vc_DeleteExprAndDecl(Expr e) {
+ nodestar input = (nodestar)e;
+ for (size_t k = 0; k < decls->size(); ++k) {
+ if ((*decls)[k] == *input) {
+ decls->erase(decls->begin() + k);
+ break;
+ }
+ }
+ delete input;
+}
+
exprkind_t getExprKind(Expr e) {
nodestar input = (nodestar)e;
return (exprkind_t)(input->GetKind());
Index: src/c_interface/c_interface.h
===================================================================
--- src/c_interface/c_interface.h (revision 1668)
+++ src/c_interface/c_interface.h (working copy)
@@ -366,6 +366,9 @@
//deletes the expression e
void vc_DeleteExpr(Expr e);
+ //deletes the expression and removes it from the list of decls
+ void vc_DeleteExprAndDecl(Expr e);
+
//Get the whole counterexample from the current context
WholeCounterExample vc_getWholeCounterExample(VC vc);