projects
/
satcheck.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
fix spacing with make tabbing
[satcheck.git]
/
eprecord.cc
diff --git
a/eprecord.cc
b/eprecord.cc
index 10b4537980e28b9173fddd07bc22ce9ca7fa0366..a87167eacd546be5d87c7c856324b87ce2630bf6 100644
(file)
--- a/
eprecord.cc
+++ b/
eprecord.cc
@@
-132,13
+132,13
@@
IntHashSet * EPRecord::getReturnValueSet() {
void EPRecord::print(int f) {
if (event==RMW) {
if (op==ADD)
void EPRecord::print(int f) {
if (event==RMW) {
if (op==ADD)
- dprintf(f, "add");
+
model_
dprintf(f, "add");
else if (op==EXC)
else if (op==EXC)
- dprintf(f, "exc");
+
model_
dprintf(f, "exc");
else
else
- dprintf(f, "cas");
+
model_
dprintf(f, "cas");
} else
} else
- dprintf(f, "%s",eventToStr(event));
+
model_
dprintf(f, "%s",eventToStr(event));
IntHashSet *i=NULL;
switch(event) {
case LOAD:
IntHashSet *i=NULL;
switch(event) {
case LOAD:
@@
-153,14
+153,14
@@
void EPRecord::print(int f) {
case FUNCTION: {
if (!getPhi()) {
CGoalIterator *cit=completed->iterator();
case FUNCTION: {
if (!getPhi()) {
CGoalIterator *cit=completed->iterator();
- dprintf(f, "{");
+
model_
dprintf(f, "{");
while(cit->hasNext()) {
CGoal *goal=cit->next();
while(cit->hasNext()) {
CGoal *goal=cit->next();
- dprintf(f,"(");
+
model_
dprintf(f,"(");
for(uint i=0;i<getNumFuncInputs();i++) {
for(uint i=0;i<getNumFuncInputs();i++) {
- dprintf(f,"%lu ", goal->getValue(i+VC_BASEINDEX));
+
model_
dprintf(f,"%lu ", goal->getValue(i+VC_BASEINDEX));
}
}
- dprintf(f,"=> %lu)", goal->getOutput());
+
model_
dprintf(f,"=> %lu)", goal->getOutput());
}
delete cit;
}
}
delete cit;
}
@@
-171,27
+171,27
@@
void EPRecord::print(int f) {
}
if (i!=NULL) {
IntIterator *it=i->iterator();
}
if (i!=NULL) {
IntIterator *it=i->iterator();
- dprintf(f, "{");
+
model_
dprintf(f, "{");
while(it->hasNext()) {
while(it->hasNext()) {
- dprintf(f, "%lu ", it->next());
+
model_
dprintf(f, "%lu ", it->next());
}
}
- dprintf(f, "}");
+
model_
dprintf(f, "}");
delete it;
}
for(uint i=0;i<numinputs;i++) {
IntIterator *it=setarray[i]->iterator();
delete it;
}
for(uint i=0;i<numinputs;i++) {
IntIterator *it=setarray[i]->iterator();
- dprintf(f,"{");
+
model_
dprintf(f,"{");
while(it->hasNext()) {
uint64_t v=it->next();
while(it->hasNext()) {
uint64_t v=it->next();
- dprintf(f,"%lu ", v);
+
model_
dprintf(f,"%lu ", v);
}
}
- dprintf(f,"}");
+
model_
dprintf(f,"}");
delete it;
}
delete it;
}
-
+
execpoint->print(f);
}
execpoint->print(f);
}