Having two Booleans that need to be kept in sync makes it harder to reason
about. Instead, use a single Boolean and use C++-11 std::all_of instead of
rolling our own loop.
Additional cleanup: remove unused cassert header.
Add a list of expected warnings from Doxygen, a Python script to
filter out those warnings from the output from Doxygen, and a simple
bash script to run doxygen using this filter.
In some cases, it would be relatively easy to fix the Doxygen
documentation so that we don't get these warnings. However, in other
cases there are bugs in Doxygen where the code and documentation are
perfectly valid, and Doxygen gives an erroneous warning message.
Currently, CI uses another script to filter out warnings related to
lines of code which have not been changed. However, this doesn't work
well because the line number reported for a warning is often not the
line where the problem lies.
The new script should be useful for CI, and also for checking changes
locally before running CI.
In case parsing a linker script fails, generate a trace, so that
debugging is possible. This way, unknown blocks in linker scripts
can be spotted more easily.
The Xen linker script has a block "PHDRS" that results in a failure
of the ls_parse.py script. As there is nothing to be done in that
script for that block, this commit adds an empty handler for this
block name. In case more blocks should be added, only the regular
expression to match the blocks has to be modified.
'format_classpath.sh' is used in regression tests that make use of the
'classpath' option. This script is needed to deal with the fact that
classpath syntex is OS-dependent.
The java concurrency regression tests make heavy use of this option as
such this commit moves 'format_classpath.sh' to
'scripts/format_classpath.sh'.
Furthermore, this commit makes a very small change to 'appveyor.yml'
that enables existing java concurrency regression tests to run on
Windows.
This was a new GCC 8 warning; testing on errno == ENOMEM with && opened the door
for non-compliant implementations to fail to allocate without capacity()
failing.
cpplint now complains if a derived-class declaration is formatted as
class derived: base
rather than complaining if it is formatted as
class derived : base
(with a space on both sides of the colon). The latter style is the one
enforced by clang-format, meaning that the two linters were inconsistent.
Evaluation is performed for a chosen GitHub or CodeCommit repository and
commit/branch/tag by running (a subset of) SV-COMP benchmarks. Runs are
done both in optimised as well as in profiling mode.
Execution should be as simple as
./perf_test.py \
-r https://github.com/diffblue/cbmc -c develop \
-e tautschn@amazon.com
assuming that AWS access keys are set up (as required for AWS cli use) and boto3
is installed. Emails will then be sent as results become available.
The script sets up (and persists) an S3 bucket for storing results, SNS
queues for email updates on the process, as well as an EBS snapshot
containing the benmarking data.
For each benchmarking run, builds are set up and performed via
CodeBuild. Evaluation is then performed using AutoScalingGroups
synchronised via SQS.
The design premise for this work was:
"Compare multiple configurations for performance, correctness, capabilities."
This was broken down into:
Configuration: target platform, timeout, memory limit, benchmark set, tool
options, source version (=repository + revision).
Compare: log files, counterexamples, CPU profile, memory profile, verification
results.
These were broken, leaving an mstreamt whose back-pointer pointed
into a different messaget than the one it enclosed, which could then have
its message_handlert changed with unexpected side-effects, or be deleted
causing a probable segfault on next log message.
The added unit tests verify that this no longer happens.
* Attempts to cope with invalid UTF-8 (present in a few CBMC files) using iconv
* Splits the filter-by-diff job into two stages (diff -> JSON description of interesting lines
and JSON -> filtered output)
This means that run_diff.sh CPPLINT is now practical, and produces a report of the linting
problems in develop but not in master (around 150 lines as of the time of writing) in about 2 minutes.
goto-gcc now runs the ls_parse.py script whenever the target codebase is
being compiled with a custom linker script (specified with the -T
option). goto-gcc then synthesizes the linker script definitions that
ls_parse reported, and adds them to the goto-program as if those
definitions were defined in the target C program rather than the linker
script.
This solves a problem where the values of some C variables are
inaccessible from CBMC because those variables are defined in the linker
script rather than the C codebase. It also solves the problem of CBMC
not knowing what memory regions are accessible to the C program, again
because the memory regions are declared to be valid in the linker
script.
This commit also introduces three tests for this functionality.
This commit also fixes a small bug in ls_parse.py that made it reject
some valid linker scripts.
travis clones a repo by 'git clone --depth 50 repo' which is ok if the
PR target is the master branch. It should actually add '--branch=
$TRAVIS_BRANCH' to the clone command. This commit provides a
workaround.
Only give warnings for namespaces with actual names, in accordance with
ad41375353.
This enables the use of anonymous namespaces without warnings.
Fixes: #932
Removal of first component for header guard suggestion is hard-coded to
remove 4 characters ("src/"). This doesn't work with all directory
names ("unit/").
Add ls_parse.py, a script to discover symbols whose values are defined
in a linker script, and valid memory extents corresponding to sections
in an object file. ls_parse can emit this information as a C file,
suitable for compiling into a goto-binary and linking with the rest of
the codebase. ls_parse can also emit the information as a JSON file,
suitable for automatic processing from within goto-cc. This supports
CPROVER in knowing the actual values of symbols that are not defined in
the C source.
CR: https://cr.amazon.com/r/7191907/
Disabling warnings globally by setting 'Wno-deprecated-register' and
'Wno-sign-compare' in CXXFLAGS will silence these errors, even in new
code. It's better to use `pragma`-based warning suppression, so that
warnings are only disabled in locations that won't or can't be fixed.
Likewise, rather than filtering 'Wpedantic' from CXXFLAGS when building
some of the solvers, it's better to disable warnings just on the
problematic headers.
Disabling warnings globally by setting 'Wno-deprecated-register' and
'Wno-sign-compare' in CXXFLAGS will silence these errors, even in new
code. It's better to use `pragma`-based warning suppression, so that
warnings are only disabled in locations that won't or can't be fixed.
Likewise, rather than filtering 'Wpedantic' from CXXFLAGS when building
some of the solvers, it's better to disable warnings just on the
problematic headers.
Sometimes the diff file would contain a unicode character. Since we were
opening the file, this meant that unidiff was reading the file in the
wrong format. By letting unidiff handle reading the file we slightly
simplify the code and fix this problem.
Change `#ifdef __linux__` and `#if defined(__linux__)` when it really
means *linux with glibc*. To avoid failures and be more specific
it is now adding `defined(__GLIBC__)` to check if `glibc` is present.
Change `#ifdef __linux__` and `#if defined(__linux__)` when it really
means *linux with glibc*. To avoid failures and be more specific
it is now adding `defined(__GLIBC__)` to check if `glibc` is present.
git-diff when a file has been removed diffs against /dev/null instead
of the usual pattern `b/some/path/to/file.cpp`. This change avoids
asserting a "b/" prefix in that case.
Works, but breaks subsequent fixes in the same file. We will need to
reverse the order of line numbers if we want to use this, so that we
apply fixes at the end of the file first.
Previously we would try and run git blame on a deleted file (since would
still show up in the diff) which would cause an error. Now we just skip
over such files.
Michael Tautschnig