pool/klee
SHA256
11
0
Fork 2
Code Issues Pull Requests Activity

up to 2.2+20210510 & Switch to LLVM 12

Browse Source 
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=98
This commit is contained in:
Jiri Slaby
2021-05-20 08:31:32 +00:00
committed by Git OBS Bridge
parent 385eb48374
commit f4bb94e032
6 changed files with 105 additions and 56 deletions
Download Patch File Download Diff File Expand all files Collapse all files

117
FileCheck.cpp
View File

@@ -15,12 +15,12 @@
//
//===----------------------------------------------------------------------===//
#include "llvm/FileCheck/FileCheck.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/InitLLVM.h"
#include "llvm/Support/Process.h"
#include "llvm/Support/WithColor.h"
#include "llvm/Support/raw_ostream.h"
#include "llvm/Support/FileCheck.h"
#include <cmath>
using namespace llvm;
@@ -77,6 +77,10 @@ static cl::opt<bool> AllowEmptyInput(
cl::desc("Allow the input file to be empty. This is useful when making\n"
"checks that some error message does not occur, for example."));
static cl::opt<bool> AllowUnusedPrefixes(
"allow-unused-prefixes", cl::init(true),
cl::desc("Allow prefixes to be specified but not appear in the test."));
static cl::opt<bool> MatchFullLines(
"match-full-lines", cl::init(false),
cl::desc("Require all positive matches to cover an entire input line.\n"
@@ -324,7 +328,7 @@ struct InputAnnotation {
};
/// Get an abbreviation for the check type.
std::string GetCheckTypeAbbreviation(Check::FileCheckType Ty) {
static std::string GetCheckTypeAbbreviation(Check::FileCheckType Ty) {
switch (Ty) {
case Check::CheckPlain:
if (Ty.getCount() > 1)
@@ -402,6 +406,18 @@ BuildInputAnnotations(const SourceMgr &SM, unsigned CheckFileBufferID,
LabelWidth = std::max((std::string::size_type)LabelWidth, A.Label.size());
A.Marker = GetMarker(DiagItr->MatchTy);
if (!DiagItr->Note.empty()) {
A.Marker.Note = DiagItr->Note;
// It's less confusing if notes that don't actually have ranges don't have
// markers. For example, a marker for 'with "VAR" equal to "5"' would
// seem to indicate where "VAR" matches, but the location we actually have
// for the marker simply points to the start of the match/search range for
// the full pattern of which the substitution is potentially just one
// component.
if (DiagItr->InputStartLine == DiagItr->InputEndLine &&
DiagItr->InputStartCol == DiagItr->InputEndCol)
A.Marker.Lead = ' ';
}
A.FoundAndExpectedMatch =
DiagItr->MatchTy == FileCheckDiag::MatchFoundAndExpected;
@@ -503,54 +519,54 @@ static void DumpAnnotatedInput(raw_ostream &OS, const FileCheckRequest &Req,
OS << "Input was:\n<<<<<<\n";
// Sort annotations.
std::sort(Annotations.begin(), Annotations.end(),
[](const InputAnnotation &A, const InputAnnotation &B) {
// 1. Sort annotations in the order of the input lines.
//
// This makes it easier to find relevant annotations while
// iterating input lines in the implementation below. FileCheck
// does not always produce diagnostics in the order of input
// lines due to, for example, CHECK-DAG and CHECK-NOT.
if (A.InputLine != B.InputLine)
return A.InputLine < B.InputLine;
// 2. Sort annotations in the temporal order FileCheck produced
// their associated diagnostics.
//
// This sort offers several benefits:
//
// A. On a single input line, the order of annotations reflects
// the FileCheck logic for processing directives/patterns.
// This can be helpful in understanding cases in which the
// order of the associated directives/patterns in the check
// file or on the command line either (i) does not match the
// temporal order in which FileCheck looks for matches for the
// directives/patterns (due to, for example, CHECK-LABEL,
// CHECK-NOT, or `--implicit-check-not`) or (ii) does match
// that order but does not match the order of those
// diagnostics along an input line (due to, for example,
// CHECK-DAG).
//
// On the other hand, because our presentation format presents
// input lines in order, there's no clear way to offer the
// same benefit across input lines. For consistency, it might
// then seem worthwhile to have annotations on a single line
// also sorted in input order (that is, by input column).
// However, in practice, this appears to be more confusing
// than helpful. Perhaps it's intuitive to expect annotations
// to be listed in the temporal order in which they were
// produced except in cases the presentation format obviously
// and inherently cannot support it (that is, across input
// lines).
//
// B. When diagnostics' annotations are split among multiple
// input lines, the user must track them from one input line
// to the next. One property of the sort chosen here is that
// it facilitates the user in this regard by ensuring the
// following: when comparing any two input lines, a
// diagnostic's annotations are sorted in the same position
// relative to all other diagnostics' annotations.
return A.DiagIndex < B.DiagIndex;
});
llvm::sort(Annotations,
[](const InputAnnotation &A, const InputAnnotation &B) {
// 1. Sort annotations in the order of the input lines.
//
// This makes it easier to find relevant annotations while
// iterating input lines in the implementation below. FileCheck
// does not always produce diagnostics in the order of input
// lines due to, for example, CHECK-DAG and CHECK-NOT.
if (A.InputLine != B.InputLine)
return A.InputLine < B.InputLine;
// 2. Sort annotations in the temporal order FileCheck produced
// their associated diagnostics.
//
// This sort offers several benefits:
//
// A. On a single input line, the order of annotations reflects
// the FileCheck logic for processing directives/patterns.
// This can be helpful in understanding cases in which the
// order of the associated directives/patterns in the check
// file or on the command line either (i) does not match the
// temporal order in which FileCheck looks for matches for the
// directives/patterns (due to, for example, CHECK-LABEL,
// CHECK-NOT, or `--implicit-check-not`) or (ii) does match
// that order but does not match the order of those
// diagnostics along an input line (due to, for example,
// CHECK-DAG).
//
// On the other hand, because our presentation format presents
// input lines in order, there's no clear way to offer the
// same benefit across input lines. For consistency, it might
// then seem worthwhile to have annotations on a single line
// also sorted in input order (that is, by input column).
// However, in practice, this appears to be more confusing
// than helpful. Perhaps it's intuitive to expect annotations
// to be listed in the temporal order in which they were
// produced except in cases the presentation format obviously
// and inherently cannot support it (that is, across input
// lines).
//
// B. When diagnostics' annotations are split among multiple
// input lines, the user must track them from one input line
// to the next. One property of the sort chosen here is that
// it facilitates the user in this regard by ensuring the
// following: when comparing any two input lines, a
// diagnostic's annotations are sorted in the same position
// relative to all other diagnostics' annotations.
return A.DiagIndex < B.DiagIndex;
});
// Compute the width of the label column.
const unsigned char *InputFilePtr = InputFileText.bytes_begin(),
@@ -759,6 +775,7 @@ int main(int argc, char **argv) {
return 2;
Req.AllowEmptyInput = AllowEmptyInput;
Req.AllowUnusedPrefixes = AllowUnusedPrefixes;
Req.EnableVarScope = EnableVarScope;
Req.AllowDeprecatedDagOverlap = AllowDeprecatedDagOverlap;
Req.Verbose = Verbose;

2
_servicedata
View File

@@ -1,4 +1,4 @@
<servicedata>
<service name="tar_scm">
<param name="url">git://github.com/klee/klee.git</param>
<param name="changesrevision">148a68df793fca84a36fefd8824ea54fdf6583f4</param></service></servicedata>
<param name="changesrevision">24badb5bf17ff586dc3f1856901f27210713b2ac</param></service></servicedata>

18
klee.changes
View File

@@ -1,3 +1,21 @@
-------------------------------------------------------------------
Thu May 20 06:05:58 UTC 2021 - jslaby@suse.cz
- Update to version 2.2+20210510:
* allocate memory objects for functions
* differentiate between partial and completed paths in summary and fix paths
stats when not dumping states
* posix runtime: add malloc checks
* Fix erroneous klee-stats legend for --print-all
* Replaced the time-based delay
* Refactored maxStaticPctChecks into a sequence of conditions.
* Added a warning when forking is skipped due to MaxStatic*Pct limits being
reached
* Added -max-static-pct-check-delay to replace the hardcoded delay after
which the MaxStatic*Pct checks are performed.
* klee-replay: Fix -Wformat-truncation warning
- Switch to LLVM 12.
-------------------------------------------------------------------
Tue Feb 23 07:33:34 UTC 2021 - jslaby@suse.cz

6
klee.obsinfo
View File

@@ -1,5 +1,5 @@
name: klee
version: 2.2+20210222
mtime: 1614010572
commit: 148a68df793fca84a36fefd8824ea54fdf6583f4
version: 2.2+20210510
mtime: 1620665314
commit: 24badb5bf17ff586dc3f1856901f27210713b2ac

4
klee.spec
View File

@@ -16,7 +16,7 @@
#
%define llvm_version_major 11
%define llvm_version_major 12
%define llvm_version %{llvm_version_major}
%ifarch x86_64
@@ -31,7 +31,7 @@ Name: klee
Summary: LLVM Execution Engine
License: NCSA
Group: Development/Languages/Other
Version: 2.2+20210222
Version: 2.2+20210510
Release: 0
URL: http://klee.github.io/
Source0: %{name}-%{version}.tar.xz

14
not.cpp
View File

@@ -15,6 +15,10 @@
#include "llvm/Support/WithColor.h"
#include "llvm/Support/raw_ostream.h"
#ifdef _WIN32
#include <windows.h>
#endif
using namespace llvm;
int main(int argc, const char **argv) {
@@ -27,6 +31,16 @@ int main(int argc, const char **argv) {
++argv;
--argc;
ExpectCrash = true;
// Crash is expected, so disable crash report and symbolization to reduce
// output and avoid potentially slow symbolization.
#ifdef _WIN32
SetEnvironmentVariableA("LLVM_DISABLE_CRASH_REPORT", "1");
SetEnvironmentVariableA("LLVM_DISABLE_SYMBOLIZATION", "1");
#else
setenv("LLVM_DISABLE_CRASH_REPORT", "1", 0);
setenv("LLVM_DISABLE_SYMBOLIZATION", "1", 0);
#endif
}
if (argc == 0)