Commit d3da5bf3 authored by Sergio Costas's avatar Sergio Costas

Now supports using a CRUST pointer "alone" in a comparison (it doesn't force...

Now supports using a CRUST pointer "alone" in a comparison (it doesn't force to use == NULL or != NULL)
parent b3a72935
......@@ -466,7 +466,7 @@ class crust(object):
return True
def _eval_statement(self, statement, thread_status, first):
def _eval_statement(self, statement, thread_status, first, is_conditional = False):
""" Evaluates an statement recursively.
@params:
statement -- the node with the statement to evaluate
......@@ -521,6 +521,12 @@ class crust(object):
if self._check_statement_is_crust(statement, vardata):
valuetype = self.TYPE_CRUST
pure = True
if (valuedata == self.VALUE_NOT_NULL_OR_NULL) and is_conditional:
var1 = self._copy_status(thread_status)
var2 = thread_status
self._set_var_value(var1, vardata["name"], crust.VALUE_NOT_NULL, 0, True)
self._set_var_value(var2, vardata["name"], crust.VALUE_NULL, 0, True)
return [ {"thread_status":var1, "value":self.VALUE_NOT_NULL, "type":valuetype, "condition":self.CONDITION_TRUE, "node":statement, "pure": True}, {"thread_status":var2, "value":self.VALUE_NULL, "type":valuetype, "condition":self.CONDITION_FALSE, "node":statement, "pure": True}]
else:
valuetype = self.TYPE_NO_CRUST
pure = True
......@@ -540,7 +546,7 @@ class crust(object):
if statement.type == "?":
threads = self._eval_statement(statement.condition[0], thread_status, False)
threads = self._eval_statement(statement.condition[0], thread_status, False, True)
retvals = []
for thread in threads:
if thread["condition"] == crust.CONDITION_FALSE_TRUE:
......@@ -874,7 +880,7 @@ class crust(object):
self._check_is_freed(thread_status, statement.child1[0])
self._check_is_freed(thread_status, statement.child2[0])
retvals = []
threads1 = self._eval_statement(statement.child1[0], thread_status, False)
threads1 = self._eval_statement(statement.child1[0], thread_status, False, True)
if statement.type == "EQ_OP":
sts1 = self.VALUE_NOT_NULL
cnd1 = self.CONDITION_TRUE
......@@ -886,7 +892,7 @@ class crust(object):
sts1 = self.VALUE_NULL
cnd1 = self.CONDITION_FALSE
for thread1 in threads1:
threads2 = self._eval_statement(statement.child2[0], thread1["thread_status"], False)
threads2 = self._eval_statement(statement.child2[0], thread1["thread_status"], False, True)
var_used = False
for thread2 in threads2:
if var_used:
......@@ -904,7 +910,7 @@ class crust(object):
return retvals
if (statement.type == "!") or (statement.type == "~"):
threads = self._eval_statement(statement.child1[0], thread_status, False)
threads = self._eval_statement(statement.child1[0], thread_status, False, True)
for thread in threads:
if thread["value"] == self.VALUE_NULL:
thread["value"] = self.VALUE_NOT_NULL
......@@ -1028,9 +1034,16 @@ class crust(object):
child1 = statement.child1
child2 = statement.child2
retvals = []
threads1 = self._eval_statement(statement.child1[0], thread_status, False)
if ((statement.type == "GE_OP") or
(statement.type == "LE_OP") or
(statement.type == "<") or
(statement.type == ">")):
is_comparison = True
else:
is_comparison = False
threads1 = self._eval_statement(statement.child1[0], thread_status, False, is_comparison)
for thread1 in threads1:
threads2 = self._eval_statement(statement.child2[0], thread1["thread_status"], False)
threads2 = self._eval_statement(statement.child2[0], thread1["thread_status"], False, is_comparison)
for thread2 in threads2:
if ((thread1["value"] == self.VALUE_FREED) or
(thread2["value"] == self.VALUE_FREED) or
......@@ -1043,23 +1056,23 @@ class crust(object):
return retvals
if statement.type == "AND_OP":
threads = self._eval_statement(statement.child1[0], thread_status, False)
threads = self._eval_statement(statement.child1[0], thread_status, False, True)
retval = []
for thread in threads:
if (thread["condition"] == self.CONDITION_FALSE) or (thread["condition"] == self.CONDITION_FALSE_TRUE):
retval.append(thread)
if (thread["condition"] == self.CONDITION_TRUE) or (thread["condition"] == self.CONDITION_FALSE_TRUE):
retval += self._eval_statement(statement.child2[0], self._copy_status(thread["thread_status"]), False)
retval += self._eval_statement(statement.child2[0], self._copy_status(thread["thread_status"]), False, True)
return retval
if statement.type == "OR_OP":
threads = self._eval_statement(statement.child1[0], thread_status, False)
threads = self._eval_statement(statement.child1[0], thread_status, False, True)
retval = []
for thread in threads:
if (thread["condition"] == self.CONDITION_TRUE) or (thread["condition"] == self.CONDITION_FALSE_TRUE):
retval.append(thread)
if (thread["condition"] == self.CONDITION_FALSE) or (thread["condition"] == self.CONDITION_FALSE_TRUE):
retval += self._eval_statement(statement.child2[0], self._copy_status(thread["thread_status"]), False)
retval += self._eval_statement(statement.child2[0], self._copy_status(thread["thread_status"]), False, True)
return retval
if statement.type == ",":
......@@ -1618,7 +1631,7 @@ class crust(object):
else:
block_true += block_other
block_false = block_other
options = self._eval_statement(node.condition[0], thread_status, False)
options = self._eval_statement(node.condition[0], thread_status, False, True)
retvals = []
status_true = {}
status_false = {}
......@@ -1826,7 +1839,7 @@ class crust(object):
return threads
if (node.type == "EVAL_TRUE") or (node.type == "EVAL_FALSE"):
threads = self._eval_statement(node.condition, self._copy_status(thread_status), False)
threads = self._eval_statement(node.condition, self._copy_status(thread_status), False, True)
retvals = []
for thread in threads:
if (node.type == "EVAL_TRUE") and (thread["condition"] == self.CONDITION_FALSE):
......
......@@ -970,6 +970,12 @@ class Test(unittest.TestCase):
def test232SetGlobalToNullInSeveralPaths(self):
self._all_fine_test("unitest/test232.c")
def test233CompareWithCrustPointerAlone(self):
self._all_fine_test("unitest/test233.c")
def test234CompareWithCrustPointerAlone2(self):
self._all_fine_test("unitest/test234.c")
if __name__ == '__main__':
try:
os.remove("error_list.txt")
......
typedef __crust__ unsigned char *crust_t;
void function(crust_t);
void main(crust_t p) {
if (p) {
function(p);
}
}
typedef __crust__ unsigned char *crust_t;
void function(crust_t);
void main(crust_t p) {
if (!p) {
int a = 5;
} else {
function(p);
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment