Skip to content

Commit 96f76cf

Browse files
committed
[refactor, fix, WIP] Writes all reports to a single file, supress compiler warnings for auto generated ID's of errors.
1 parent a8385a6 commit 96f76cf

3 files changed

Lines changed: 9 additions & 3 deletions

File tree

lib/Core/Executor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5700,7 +5700,7 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref<Expr> size,
57005700
Expr::Width pointerWidthInBits = Context::get().getPointerWidth();
57015701

57025702
/// Determine source for address array:
5703-
/// * LI source if allocate occures on lazi initialization
5703+
/// * LI source if allocate occures on lazy initialization
57045704
/// * Otherwise choose source depending on the allocation site
57055705
ref<SymbolicSource> sourceAddressArray;
57065706
if (!lazyInitializationSource) {

test/Feature/SymbolicSizes/FirstAndLastElements.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
22
// RUN: rm -rf %t.klee-out
3-
// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s
3+
// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --use-merged-pointer-dereference=true --max-sym-alloc=128 %t1.bc 2>&1 | FileCheck %s
44

55
#include "klee/klee.h"
66
#include <assert.h>

tools/klee/main.cpp

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -568,6 +568,11 @@ SmallString<128> KleeHandler::getOutputDirectory() const {
568568
static std::vector<RuleJson> rules() {
569569
std::vector<RuleJson> ret;
570570
// Push back rules
571+
// Wtype-limits deprecated as I might be equal to 0.
572+
DISABLE_WARNING_PUSH
573+
// clang-format off
574+
DISABLE_WARNING(-Wtype-limits)
575+
// clang-format on
571576
#undef TTYPE
572577
#undef TTMARK
573578
#define TTYPE(N, I, S) \
@@ -578,6 +583,7 @@ static std::vector<RuleJson> rules() {
578583
#define TTMARK(N, I)
579584

580585
TERMINATION_TYPES;
586+
DISABLE_WARNING_POP
581587
return ret;
582588
};
583589

@@ -745,7 +751,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
745751
}
746752

747753
if (isError && WriteSARIFs) {
748-
auto f = openTestFile("sarif", id);
754+
auto f = openOutputFile("report.sarif");
749755

750756
// Rewrite .sarif each time it is updated to
751757
// receive results as they appear.

0 commit comments

Comments
 (0)