From a31b58cea45159999ae2ecdaa661490d29b6e3ab Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 5 Aug 2010 09:51:54 +0000 Subject: Applied patch submitted by Stefan Bucur that fixes a memory corruption bug in the internal version of MiniSAT. See http://llvm.org/bugs/show_bug.cgi?id=7677 for more details. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110325 91177308-0d34-0410-b5e6-96231b3b80d8 --- stp/sat/SolverTypes.h | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/stp/sat/SolverTypes.h b/stp/sat/SolverTypes.h index 29c3b95d..fe15a968 100644 --- a/stp/sat/SolverTypes.h +++ b/stp/sat/SolverTypes.h @@ -82,8 +82,12 @@ public: friend Clause* Clause_new(const V& ps, bool learnt = false) { assert(sizeof(Lit) == sizeof(uint)); assert(sizeof(float) == sizeof(uint)); - void* mem = xmalloc(sizeof(Clause) + - sizeof(uint)*(ps.size() - 1)); + + size_t aux_size = 0; + if (ps.size() > 0) + aux_size = sizeof(uint)*(ps.size() - 1); + + void* mem = xmalloc(sizeof(Clause) + aux_size); return new (mem) Clause(ps, learnt); } int size () const { return size_etc >> 3; } -- cgit 1.4.1