Accepting request 798002 from home:aaronpuchert:branches:devel:tools:statica
Update klee, switch to LLVM 10, disable assertions. OBS-URL: https://build.opensuse.org/request/show/798002 OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=80
This commit is contained in:
Martin Pluskal
Git OBS Bridge
parent
4477202c6c
commit
1bd14479db
@ -24,6 +24,10 @@
|
||||
#include <cmath>
|
||||
using namespace llvm;
|
||||
|
||||
static cl::extrahelp FileCheckOptsEnv(
|
||||
"\nOptions are parsed from the environment variable FILECHECK_OPTS and\n"
|
||||
"from the command line.\n");
|
||||
|
||||
static cl::opt<std::string>
|
||||
CheckFilename(cl::Positional, cl::desc("<check-file>"), cl::Optional);
|
||||
|
||||
@ -44,6 +48,10 @@ static cl::opt<bool> NoCanonicalizeWhiteSpace(
|
||||
"strict-whitespace",
|
||||
cl::desc("Do not treat all horizontal whitespace as equivalent"));
|
||||
|
||||
static cl::opt<bool> IgnoreCase(
|
||||
"ignore-case",
|
||||
cl::desc("Use case-insensitive matching"));
|
||||
|
||||
static cl::list<std::string> ImplicitCheckNot(
|
||||
"implicit-check-not",
|
||||
cl::desc("Add an implicit negative check with this pattern to every\n"
|
||||
@ -93,30 +101,35 @@ static cl::opt<bool> VerboseVerbose(
|
||||
static const char * DumpInputEnv = "FILECHECK_DUMP_INPUT_ON_FAILURE";
|
||||
|
||||
static cl::opt<bool> DumpInputOnFailure(
|
||||
"dump-input-on-failure", cl::init(std::getenv(DumpInputEnv)),
|
||||
"dump-input-on-failure",
|
||||
cl::init(std::getenv(DumpInputEnv) && *std::getenv(DumpInputEnv)),
|
||||
cl::desc("Dump original input to stderr before failing.\n"
|
||||
"The value can be also controlled using\n"
|
||||
"FILECHECK_DUMP_INPUT_ON_FAILURE environment variable.\n"
|
||||
"This option is deprecated in favor of -dump-input=fail.\n"));
|
||||
|
||||
// The order of DumpInputValue members affects their precedence, as documented
|
||||
// for -dump-input below.
|
||||
enum DumpInputValue {
|
||||
DumpInputDefault,
|
||||
DumpInputHelp,
|
||||
DumpInputNever,
|
||||
DumpInputFail,
|
||||
DumpInputAlways
|
||||
DumpInputAlways,
|
||||
DumpInputHelp
|
||||
};
|
||||
|
||||
static cl::opt<DumpInputValue> DumpInput(
|
||||
"dump-input", cl::init(DumpInputDefault),
|
||||
static cl::list<DumpInputValue> DumpInputs(
|
||||
"dump-input",
|
||||
cl::desc("Dump input to stderr, adding annotations representing\n"
|
||||
" currently enabled diagnostics\n"),
|
||||
"currently enabled diagnostics. When there are multiple\n"
|
||||
"occurrences of this option, the <value> that appears earliest\n"
|
||||
"in the list below has precedence.\n"),
|
||||
cl::value_desc("mode"),
|
||||
cl::values(clEnumValN(DumpInputHelp, "help",
|
||||
"Explain dump format and quit"),
|
||||
clEnumValN(DumpInputNever, "never", "Never dump input"),
|
||||
clEnumValN(DumpInputAlways, "always", "Always dump input"),
|
||||
clEnumValN(DumpInputFail, "fail", "Dump input on failure"),
|
||||
clEnumValN(DumpInputAlways, "always", "Always dump input")));
|
||||
clEnumValN(DumpInputNever, "never", "Never dump input")));
|
||||
|
||||
typedef cl::list<std::string>::const_iterator prefix_iterator;
|
||||
|
||||
@ -312,8 +325,7 @@ static void BuildInputAnnotations(const std::vector<FileCheckDiag> &Diags,
|
||||
Label.flush();
|
||||
LabelWidth = std::max((std::string::size_type)LabelWidth, A.Label.size());
|
||||
|
||||
MarkerStyle Marker = GetMarker(DiagItr->MatchTy);
|
||||
A.Marker = Marker;
|
||||
A.Marker = GetMarker(DiagItr->MatchTy);
|
||||
A.FoundAndExpectedMatch =
|
||||
DiagItr->MatchTy == FileCheckDiag::MatchFoundAndExpected;
|
||||
|
||||
@ -332,28 +344,25 @@ static void BuildInputAnnotations(const std::vector<FileCheckDiag> &Diags,
|
||||
assert(DiagItr->InputStartLine < DiagItr->InputEndLine &&
|
||||
"expected input range not to be inverted");
|
||||
A.InputEndCol = UINT_MAX;
|
||||
A.Marker.Note = "";
|
||||
Annotations.push_back(A);
|
||||
for (unsigned L = DiagItr->InputStartLine + 1, E = DiagItr->InputEndLine;
|
||||
L <= E; ++L) {
|
||||
// If a range ends before the first column on a line, then it has no
|
||||
// characters on that line, so there's nothing to render.
|
||||
if (DiagItr->InputEndCol == 1 && L == E) {
|
||||
Annotations.back().Marker.Note = Marker.Note;
|
||||
if (DiagItr->InputEndCol == 1 && L == E)
|
||||
break;
|
||||
}
|
||||
InputAnnotation B;
|
||||
B.CheckLine = A.CheckLine;
|
||||
B.CheckDiagIndex = A.CheckDiagIndex;
|
||||
B.Label = A.Label;
|
||||
B.InputLine = L;
|
||||
B.Marker = Marker;
|
||||
B.Marker = A.Marker;
|
||||
B.Marker.Lead = '~';
|
||||
B.Marker.Note = "";
|
||||
B.InputStartCol = 1;
|
||||
if (L != E) {
|
||||
if (L != E)
|
||||
B.InputEndCol = UINT_MAX;
|
||||
B.Marker.Note = "";
|
||||
} else
|
||||
else
|
||||
B.InputEndCol = DiagItr->InputEndCol;
|
||||
B.FoundAndExpectedMatch = A.FoundAndExpectedMatch;
|
||||
Annotations.push_back(B);
|
||||
@ -511,6 +520,10 @@ int main(int argc, char **argv) {
|
||||
InitLLVM X(argc, argv);
|
||||
cl::ParseCommandLineOptions(argc, argv, /*Overview*/ "", /*Errs*/ nullptr,
|
||||
"FILECHECK_OPTS");
|
||||
DumpInputValue DumpInput =
|
||||
DumpInputs.empty()
|
||||
? DumpInputDefault
|
||||
: *std::max_element(DumpInputs.begin(), DumpInputs.end());
|
||||
if (DumpInput == DumpInputHelp) {
|
||||
DumpInputAnnotationHelp(outs());
|
||||
return 0;
|
||||
@ -554,6 +567,7 @@ int main(int argc, char **argv) {
|
||||
Req.VerboseVerbose = VerboseVerbose;
|
||||
Req.NoCanonicalizeWhiteSpace = NoCanonicalizeWhiteSpace;
|
||||
Req.MatchFullLines = MatchFullLines;
|
||||
Req.IgnoreCase = IgnoreCase;
|
||||
|
||||
if (VerboseVerbose)
|
||||
Req.Verbose = true;
|
||||
@ -596,8 +610,7 @@ int main(int argc, char **argv) {
|
||||
CheckFileText, CheckFile.getBufferIdentifier()),
|
||||
SMLoc());
|
||||
|
||||
std::vector<FileCheckString> CheckStrings;
|
||||
if (FC.ReadCheckFile(SM, CheckFileText, PrefixRE, CheckStrings))
|
||||
if (FC.readCheckFile(SM, CheckFileText, PrefixRE))
|
||||
return 2;
|
||||
|
||||
// Open the file to check and add it to SourceMgr.
|
||||
@ -627,7 +640,7 @@ int main(int argc, char **argv) {
|
||||
DumpInput = DumpInputOnFailure ? DumpInputFail : DumpInputNever;
|
||||
|
||||
std::vector<FileCheckDiag> Diags;
|
||||
int ExitCode = FC.CheckInput(SM, InputFileText, CheckStrings,
|
||||
int ExitCode = FC.checkInput(SM, InputFileText,
|
||||
DumpInput == DumpInputNever ? nullptr : &Diags)
|
||||
? EXIT_SUCCESS
|
||||
: 1;
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
<servicedata>
|
||||
<service name="tar_scm">
|
||||
<param name="url">git://github.com/klee/klee.git</param>
|
||||
<param name="changesrevision">d9888fcefc216b16404a39ac7b82a8fd8d5f343f</param></service></servicedata>
|
||||
<param name="changesrevision">e6d3f654df90dc6211d6c4993b937ef44b945f36</param></service></servicedata>
|
||||
@ -1,3 +0,0 @@
|
||||
version https://git-lfs.github.com/spec/v1
|
||||
oid sha256:f6b3ac84a0070c3cdb335c79e1103fc0fe89fddcc47d5d88788cc119301210dd
|
||||
size 646824
|
||||
3
klee-2.1+20200420.tar.xz
Normal file
3
klee-2.1+20200420.tar.xz
Normal file
@ -0,0 +1,3 @@
|
||||
version https://git-lfs.github.com/spec/v1
|
||||
oid sha256:1391db6895033dee074a7fb8640ae2443c424a5a0913546748f8e8d52653b8f3
|
||||
size 649528
|
||||
68
klee.changes
68
klee.changes
@ -1,3 +1,71 @@
|
||||
-------------------------------------------------------------------
|
||||
Sat Apr 25 22:10:44 UTC 2020 - aaronpuchert@alice-dsl.net
|
||||
|
||||
- Update to version 2.1+20200420:
|
||||
* Consistently define variable using notation VAR=value; fixed comment placement
|
||||
* Named jobs in Travis CI for better visualization of results
|
||||
* [posix-runtime] Improve model to handle full-path symbolic files
|
||||
* [posix-runtime] Add test for full path consistency for symbolic files
|
||||
* readStringAtAddress: support pointer into objects
|
||||
* test: add a new test for readStringAtAddress
|
||||
* readStringAtAddress: use stringstream to obtain the string
|
||||
* stats: rename QueriesConstructs to QueryConstructs
|
||||
* Statistic: slightly modernise class definition
|
||||
* stats: remove queryConstructTime (unused)
|
||||
* Add unit test for Z3Solver::getConstraintLog
|
||||
* Run "pkg update -f" before installing dependencies on FreeBSD
|
||||
* Don't search for CryptoMiniSAT when configuring STP
|
||||
* Fixed some messages, particularly Klee -> KLEE
|
||||
* Ensure that temp_builder is used when adding constant array value assertion constraints
|
||||
* StatsTracker: remove NumObjects, fix assignment of and always write ArrayHashTime
|
||||
* [posix-runtime] Simple GET/SET_LK model
|
||||
* Additional test for dealing with vector instructions
|
||||
* Added another `ScalarizerLegacyPass` run to remove vectorized code introduced during the optimization step
|
||||
* Fixed compiler warning when printing variable of type off_t
|
||||
* stat64 is deprecated on macOS; use stat instead
|
||||
* Use -snap VMs on Cirrus for FreeBSD
|
||||
* Updating KLEE's version post-release
|
||||
* Release notes for 2.1
|
||||
* Set version to 2.1
|
||||
* fix lit.cfg: numerical comparison of LLVM version numbers
|
||||
* travis: add LLVM 10.0
|
||||
* test/lit.cfg: add LLVM 10.0
|
||||
* stats: enforce table creation
|
||||
* [klee-stats] Grafana: Limit number of entries to query for column names
|
||||
* [klee-stats] Use the last row inserted instead of the row with highest Instructions
|
||||
* [klee-stats] Refactor preparing and printing the table
|
||||
* [klee-stats] Check for existence of stats file for Grafana as well
|
||||
* [klee-stats] Do not crash if tabulate is not installed but requested
|
||||
* [klee-stats] Refactor writing table into own function
|
||||
* [klee-stats] Refactor CSV printout in own function
|
||||
* [klee-stats] Check if stats file exist before trying to open it
|
||||
* Add leading zeros to genbout
|
||||
* fix p-llvm.inc: invocation for monorepo directory layout
|
||||
* find_llvm.cmake: enable parsing for git version
|
||||
* Use FreeBSD 11.3-STABLE instead of EoLed 11.2.
|
||||
* Workaround `pkg` breakage on FreeBSD CI.
|
||||
* Use `ref<>` for MemoryObject handling
|
||||
* Use `ref<>` for UpdateNode
|
||||
* Clean-up header files
|
||||
* Add move assignment operator and move construct for `ref` class.
|
||||
* Add `ReferenceCounter` struct utilized by ref<>
|
||||
* Fix ptr reference invalidation if last reference gets freed before new reference assigned.
|
||||
* Use call-by-reference for hash-function invocation
|
||||
* Replace old TR1 implementations of unordered_map/set with std::* versions
|
||||
* Use a newer Ubuntu 18.04 from the year 2020 to build KLEE Dockerimage
|
||||
* Use a newer Ubuntu 18.04 from the year 2020 to build KLEE
|
||||
* Update Docker image template for KLEE.
|
||||
* Use system's boost when building metasmt and user newer boolector version
|
||||
* Do not wait if SANITIZER_BUILD is empty
|
||||
* Add llvm as build dependency of clang in case no system packages are available
|
||||
* Add patch support for libcxx
|
||||
* Use git repository to build LLVM
|
||||
* Update ubuntu build dependencies for KLEE
|
||||
* update
|
||||
- Switch to LLVM 10.
|
||||
- Disable assertions.
|
||||
- Take "FileCheck" and "not" from official git repository.
|
||||
|
||||
-------------------------------------------------------------------
|
||||
Fri Jan 24 07:34:10 UTC 2020 - jslaby@suse.com
|
||||
|
||||
|
||||
12
klee.spec
12
klee.spec
@ -16,11 +16,10 @@
|
||||
#
|
||||
|
||||
|
||||
%define llvm_version_major 9
|
||||
%define llvm_version_minor 0
|
||||
%define llvm_version_major 10
|
||||
%define llvm_version %{llvm_version_major}
|
||||
|
||||
%define version_unconverted 2.0+20200119
|
||||
%define version_unconverted 2.1+20200420
|
||||
|
||||
%ifarch %{ix86} x86_64
|
||||
%define with_uclibc 1
|
||||
@ -32,13 +31,13 @@ Name: klee
|
||||
Summary: LLVM Execution Engine
|
||||
License: NCSA
|
||||
Group: Development/Languages/Other
|
||||
Version: 2.0+20200119
|
||||
Version: 2.1+20200420
|
||||
Release: 0
|
||||
URL: http://klee.github.io/
|
||||
Source0: %{name}-%{version}.tar.xz
|
||||
Source1: %{name}-rpmlintrc
|
||||
Source2: https://raw.githubusercontent.com/llvm-mirror/llvm/release_%{llvm_version_major}%{llvm_version_minor}/utils/not/not.cpp
|
||||
Source3: https://raw.githubusercontent.com/llvm-mirror/llvm/release_%{llvm_version_major}%{llvm_version_minor}/utils/FileCheck/FileCheck.cpp
|
||||
Source2: https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version_major}.0.0/llvm/utils/not/not.cpp
|
||||
Source3: https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version_major}.0.0/llvm/utils/FileCheck/FileCheck.cpp
|
||||
|
||||
BuildRequires: clang%{llvm_version}
|
||||
BuildRequires: cmake
|
||||
@ -94,6 +93,7 @@ sed -i '1s@/usr/bin/env python3*@/usr/bin/python3@' \
|
||||
-DCMAKE_CXX_COMPILER=clang++ \
|
||||
-DCMAKE_AR=%{_bindir}/llvm-ar \
|
||||
-DCMAKE_RANLIB=%{_bindir}/llvm-ranlib \
|
||||
-DENABLE_KLEE_ASSERTS=OFF \
|
||||
-DENABLE_DOXYGEN=OFF \
|
||||
-DENABLE_SOLVER_STP=ON \
|
||||
-DENABLE_TCMALLOC=ON \
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user