From 3fd9be596e20664e62f8daf5ddabaa10d7b4de3f Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Wed, 29 Jan 2020 19:13:20 +0000 Subject: Enforce fork/branch limits in branch() and fix double termination * extend help messages for -max-memory and -max-memory-inhibit * introduces branchingPermitted() * enforces fork/branch limits in branch() (vector version) * changes main loop * calls updateStates() before checkMemoryUsage() * calls updateStates() again in case we early terminate states This should prevent double termination for now. Other solutions are imho more expensive as we would have to compare possibly large vectors of states (either states(arr) in checkMemoryUsage() or removedStates in terminateState()). --- test/Feature/MemoryLimit.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test') diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index 1cdf7260..e9635cab 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -9,14 +9,14 @@ // RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log // RUN: not grep -q "MALLOC FAILED" %t.little.log // RUN: not grep -q "DONE" %t.little.log -// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt +// RUN: grep "WARNING: killing 1 states (over memory cap" %t.klee-out/warnings.txt // RUN: %clang -emit-llvm -g -c %s -o %t.big.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.big.bc > %t.big.log 2> %t.big.err // RUN: not grep -q "MALLOC FAILED" %t.big.log // RUN: not grep -q "DONE" %t.big.log -// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt +// RUN: grep "WARNING: killing 1 states (over memory cap" %t.klee-out/warnings.txt #include #include -- cgit 1.4.1