Skip to content

Merge master #1296

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 535 commits into from
Aug 30, 2017
Merged

Conversation

NathanJPhillips
Copy link
Contributor

Merge of master into SSS branch

smowton and others added 30 commits June 19, 2017 13:12
(Source: https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-6.html)

Nothing appears to use the annotation at the moment, so it cause any ill
behaviour and can't be tested, but in case it becomes used in the future
we might as well correct it.
These result from array_set instructions, which when targeting
variable-length arrays can end up targeting zero-sized arrays.
This should compile warning-free, since it is legal Java. Previously
an array_of expression with nil length yielded a warning, as would a WITH
based upon one.
Use empty() instead of size()==0, size()<1
Float-point library implementation
Follow-up to fix build failure introduced in diffblue#1032/9d991b4
…urn_type

Fix sipush return type annotation
Add empty() to grapht as it implements size()
Add empty() to containers with size()
…ers_without_simplify

Fix Java integers when --no-simplify is set
Most typos are in comments. Some are in strings - mainly strings that
are printed out.
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/").
Those are required to have sufficient information in the parse trees to make it
even remotely possible that this test passes.
Those tests broke in several ways the last months an no one noticed.
1. has_values was not initialised or used correctly. Fix-up for bda847f
2. merge would never include new values from the other element and was a no-op
for the "must" case.
Broke up the code handling initilising a pointer into a standalone
function.
Split out the logic for initilising a struct into a standalone method
@tautschnig
Copy link
Collaborator

As has been briefly discussed: wouldn't it be feasible to rebase onto develop (and keep rebasing)?

@NathanJPhillips
Copy link
Contributor Author

@tautschnig - I'm not sure we can regularly rebase as doing a complex rebase of a branch that multiple people have branches based upon requires that same rebase to be done for each of their branches. Instead I expect we will regularly merge develop into SSS (possibly after an initial one-off rebase) and that will be done very soon once this first step of merging master in is complete.

@peterschrammel
Copy link
Member

@NathanJPhillips, I strongly recommend to take the keep-rebasing approach. The hassle of rebasing feature branches is minor in comparison to the effort required to merge changes back into develop, once develop and sss have diverged.

@tautschnig
Copy link
Collaborator

Anything other than what @peterschrammel said would imply it is a proper fork, and should thus be done as such.

@smowton
Copy link
Contributor

smowton commented Aug 29, 2017

Recreated this merge myself using slightly different methods, and found the following discrepancies:

  • src/pointer-analysis/value_set_analysis.h: location.get_file()==irep_idt() -> location.get_file().empty() (current version discards a change made in 7ce9549)
  • expr2cpp_class.h and expr2jsil_class.h have both lost their explicit convert forwards (perhaps deliberately) [confirmed better in Nathan's version; this code was removed in https://github.com/diffblue/cbmc/commit/b88f98fa40874ebe1adceaa9b982fd713ca9ffb1]
  • unit/Makefile somehow has the following difference (appears cosmetic but unsure how it appeared):
-CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \
-              ../src/cpp/cpp$(LIBEXT) \
-              ../src/json/json$(LIBEXT) \
-              ../src/linking/linking$(LIBEXT) \
-              ../src/util/util$(LIBEXT) \
-              ../src/big-int/big-int$(LIBEXT) \
-              ../src/goto-programs/goto-programs$(LIBEXT) \
-              ../src/pointer-analysis/pointer-analysis$(LIBEXT) \
-              ../src/langapi/langapi$(LIBEXT) \
-              ../src/assembler/assembler$(LIBEXT) \
-              ../src/analyses/analyses$(LIBEXT) \
-              ../src/solvers/solvers$(LIBEXT) \
-              # Empty last line
+CPROVER_LIBS += ../src/ansi-c/ansi-c$(LIBEXT) \
+                ../src/cpp/cpp$(LIBEXT) \
+                ../src/json/json$(LIBEXT) \
+                ../src/linking/linking$(LIBEXT) \
+                ../src/util/util$(LIBEXT) \
+                ../src/big-int/big-int$(LIBEXT) \
+                ../src/goto-programs/goto-programs$(LIBEXT) \
+                ../src/pointer-analysis/pointer-analysis$(LIBEXT) \
+                ../src/langapi/langapi$(LIBEXT) \
+                ../src/assembler/assembler$(LIBEXT) \
+                ../src/analyses/analyses$(LIBEXT) \
+                ../src/solvers/solvers$(LIBEXT) \
+                # Empty last line

@smowton
Copy link
Contributor

smowton commented Aug 29, 2017

@peterschrammel @tautschnig I'm going for strategy #3: start submitting PRs against develop to get it closer to SSS; then either eliminate the SSS branch or its changes will be sufficiently slight that the repeated rebasing will be little work. However I would like to merge this so we have an appropriate support branch to work against in the next couple of weeks.

@NathanJPhillips
Copy link
Contributor Author

Differences with @smowton's version resolved.

@marek-trtik
Copy link
Contributor

marek-trtik commented Aug 30, 2017

I've run the regression tests and they all passed. So, I'd prove the PR for merge.

Details:
There were checked out merge-master of https://github.com/NathanJPhillips/cbmc.git (commit c043179) and update-merge of https://github.com/diffblue/security-scanner.git (commit 404cdf4). After build, the command make regression produced:

python ./benchmarks/evaluator.py
Buildfile: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_01/build.xml

jar:

compile:

clean:
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_01/build
    [javac] Compiling 2 source files to /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_01/build
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_01/dist
      [jar] Building jar: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_01/dist/taint_traces_01.jar

BUILD SUCCESSFUL
Total time: 0 seconds
Starting analysis of Java web application 'taint_traces_01'.
First performing cleanup.
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01
Collecting Java CLASS files to analyse:
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/BIN/UNPACK/JAR/taint_traces_01.jar.UNPACK_0/Main.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/BIN/UNPACK/JAR/taint_traces_01.jar.UNPACK_0/Node.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/BIN/UNPACK/JAR/taint_traces_01.jar.UNPACK_0/Other.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/BIN/UNPACK/JAR/taint_traces_01.jar.UNPACK_0/OtherBase1.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/BIN/UNPACK/JAR/taint_traces_01.jar.UNPACK_0/OtherBase2.class
Packing collected CLASS files to single JAR file: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/DIST/classes.jar
Building the program JSON file (the list of all JARs application consists of) for the 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/program.json
Building the root config JSON file for 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/config.json
Invoking 'security-analyser' ...
DiffBlue Security Analyzer version 5.8 64-bit x86_64 linux
Parsing ./../../TEMP/taint_traces_01/DIST/classes.jar
read class file Main.class from ./../../TEMP/taint_traces_01/DIST/classes.jar
read class file Node.class from ./../../TEMP/taint_traces_01/DIST/classes.jar
read class file Other.class from ./../../TEMP/taint_traces_01/DIST/classes.jar
read class file OtherBase1.class from ./../../TEMP/taint_traces_01/DIST/classes.jar
read class file OtherBase2.class from ./../../TEMP/taint_traces_01/DIST/classes.jar
JAR file without entry point: loading class files
read class file Main.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/DIST/classes.jar
read class file Node.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/DIST/classes.jar
read class file Other.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/DIST/classes.jar
read class file OtherBase1.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/DIST/classes.jar
read class file OtherBase2.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_01/DIST/classes.jar
failed to load class `java.lang.StringBuilder'
failed to load class `java.lang.String'
failed to load class `java.lang.Object'
failed to load class `java.lang.Class'
Converting
Generating GOTO Program
Removing function pointers and virtual functions
Partial Inlining
Starting the security scanner.
Loading config files.
Building supporting program-related data structures (ClassHierarchy, CallGgraph, InvertedCallGraph, InvertedTopologicalOrderOfFunctions).
Loading transition rules for the function-summarisation algorithm.
Building tokens propagation graph.
Loading summary database of LVSA analysis.
Loading summary database of TAINT analysis.
Starting computation of missing function summaries (timeout=900.0s).
[  0.0%] Skipping [function without a body]: java::java.lang.Object.<init>:()V
[  3.4%] Skipping [function without a body]: java::java.lang.StringBuilder.<init>:()V
[  6.9%] Skipping [function without a body]: java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;
[ 10.3%] Skipping [function without a body]: java::java.lang.StringBuilder.toString:()Ljava/lang/String;
[ 13.8%] java::OtherBase1.<init>:()V
[ 17.2%] java::OtherBase2.<init>:()V
[ 20.7%] java::Other.<init>:()V
[ 24.1%] java::OtherBase1.someMethod:()V
[ 27.6%] java::Other.someMethod:()V
[ 31.0%] java::OtherBase2.someMethod:()V
[ 34.5%] java::Other.someMethodCaller:(LOtherBase1;)V
[ 37.9%] java::Node.<init>:()V
[ 41.4%] java::Main.branches:(I)V
[ 44.8%] Skipping [function call representing a transition rule]: java::Main.taint_source_X1_retval:()I
[ 48.3%] Skipping [function call representing a transition rule]: java::Main.taint_sanitiser_X1_retval:(I)I
[ 51.7%] java::Other.XX:()V
[ 55.2%] java::Other.YY:()V
[ 58.6%] Skipping [function call representing a transition rule]: java::Main.taint_sink_X1_arg_0:(I)V
[ 62.1%] java::Other.baz1:(I)I
[ 65.5%] java::Other.baz0:(I)I
[ 69.0%] java::Other.branches:(I)V
[ 72.4%] java::Main.XYZ:(I)V
[ 75.9%] java::Main.bug:(I)V
[ 79.3%] java::Main.<init>:()V
[ 82.8%] java::Main.stringFoo:()V
[ 86.2%] java::Main.someMethodCaller:()V
[ 89.7%] java::Main.test_stuff:()V
[ 93.1%] java::Main.foo:()V
[ 96.6%] java::Main.bar:()I
[100.0%] Summarisation of functions has finished successfully (22 processed, 0 modelled, 7 skipped).
Starting slicer on the analysed GOTO program (timeout=900.0s).
Saving tokens propagation graph (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/program_slicing/tokens_propagation_graph.svg').
Saving summaries of TAINT analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/summaries/taint/HTML/index.html').
Saving summaries of TAINT analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/summaries/taint/JSON/__index.json').
Saving summaries of LVSA analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/summaries/lvsa/__index.json').
Saving statistics of the whole analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/HTML/index.html').
Saving statistics of the whole analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/JSON/statistics.json').
Saving analysed GOTO program in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01//goto-program/HTML/index.html').
The security scanner has finished successfully.
Starting program slicing.
Starting the search for error traces.
Invoking 'cbmc' ...
Building performance plots.
  Loading JSON file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/JSON/statistics.json".
  Building plot data file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_data.dat".
  Building function-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_speed_functions.plt".
  Building location-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_speed_locations.plt".
  Building function-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_progress_functions.plt".
  Building locations-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_progress_locations.plt".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_speed_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_speed_locations.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_progress_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/statistics/plots/analysis_progress_locations.svg".
Saving performance data in JSON format to: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/overall_performance.json
Building HTML report of all results and performance data: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_01/index.html
Done. [Time=1.31457901001s]
PASSED:"TRAINING/diffblue/taint_traces_01"
Buildfile: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_02/build.xml

jar:

compile:

clean:
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_02/build
    [javac] Compiling 1 source file to /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_02/build
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_02/dist
      [jar] Building jar: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_02/dist/taint_traces_02.jar

BUILD SUCCESSFUL
Total time: 0 seconds
Starting analysis of Java web application 'taint_traces_02'.
First performing cleanup.
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_02
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02
Collecting Java CLASS files to analyse:
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_02/BIN/UNPACK/JAR/taint_traces_02.jar.UNPACK_0/Test.class
Packing collected CLASS files to single JAR file: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_02/DIST/classes.jar
Building the program JSON file (the list of all JARs application consists of) for the 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/program.json
Building the root config JSON file for 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/config.json
Invoking 'security-analyser' ...
DiffBlue Security Analyzer version 5.8 64-bit x86_64 linux
Parsing ./../../TEMP/taint_traces_02/DIST/classes.jar
read class file Test.class from ./../../TEMP/taint_traces_02/DIST/classes.jar
JAR file without entry point: loading class files
read class file Test.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_02/DIST/classes.jar
failed to load class `java.lang.Object'
failed to load class `java.lang.Class'
failed to load class `java.lang.String'
Converting
Generating GOTO Program
Removing function pointers and virtual functions
Partial Inlining
Starting the security scanner.
Loading config files.
Building supporting program-related data structures (ClassHierarchy, CallGgraph, InvertedCallGraph, InvertedTopologicalOrderOfFunctions).
Loading transition rules for the function-summarisation algorithm.
Sanitizer rules should not also specify input, ignoring the input.
Building tokens propagation graph.
Loading summary database of LVSA analysis.
Loading summary database of TAINT analysis.
Starting computation of missing function summaries (timeout=900.0s).
[  0.0%] Skipping [function without a body]: java::java.lang.Object.<init>:()V
[ 11.1%] Skipping [function call representing a transition rule]: java::Test.taint_source_01:()I
[ 22.2%] java::Test.func1:()I
[ 33.3%] Skipping [function call representing a transition rule]: java::Test.taint_sanitize_01:(I)I
[ 44.4%] java::Test.func2:(I)I
[ 55.6%] Skipping [function call representing a transition rule]: java::Test.taint_sink_01:(I)V
[ 66.7%] java::Test.func3:(I)V
[ 77.8%] java::Test.<init>:()V
[ 88.9%] java::Test.start:()V
[100.0%] Summarisation of functions has finished successfully (5 processed, 0 modelled, 4 skipped).
Starting slicer on the analysed GOTO program (timeout=900.0s).
Saving tokens propagation graph (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/program_slicing/tokens_propagation_graph.svg').
Saving summaries of TAINT analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/summaries/taint/HTML/index.html').
Saving summaries of TAINT analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/summaries/taint/JSON/__index.json').
Saving summaries of LVSA analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/summaries/lvsa/__index.json').
Saving statistics of the whole analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/HTML/index.html').
Saving statistics of the whole analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/JSON/statistics.json').
Saving analysed GOTO program in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02//goto-program/HTML/index.html').
The security scanner has finished successfully.
Starting program slicing.
Starting the search for error traces.
Invoking 'cbmc' ...
Building performance plots.
  Loading JSON file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/JSON/statistics.json".
  Building plot data file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_data.dat".
  Building function-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_speed_functions.plt".
  Building location-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_speed_locations.plt".
  Building function-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_progress_functions.plt".
  Building locations-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_progress_locations.plt".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_speed_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_speed_locations.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_progress_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/statistics/plots/analysis_progress_locations.svg".
Saving performance data in JSON format to: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/overall_performance.json
Building HTML report of all results and performance data: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_02/index.html
Done. [Time=0.405860900879s]
PASSED:"TRAINING/diffblue/taint_traces_02"
Buildfile: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_03/build.xml

jar:

compile:

clean:
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_03/build
    [javac] Compiling 1 source file to /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_03/build
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_03/dist
      [jar] Building jar: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_03/dist/taint_traces_03.jar

BUILD SUCCESSFUL
Total time: 0 seconds
Starting analysis of Java web application 'taint_traces_03'.
First performing cleanup.
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_03
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03
Collecting Java CLASS files to analyse:
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_03/BIN/UNPACK/JAR/taint_traces_03.jar.UNPACK_0/Test.class
Packing collected CLASS files to single JAR file: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_03/DIST/classes.jar
Building the program JSON file (the list of all JARs application consists of) for the 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/program.json
Building the root config JSON file for 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/config.json
Invoking 'security-analyser' ...
DiffBlue Security Analyzer version 5.8 64-bit x86_64 linux
Parsing ./../../TEMP/taint_traces_03/DIST/classes.jar
read class file Test.class from ./../../TEMP/taint_traces_03/DIST/classes.jar
JAR file without entry point: loading class files
read class file Test.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_03/DIST/classes.jar
failed to load class `java.lang.String'
failed to load class `java.lang.Object'
failed to load class `java.lang.Class'
Converting
Generating GOTO Program
Removing function pointers and virtual functions
Partial Inlining
Starting the security scanner.
Loading config files.
Building supporting program-related data structures (ClassHierarchy, CallGgraph, InvertedCallGraph, InvertedTopologicalOrderOfFunctions).
Loading transition rules for the function-summarisation algorithm.
Building tokens propagation graph.
Loading summary database of LVSA analysis.
Loading summary database of TAINT analysis.
Starting computation of missing function summaries (timeout=900.0s).
[  0.0%] Skipping [function without a body]: java::java.lang.Object.<init>:()V
[ 16.7%] Skipping [function call representing a transition rule]: java::Test.taint_sink_01:(Ljava/lang/String;)V
[ 33.3%] java::Test.<init>:()V
[ 50.0%] java::Test.start:()V
[ 66.7%] Skipping [function call representing a transition rule]: java::Test.taint_source_01:()Ljava/lang/String;
[ 83.3%] Skipping [function call representing a transition rule]: java::Test.taint_sanitize_01:(Ljava/lang/String;)Ljava/lang/String;
[100.0%] Summarisation of functions has finished successfully (2 processed, 0 modelled, 4 skipped).
Starting slicer on the analysed GOTO program (timeout=900.0s).
Saving tokens propagation graph (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/program_slicing/tokens_propagation_graph.svg').
Saving summaries of TAINT analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/summaries/taint/HTML/index.html').
Saving summaries of TAINT analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/summaries/taint/JSON/__index.json').
Saving summaries of LVSA analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/summaries/lvsa/__index.json').
Saving statistics of the whole analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/HTML/index.html').
Saving statistics of the whole analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/JSON/statistics.json').
Saving analysed GOTO program in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03//goto-program/HTML/index.html').
The security scanner has finished successfully.
Starting program slicing.
Starting the search for error traces.
Building performance plots.
  Loading JSON file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/JSON/statistics.json".
  Building plot data file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_data.dat".
  Building function-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_speed_functions.plt".
  Building location-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_speed_locations.plt".
  Building function-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_progress_functions.plt".
  Building locations-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_progress_locations.plt".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_speed_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_speed_locations.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_progress_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/statistics/plots/analysis_progress_locations.svg".
Saving performance data in JSON format to: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/overall_performance.json
Building HTML report of all results and performance data: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_03/index.html
Done. [Time=0.367896080017s]
PASSED:"TRAINING/diffblue/taint_traces_03"
Buildfile: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_04/build.xml

jar:

compile:

clean:
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_04/build
    [javac] Compiling 4 source files to /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_04/build
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_04/dist
      [jar] Building jar: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_04/dist/taint_traces_04.jar

BUILD SUCCESSFUL
Total time: 0 seconds
Starting analysis of Java web application 'taint_traces_04'.
First performing cleanup.
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04
Collecting Java CLASS files to analyse:
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/BIN/UNPACK/JAR/taint_traces_04.jar.UNPACK_0/Main.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/BIN/UNPACK/JAR/taint_traces_04.jar.UNPACK_0/Other.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/BIN/UNPACK/JAR/taint_traces_04.jar.UNPACK_0/OtherBase1.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/BIN/UNPACK/JAR/taint_traces_04.jar.UNPACK_0/OtherBase2.class
Packing collected CLASS files to single JAR file: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/DIST/classes.jar
Building the program JSON file (the list of all JARs application consists of) for the 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/program.json
Building the root config JSON file for 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/config.json
Invoking 'security-analyser' ...
DiffBlue Security Analyzer version 5.8 64-bit x86_64 linux
Parsing ./../../TEMP/taint_traces_04/DIST/classes.jar
read class file Main.class from ./../../TEMP/taint_traces_04/DIST/classes.jar
read class file Other.class from ./../../TEMP/taint_traces_04/DIST/classes.jar
read class file OtherBase1.class from ./../../TEMP/taint_traces_04/DIST/classes.jar
read class file OtherBase2.class from ./../../TEMP/taint_traces_04/DIST/classes.jar
JAR file without entry point: loading class files
read class file Main.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/DIST/classes.jar
read class file Other.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/DIST/classes.jar
read class file OtherBase1.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/DIST/classes.jar
read class file OtherBase2.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_04/DIST/classes.jar
failed to load class `java.lang.Object'
failed to load class `java.lang.Class'
failed to load class `java.lang.String'
Converting
Generating GOTO Program
Removing function pointers and virtual functions
Partial Inlining
Starting the security scanner.
Loading config files.
Building supporting program-related data structures (ClassHierarchy, CallGgraph, InvertedCallGraph, InvertedTopologicalOrderOfFunctions).
Loading transition rules for the function-summarisation algorithm.
Building tokens propagation graph.
Loading summary database of LVSA analysis.
Loading summary database of TAINT analysis.
Starting computation of missing function summaries (timeout=900.0s).
[  0.0%] Skipping [function without a body]: java::java.lang.Object.<init>:()V
[  6.2%] java::OtherBase1.<init>:()V
[ 12.5%] java::OtherBase2.<init>:()V
[ 18.8%] java::Other.<init>:()V
[ 25.0%] java::Main.dummy_alloc:()V
[ 31.2%] java::Main.foo:()LOtherBase1;
[ 37.5%] java::OtherBase1.someMethod:()I
[ 43.8%] Skipping [function call representing a transition rule]: java::Main.taint_sink_X1_arg_0:(I)V
[ 50.0%] Skipping [function call representing a transition rule]: java::Other.source:()I
[ 56.2%] java::Other.someMethod:()I
[ 62.5%] java::Main.<init>:()V
[ 68.8%] java::OtherBase2.someMethod:()I
[ 75.0%] java::Main.baz0:()V
[ 81.2%] java::Main.baz1:()V
[ 87.5%] java::Main.baz2:(LOther;)V
[ 93.8%] Skipping [function call representing a transition rule]: java::Main.taint_sanitiser_X1_retval:(I)I
[100.0%] Summarisation of functions has finished successfully (12 processed, 0 modelled, 4 skipped).
Starting slicer on the analysed GOTO program (timeout=900.0s).
Saving tokens propagation graph (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/program_slicing/tokens_propagation_graph.svg').
Saving summaries of TAINT analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/summaries/taint/HTML/index.html').
Saving summaries of TAINT analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/summaries/taint/JSON/__index.json').
Saving summaries of LVSA analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/summaries/lvsa/__index.json').
Saving statistics of the whole analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/HTML/index.html').
Saving statistics of the whole analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/JSON/statistics.json').
Saving analysed GOTO program in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04//goto-program/HTML/index.html').
The security scanner has finished successfully.
Starting program slicing.
Starting the search for error traces.
Invoking 'cbmc' ...
Invoking 'cbmc' ...
Invoking 'cbmc' ...
Building performance plots.
  Loading JSON file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/JSON/statistics.json".
  Building plot data file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_data.dat".
  Building function-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_speed_functions.plt".
  Building location-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_speed_locations.plt".
  Building function-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_progress_functions.plt".
  Building locations-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_progress_locations.plt".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_speed_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_speed_locations.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_progress_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/statistics/plots/analysis_progress_locations.svg".
Saving performance data in JSON format to: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/overall_performance.json
Building HTML report of all results and performance data: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_04/index.html
Done. [Time=1.06107616425s]
PASSED:"TRAINING/diffblue/taint_traces_04"
Buildfile: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_05/build.xml

jar:

compile:

clean:
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_05/build
    [javac] Compiling 13 source files to /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_05/build
    [javac] Note: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_05/AssignmentAction.java uses unchecked or unsafe operations.
    [javac] Note: Recompile with -Xlint:unchecked for details.
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_05/dist
      [jar] Building jar: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_05/dist/taint_traces_05.jar

BUILD SUCCESSFUL
Total time: 0 seconds
Starting analysis of Java web application 'taint_traces_05'.
First performing cleanup.
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05
Collecting Java CLASS files to analyse:
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/ParameterParser.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/AssignmentSubmission.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/RunData.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/AssignmentService.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/XZipInputStream.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/AssignmentAction.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/DummyAssignmentSubmissionEdit.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/FormattedText.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/AssignmentSubmissionEdit.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/TaintSource.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/TaintSink.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/FileItem.class
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/BIN/UNPACK/JAR/taint_traces_05.jar.UNPACK_0/TaintedInputStream.class
Packing collected CLASS files to single JAR file: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
Building the program JSON file (the list of all JARs application consists of) for the 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/program.json
Building the root config JSON file for 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/config.json
Invoking 'security-analyser' ...
DiffBlue Security Analyzer version 5.8 64-bit x86_64 linux
Parsing ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file ParameterParser.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file AssignmentSubmission.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file RunData.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file AssignmentService.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file XZipInputStream.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file AssignmentAction.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file DummyAssignmentSubmissionEdit.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file FormattedText.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file AssignmentSubmissionEdit.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file TaintSource.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file TaintSink.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file FileItem.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
read class file TaintedInputStream.class from ./../../TEMP/taint_traces_05/DIST/classes.jar
JAR file without entry point: loading class files
read class file ParameterParser.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file AssignmentSubmission.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file RunData.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file AssignmentService.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file XZipInputStream.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file AssignmentAction.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file DummyAssignmentSubmissionEdit.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file FormattedText.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file AssignmentSubmissionEdit.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file TaintSource.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file TaintSink.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file FileItem.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
read class file TaintedInputStream.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_05/DIST/classes.jar
failed to load class `java.lang.String'
failed to load class `java.lang.Object'
failed to load class `java.io.InputStream'
failed to load class `java.lang.Class'
failed to load class `java.util.List'
failed to load class `java.util.LinkedList'
failed to load class `java.io.IOException'
failed to load class `java.lang.StringBuilder'
failed to load class `java.util.HashMap'
Converting
Generating GOTO Program
Removing function pointers and virtual functions
Partial Inlining
Starting the security scanner.
Loading config files.
Building supporting program-related data structures (ClassHierarchy, CallGgraph, InvertedCallGraph, InvertedTopologicalOrderOfFunctions).
Loading transition rules for the function-summarisation algorithm.
Building tokens propagation graph.
Loading summary database of LVSA analysis.
Loading summary database of TAINT analysis.
Starting computation of missing function summaries (timeout=900.0s).
[  0.0%] Skipping [function without a body]: java::java.lang.Object.<init>:()V
[  2.3%] java::FileItem.<init>:()V
[  4.5%] java::ParameterParser.<init>:()V
[  6.8%] java::ParameterParser.getFileItem:(Ljava/lang/String;)LFileItem;
[  9.1%] Skipping [function without a body]: java::java.io.InputStream.<init>:()V
[ 11.4%] java::TaintedInputStream.<init>:()V
[ 13.6%] Skipping [function call representing a transition rule]: java::FileItem.getInputStream:()Ljava/io/InputStream;
[ 15.9%] Skipping [function call representing a transition rule]: java::TaintSource.get_tainted_int:()I
[ 18.2%] java::TaintedInputStream.read:()I
[ 20.5%] Skipping [function call representing a transition rule]: java::TaintedInputStream.read:([BII)I
[ 22.7%] java::TaintSource.<init>:()V
[ 25.0%] java::TaintSource.<clinit>:()V
[ 27.3%] java::RunData.<init>:()V
[ 29.5%] java::RunData.getParameters:()LParameterParser;
[ 31.8%] Skipping [function without a body]: java::java.util.LinkedList.<init>:()V
[ 34.1%] java::DummyAssignmentSubmissionEdit.<init>:()V
[ 36.4%] java::AssignmentService.<init>:()V
[ 38.6%] java::AssignmentService.getSubmissions:(Ljava/lang/String;)Ljava/util/List;
[ 40.9%] java::AssignmentService.editSubmission:(Ljava/lang/String;)LAssignmentSubmissionEdit;
[ 43.2%] Skipping [function without a body]: java::java.lang.String.charAt:(I)C
[ 45.5%] Skipping [function call representing a transition rule]: java::TaintSink.receive_taint:(C)V
[ 47.7%] java::DummyAssignmentSubmissionEdit.setSubmittedText:(Ljava/lang/String;)V
[ 50.0%] java::TaintSink.<init>:()V
[ 52.3%] Skipping [function call representing a transition rule]: java::XZipInputStream.<init>:(Ljava/io/InputStream;)V
[ 54.5%] java::XZipInputStream.read:()I
[ 56.8%] Skipping [function call representing a transition rule]: java::XZipInputStream.read:([BII)I
[ 59.1%] Skipping [function without a body]: java::java.util.HashMap.<init>:()V
[ 61.4%] Skipping [function without a body]: java::java.lang.StringBuilder.<init>:()V
[ 63.6%] Skipping [function without a body]: java::java.io.InputStream.read:([BII)I
[ 65.9%] Skipping [function without a body]: java::java.lang.String.<init>:([BII)V
[ 68.2%] Skipping [function without a body]: java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;
[ 70.5%] Skipping [function without a body]: java::java.lang.StringBuilder.toString:()Ljava/lang/String;
[ 72.7%] java::AssignmentAction.readIntoString:(Ljava/io/InputStream;)Ljava/lang/String;
[ 75.0%] java::AssignmentAction.getBodyTextFromZipHtml:(Ljava/io/InputStream;Z)Ljava/lang/String;
[ 77.3%] Skipping [function without a body]: java::java.util.HashMap.put:(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;
[ 79.5%] java::AssignmentAction.uploadAll_parseZipFile:(Ljava/io/InputStream;Ljava/util/HashMap;)Ljava/util/HashMap;
[ 81.8%] java::AssignmentAction.editSubmission:()LAssignmentSubmissionEdit;
[ 84.1%] Skipping [function without a body]: java::java.util.HashMap.get:(Ljava/lang/Object;)Ljava/lang/Object;
[ 86.4%] Skipping [function without a body]: java::AssignmentSubmissionEdit.setSubmittedText:(Ljava/lang/String;)V
[ 88.6%] java::AssignmentAction.uploadAll_updateSubmissions:(Ljava/util/HashMap;Ljava/util/List;)V
[ 90.9%] java::AssignmentAction.<init>:()V
[ 93.2%] java::AssignmentAction.doUpload_all:(LRunData;)V
[ 95.5%] java::FormattedText.<init>:()V
[ 97.7%] java::FormattedText.processEscapedHtml:(Ljava/lang/String;)Ljava/lang/String;
[100.0%] Summarisation of functions has finished successfully (25 processed, 0 modelled, 19 skipped).
Starting slicer on the analysed GOTO program (timeout=900.0s).
WARNING: Instruction without 'function' reference:
  loc.: 146
  func: java::AssignmentAction.uploadAll_updateSubmissions:(Ljava/util/HashMap;Ljava/util/List;)V
  code: instanceof_tmp$1 = return_tmp1-&gt;@class_identifier;
  Fixing the issue.
WARNING: Instruction without 'function' reference:
  loc.: 234
  func: java::AssignmentAction.readIntoString:(Ljava/io/InputStream;)Ljava/lang/String;
  code: instanceof_tmp$2 = ((struct java.lang.Object *)TaintedInputStream.read:([BII)I#exception_value)-&gt;@class_identifier;
  Fixing the issue.
WARNING: Instruction without 'function' reference:
  loc.: 248
  func: java::AssignmentAction.readIntoString:(Ljava/io/InputStream;)Ljava/lang/String;
  code: instanceof_tmp$3 = ((struct java.lang.Object *)XZipInputStream.read:([BII)I#exception_value)-&gt;@class_identifier;
  Fixing the issue.
Saving tokens propagation graph (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/program_slicing/tokens_propagation_graph.svg').
Saving summaries of TAINT analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/summaries/taint/HTML/index.html').
Saving summaries of TAINT analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/summaries/taint/JSON/__index.json').
Saving summaries of LVSA analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/summaries/lvsa/__index.json').
Saving statistics of the whole analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/HTML/index.html').
Saving statistics of the whole analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/JSON/statistics.json').
Saving analysed GOTO program in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05//goto-program/HTML/index.html').
The security scanner has finished successfully.
Starting program slicing.
Starting the search for error traces.
Invoking 'cbmc' ...
Building performance plots.
  Loading JSON file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/JSON/statistics.json".
  Building plot data file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_data.dat".
  Building function-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_speed_functions.plt".
  Building location-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_speed_locations.plt".
  Building function-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_progress_functions.plt".
  Building locations-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_progress_locations.plt".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_speed_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_speed_locations.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_progress_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/statistics/plots/analysis_progress_locations.svg".
Saving performance data in JSON format to: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/overall_performance.json
Building HTML report of all results and performance data: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_05/index.html
Done. [Time=2.6390349865s]
PASSED:"TRAINING/diffblue/taint_traces_05"
Buildfile: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_06/build.xml

jar:

compile:

clean:
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_06/build
    [javac] Compiling 1 source file to /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_06/build
    [mkdir] Created dir: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_06/dist
      [jar] Building jar: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/taint_traces_06/dist/taint_traces_06.jar

BUILD SUCCESSFUL
Total time: 0 seconds
Starting analysis of Java web application 'taint_traces_06'.
First performing cleanup.
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_06
  Deleting /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06
Collecting Java CLASS files to analyse:
   /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_06/BIN/UNPACK/JAR/taint_traces_06.jar.UNPACK_0/taint_test/test.class
Packing collected CLASS files to single JAR file: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_06/DIST/classes.jar
Building the program JSON file (the list of all JARs application consists of) for the 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/program.json
Building the root config JSON file for 'goto-analyser': /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/config.json
Invoking 'security-analyser' ...
DiffBlue Security Analyzer version 5.8 64-bit x86_64 linux
Parsing ./../../TEMP/taint_traces_06/DIST/classes.jar
read class file taint_test/test.class from ./../../TEMP/taint_traces_06/DIST/classes.jar
JAR file without entry point: loading class files
read class file taint_test/test.class from /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/TEMP/taint_traces_06/DIST/classes.jar
failed to load class `java.lang.Character'
failed to load class `java.util.List'
failed to load class `java.util.ArrayList'
failed to load class `javax.servlet.ServletOutputStream'
failed to load class `java.lang.CharSequence'
failed to load class `javax.servlet.ServletInputStream'
failed to load class `java.io.IOException'
failed to load class `javax.servlet.http.HttpServletResponse'
failed to load class `java.io.OutputStream'
failed to load class `javax.servlet.http.HttpServletRequest'
failed to load class `java.io.InputStream'
failed to load class `javax.servlet.http.HttpServlet'
failed to load class `java.lang.String'
failed to load class `java.lang.Object'
failed to load class `java.lang.Class'
Converting
Generating GOTO Program
Removing function pointers and virtual functions
Partial Inlining
Starting the security scanner.
Loading config files.
Building supporting program-related data structures (ClassHierarchy, CallGgraph, InvertedCallGraph, InvertedTopologicalOrderOfFunctions).
Loading transition rules for the function-summarisation algorithm.
Building tokens propagation graph.
Loading summary database of LVSA analysis.
Loading summary database of TAINT analysis.
Starting computation of missing function summaries (timeout=900.0s).
[  0.0%] Skipping [function without a body]: java::javax.servlet.http.HttpServlet.<init>:()V
[  5.0%] Skipping [function without a body]: java::javax.servlet.http.HttpServletRequest.getInputStream:()Ljavax/servlet/ServletInputStream;
[ 10.0%] java::taint_test.test.getInStream:(Ljavax/servlet/http/HttpServletRequest;)Ljava/io/InputStream;
[ 15.0%] Skipping [function without a body]: java::java.io.InputStream.read:([BII)I
[ 20.0%] java::taint_test.test.getBytes:([BLjava/io/InputStream;)I
[ 25.0%] Skipping [function without a body]: java::java.lang.String.<init>:([BII)V
[ 30.0%] Skipping [function without a body]: java::java.lang.String.charAt:(I)C
[ 35.0%] Skipping [function without a body]: java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;
[ 40.0%] Skipping [function call representing a transition rule]: java::taint_test.test.sanitise:(Ljava/lang/String;)Ljava/lang/String;
[ 45.0%] Skipping [function without a body]: java::javax.servlet.http.HttpServletResponse.getOutputStream:()Ljavax/servlet/ServletOutputStream;
[ 50.0%] java::taint_test.test.getOutStream:(Ljavax/servlet/http/HttpServletResponse;)Ljava/io/OutputStream;
[ 55.0%] Skipping [function without a body]: java::java.io.OutputStream.write:([BII)V
[ 60.0%] Skipping [function without a body]: java::java.lang.String.getBytes:()[B
[ 65.0%] Skipping [function without a body]: java::java.io.OutputStream.write:([B)V
[ 70.0%] Skipping [function without a body]: java::java.io.OutputStream.write:(I)V
[ 75.0%] Skipping [function without a body]: java::java.util.ArrayList.<init>:()V
[ 80.0%] Skipping [function without a body]: java::java.util.List.add:(Ljava/lang/Object;)Z
[ 85.0%] java::taint_test.test.<init>:()V
[ 90.0%] java::taint_test.test.doGet:(Ljavax/servlet/http/HttpServletRequest;Ljavax/servlet/http/HttpServletResponse;)V
[ 95.0%] java::taint_test.test.foo:(Ljava/lang/String;Ljava/lang/Character;)Ljava/util/List;
[100.0%] Summarisation of functions has finished successfully (6 processed, 0 modelled, 14 skipped).
Starting slicer on the analysed GOTO program (timeout=900.0s).
Saving tokens propagation graph (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/program_slicing/tokens_propagation_graph.svg').
Saving summaries of TAINT analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/summaries/taint/HTML/index.html').
Saving summaries of TAINT analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/summaries/taint/JSON/__index.json').
Saving summaries of LVSA analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/summaries/lvsa/__index.json').
Saving statistics of the whole analysis in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/HTML/index.html').
Saving statistics of the whole analysis in JSON format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/JSON/statistics.json').
Saving analysed GOTO program in HTML format (see '/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06//goto-program/HTML/index.html').
The security scanner has finished successfully.
Starting program slicing.
Starting the search for error traces.
Invoking 'cbmc' ...
Building performance plots.
  Loading JSON file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/JSON/statistics.json".
  Building plot data file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_data.dat".
  Building function-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_speed_functions.plt".
  Building location-speed plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_speed_locations.plt".
  Building function-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_progress_functions.plt".
  Building locations-progress plot script "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_progress_locations.plt".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_speed_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_speed_locations.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_progress_functions.svg".
  Building SVG file "/home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/statistics/plots/analysis_progress_locations.svg".
Saving performance data in JSON format to: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/overall_performance.json
Building HTML report of all results and performance data: /home/marek/root/TEMP/merge_sss/benchmarks/TRAINING/diffblue/RESULTS/taint_traces_06/index.html
Done. [Time=0.494382143021s]
PASSED:"TRAINING/diffblue/taint_traces_06"

@smowton smowton merged commit 33d8af7 into diffblue:security-scanner-support Aug 30, 2017
@NathanJPhillips NathanJPhillips deleted the merge-master branch August 31, 2017 09:10
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
REVERT: 720200398 Merge branch 'develop' of github.com:diffblue/cbmc into CBMC_subtree_2018-04-10
REVERT: e2d4b09dd Updates for merge
REVERT: 1ab596d0e Merge commit '3b8120f3a8c9ed3a343493a44ac454ae265946c1' into develop
REVERT: f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327
REVERT: 207b801 Merge branch 'develop' into merge_2018-03-26
REVERT: 906aeb3 Merge pull request diffblue#349 from diffblue/owen-jones-diffblue/fix-compilation-for-release
REVERT: 3d8423c Merge pull request diffblue#350 from diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods
REVERT: 73fb488 bugfix from upstream repo for generic crash
REVERT: fd76555 Speed up resolution of virtual callsites in lazy loading
REVERT: 3fd28f3 Replace assert(X) by UNREACHABLE/INVARIANT(X)
REVERT: 557158e Merge pull request diffblue#334 from diffblue/pull-support-20180216
REVERT: 1e48132 Merge from master, 20180216
REVERT: ad7b28e Updates requsted in the PR: mostly rename 'size -> length'.
REVERT: e3fcb9b Introducing MAX_FILE_NAME_SIZE constant.
REVERT: 40b8c03 Updates requested in PR - mainly rename of functions.
REVERT: 7f868e2 Reused private code in 'remove_virtual_functions.cpp' by making it public.
REVERT: 1e0ac30 Turn get_may, set_may, etc into irep_ids
REVERT: bf7ed1a Merge pull request diffblue#313 from diffblue/owen-jones-diffblue/add-structured-lhs-to-value-set
REVERT: 1f06d35 Merge pull request diffblue#312 from diffblue/pull-support-20180112
REVERT: e42e97a Merge commit '23666e3af35673c734c9816ffc131b6b9a379e86' into pull-support-20180112
REVERT: 53f1a41 Populate structured_lhs in all `entryt`s
REVERT: 574101c Add `structured_lhs` field to entryt
REVERT: 3d492fe Add documentation of return values
REVERT: d190fd8 Merge remote-tracking branch 'upstream/develop' into pull-support-20180112
REVERT: 092df69 Switch from custom file / path routines to Boost-filesystem
REVERT: faf8f00 Merge commit 'a83b52cddbed22304372c276512c63701eb3aedb' into pull-support-20180104
REVERT: 67ec6f2 Merge remote-tracking branch 'upstream/develop' into pull-support-20180104
REVERT: 5266ba2 Merge commit 'ac4756fc3bb0e853f04de2b69f300d65cfbfc553' into pull-support-20171212
REVERT: ca5aa95 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171212
REVERT: ed5f719 Move of alias code from VSA to LVSA.
REVERT: a44becc Requests in the PR (structure of comments).
REVERT: ef51720 Updates requested in the PR (added comments).
REVERT: 377a515 Introducing function 'get_may_alias_values'.
REVERT: c0de6fb Merge pull request diffblue#273 from diffblue/smowton/fix/end_to_end_tests
REVERT: 37e5b80 Add `override` in a few places
REVERT: 653dcb6 Fix taint instrumenter handling array initalisers
REVERT: 523f60e Change template of value_set_analysis_baset
REVERT: 4f45985 Merge pull request diffblue#271 from diffblue/smowton/merge_develop_2017_11_16
REVERT: 7619d15 Rename ID_lvsa_mode to ID_lvsa_evs_type
REVERT: 471180d Adapt to upstream CBMC changes
REVERT: e8b3cb9 Merge remote-tracking branch 'upstream/develop' into smowton/merge/develop_20171116
REVERT: f653f85 Merge pull request diffblue#263 from diffblue/owen/fix-memory-bug
REVERT: 599a2f9 Merge pull request diffblue#264 from diffblue/smowton/fix/slice24_include
REVERT: de905e7 slice24 test: switch from malloc.h to stdlib.h
REVERT: c8efb6f Fix bug that can cause segfault
REVERT: fac9dea Rename "#lva_mode" to "lvsa_mode"
REVERT: 72c8533 Make two irep IDs
REVERT: 93ebb84 Merge commit '356aed461b387a8ae815a9901a16d26f32f102be' into develop
REVERT: 4820601 Merge remote-tracking branch 'diffblue/develop' into merge-dev-to-ss
REVERT: b03ec16 Merge pull request diffblue#239 from diffblue/bugfix/value_sets_fi_and_reaching_defs_retrievals_of_dynamic_objects
REVERT: 739c7f5 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171026
REVERT: 37b868a Merge pull request diffblue#251 from diffblue/feature/revert-recording-symbol-table
REVERT: c4ed1ae Revert security-scanner version of recording symbol table
REVERT: e83e307 Fixed scope of moved symbol
REVERT: a6adb19 Fix more catch std::string occurances
REVERT: d115b4e catch by const ref instead of by value or non-const ref
REVERT: 912ee38 Improve symbol table style
REVERT: 6b1a49d Add missing goto-statistics file to Makefile
REVERT: d512204 Add cbmc and jbmc as install targets
REVERT: bc887c5 Merge commit '93e2d7626046f90e14de76abbaf16c57a0425d8a' into pull-support-20171019
REVERT: 64d81f1 Merge remote-tracking branch 'upstream/develop' into pull-support-20171019
REVERT: 9a59fb9 Renamed DiffBlue -> Diffblue
REVERT: db79106 Added explanatory comment for the introduced condition.
REVERT: dfc6a20 Fixing C++ code-style issues.
REVERT: 7989831 Added regression test for the fixed bug.
REVERT: 00b4af2 Bugfix: Explicit retrievals of DOs from value_set amd reaching_defs.
REVERT: 19858f9 Fix zeroing of arrays in value set analysis
REVERT: 12fd5fe Fix identifying arrays in value set analysis
REVERT: 89341da Merge pull request diffblue#227 from diffblue/feature/adding_goto_statistics_to_goto-instrument
REVERT: 9cf47a2 Updates requested in the PR.
REVERT: 4c4a267 Adding computation and save of goto program statistics.
REVERT: 48b154a Bugfix: Exclude functions without bodies from GOTO statistics.
REVERT: 6bc86e1 Merge pull request diffblue#222 from diffblue/feature/lexicographical_ordered_dump_of_functions_and_symbols
REVERT: a73ee46 Merge pull request diffblue#224 from diffblue/feature/file_utils_add_parsing_of_file_extension
REVERT: 421f4eb Merge pull request diffblue#226 from diffblue/feature/goto_statistics
REVERT: 6d9f029 Updates requested in the PR.
REVERT: 6f8ebe4 Updates requested in the PR.
REVERT: d4a04ac Added support of Windows platform to parsing file extension.
REVERT: 1884d67 Merge pull request diffblue#221 from diffblue/bugfix/INVARIANT_while(0)_to_while(false)
REVERT: 39a774f Introducing GOTO program statistics.
REVERT: 821ba1c Updates requested in the PR.
REVERT: 9266de0 Add parsing of file extension from file path-name.
REVERT: 632ae4b Updates to recording_symbol_tablet
REVERT: 56b0b26 Added lexicographical order to textual dump of functions and symbols.
REVERT: 79324b3 INVARIANT: while(0) -> while(false)
REVERT: 733f7b2 Added is_success and is_error helpers
REVERT: 5e7f3f7 Added implicit constructors to main_function_resultt to make code in get_main_symbol even briefer
REVERT: 3317a3a Tidied up code in get_main_symbol
REVERT: 47fe36f Changed main_function_resultt to use an enum instead of a collection of bools
REVERT: a084a6a Reverting indentation in order to make the compiler silent.
REVERT: e4b5e12 Merge pull request diffblue#218 from diffblue/cleanup/typo
REVERT: 5fecceb Added recording_symbol_tablet
REVERT: 4d65951 Split storage for symbol_tablet into a concrete derived type
REVERT: 7b254e2 Made move constructor strong exception safe
REVERT: d66c0bc Changed interface to symbol_tablet::insert
REVERT: 6dc1213 Typo in reachable
REVERT: db9a0a7 Updates requested in the PR.
REVERT: d00c03d Introducing "enable_ccache" switch (default on) into our build system.
REVERT: f079156 Merge pull request diffblue#205 from diffblue/feature/restrict-symbol-table
REVERT: 2462077 Misc review requests
REVERT: 98d0082 Made lookup return optional
REVERT: db69023 Restricted interface of current symbol_tablet
REVERT: ea74c6d Updated comment
REVERT: 909b557 Added INVARIANT to symbol_tablet::remove
REVERT: bd3ee6e Add move insert to symbol_table
REVERT: 18aacc0 Add full JSON-structured output for value-set analysis
REVERT: 0cdd9c6 Improve structure of JSON static-analysis dump
REVERT: 7df9f15 Add LVSA summary dump-to-JSON
REVERT: d0d3620 Merge remote-tracking branch 'upstream/develop' into security-scanner-support
REVERT: ae83e4e Added install command for required projects.
REVERT: c48170e Merge pull request diffblue#192 from diffblue/smowton/feature/split_frontend_final_stage
REVERT: f4df5c6 Add tests for mixed GOTO and C input
REVERT: 215d5bf Split the entry-point-generation phase into two parts
REVERT: ab347d5 Merge pull request diffblue#195 from diffblue/bugfix/missing-const_cast
REVERT: 73fba6e Fixed missing const_cast
REVERT: eaf97f6 Simplify remove_instanceof logic
REVERT: 4969295 Tidy up remove_instanceof
REVERT: 2716410 Update linter to cope with CBMC subtree
REVERT: da91319 Adapt to upstream change in write_goto_binary interface and languaget
REVERT: 08f269c Merge pull request diffblue#1388 from smowton/merge-develop-20170914
REVERT: e3f3abd Merge remote-tracking branch 'upstream/develop' into merge-develop-20170914
REVERT: f25db0a Merge pull request diffblue#189 from diffblue/smowton/fix/remove_debug_code
REVERT: 1fae64c Remove stray use of overlay_map
REVERT: a2834d0 Map wrappers: forward more of the std::map interface
REVERT: 0a668ae Merge commit '6f386e5eeffa223e7213b596403085f8b497023e' into pull-support-20170908-2
REVERT: 04b4f63 Merge pull request diffblue#186 from diffblue/cleanup/misc
REVERT: 577fa6c Tightened up usage of maps
REVERT: 40557df Used range iterators
REVERT: d4e89fd Tidy up symbol_tablet::move
REVERT: 5a58539 Merge pull request diffblue#1354 from NathanJPhillips/merge-develop-to-sss
REVERT: 498718f Code readability
REVERT: 5648db1 Merge latest changes from develop to Security Scanner Support
REVERT: 52eb7ed Merge pull request diffblue#1347 from NathanJPhillips/sss/merge-develop
REVERT: 660f804 Merge develop into SSS
REVERT: 281e384 Workaround for travis performing shallow clones with wrong branch
REVERT: 33d8af7 Merge pull request diffblue#1296 from NathanJPhillips/merge-master
REVERT: c043179 Applied doxygen style to all new comments
REVERT: 3ab10aa Merge branch 'master' into security-scanner-support
REVERT: 29e1832 Merge pull request diffblue#925 from NathanJPhillips/security-scanner-support
REVERT: 42ea812 Fix missing += in Makefile that causes issues in building unit test
REVERT: d016980 Merge master into security-scanner-support
REVERT: fbe3f7a Merge pull request diffblue#845 from NathanJPhillips/security-scanner-support
REVERT: 1e919d1 Merge branch 'master' into security-scanner-support
REVERT: 5159ef1 Merge pull request diffblue#830 from mariusmc92/cleanup/move-singularity-in-vsa
REVERT: 606a5ab Added singularity check method as virtual in VSA
REVERT: 8faef3b Merge pull request diffblue#818 from NathanJPhillips/security-scanner-support
REVERT: 9c06fba Merge master into security-scanner-support
REVERT: cdce3fa Merge pull request diffblue#779 from mariusmc92/cleanup/replace-plain-string-dynamic-object
REVERT: 42f12f1 Added usages of the dynamic-object prefix's string
REVERT: 8a7fbb7 Added global string for dynamic-object prefix
REVERT: 55b3640 Merge pull request diffblue#756 from mariusmc92/feature/recency-analysis
REVERT: 9b728a7 Propagated changes of dynamic-objects' recency
REVERT: 72694d1 Added usage of dynamic-objects with recency
REVERT: 28dc578 Merge pull request diffblue#750 from NathanJPhillips/security-scanner-support
REVERT: 3dc10b7 Merge master into security-scanner-support
REVERT: 33693d8 Merge pull request diffblue#725 from smowton/boost_download
REVERT: e16f583 Switch to using Boost header-only tarball
REVERT: 36851e1 Merge pull request diffblue#706 from smowton/remove_boost_fs_dependency
REVERT: 037da22 Replace boost dependency with simple mkdir -p implementation
REVERT: 3f87bb2 Merge pull request diffblue#704 from NathanJPhillips/feature/serialization-improvements
REVERT: ad18aa9 Use shared_ptr for traits
REVERT: ca0b983 Use explicitly sized integer types
REVERT: 1ab6a25 Undid accidental config.inc change
REVERT: 29cf00c Extension of the call-graph and call-graph-based algorithms (diffblue#641)
REVERT: c694703 Added output in DOT format for class hierarchy. (diffblue#642)
REVERT: ef04e12 Merge pull request diffblue#663 from NathanJPhillips/feature/serialization
REVERT: 0764707 Used assert instead of logic_error as requested in review
REVERT: 74aea8f Added section headings
REVERT: 87a6ff5 Added serialization of irept and dstringt
REVERT: a39da77 Merge pull request diffblue#673 from NathanJPhillips/security-scanner-support
REVERT: 0bd91b5 Merge branch 'master' into security-scanner-support
REVERT: 43caa75 Merge pull request diffblue#667 from NathanJPhillips/security-scanner-support
REVERT: da9fe29 Merged master to get update to delete_directory and linter
REVERT: 08487ad Merge pull request diffblue#634 from smowton/sss_pretty_printing
REVERT: ebf7b78 Merge pull request diffblue#643 from NathanJPhillips/bugfix/file_util_sss
REVERT: ff0f281 Document pretty-printing mechanism
REVERT: 208b2e8 Add pretty-printer extension mechanism
REVERT: c4c75da Merge pull request diffblue#656 from NathanJPhillips/security-scanner-support
REVERT: 8723d57 Merge master into SSS
REVERT: e4ee8e5 Handle path doesn't exist in fileutl_absolute_path
REVERT: 749264b Call get_value_set via a base-class reference
REVERT: a5ccbd9 Add irep IDs used by the security module
REVERT: 7789d01 Add dynamic-object-expr recency
REVERT: dcd058a Comment and slightly reformat strip_casts
REVERT: c6196c3 Lint value-sets
REVERT: 9a811f7 Templatize and virtualize value-set analysis
REVERT: 3cd62e0 Value set: add declared-on-type entry member
REVERT: 53f9cd1 Add function id to value-set.
REVERT: 92ce232 Value set: avoid potential infinite expression
REVERT: 8cbf554 Trim and rename namespace-utils
REVERT: e9205e6 Style namespace-utils
REVERT: a69d950 Add namespace-utils to utils Makefile
REVERT: 229bd5b Add symbol parsing utilities.
REVERT: 116d994 Windows fileutl builds need shlwapi
REVERT: 4bd055b Style and document call graph
REVERT: af7599f Style call_graph
REVERT: 9bfa1ee Amend function documentation style
REVERT: 1095e99 Add call-graph invert and gather-leaves
REVERT: c92564f call_graph: add is-(indirect)-parent functions
REVERT: 0d862d8 Add call-graph topo sort on goto_functionst
REVERT: 85df6db Add call graph sorting and output functions
REVERT: b40dc2b Add option for simplify-expr to keep identical structs
REVERT: 885bedf Add irep IDs
REVERT: 7d57fda Add get-underlying-object utility
REVERT: db44fce Add get_this utility function
REVERT: 5150eca Add parameter-indices to util Makefile
REVERT: 998cc63 Add parameter-indexing utility
REVERT: d895844 Call get_language_options from get_goto_model
REVERT: 554f796 Static analysis: print instructions in dumps
REVERT: 37aa2de Record number of static analysis steps taken
REVERT: 32fd50f Permit static analysis to recurse
REVERT: 8157141 Use function stub behaviour in single-function mode
REVERT: 1c79841 Add static analysis hook for unavailable functions
REVERT: 09937e4 Add overlay-map
REVERT: afe9f5f Make _start optional
REVERT: da72f88 Disable Windows.h min/max define
REVERT: 8bb0fe4 Disable Boost on non-Linux platforms
REVERT: 03eeb47 Style file-util
REVERT: ba470e9 File-util: Windows compatibility fixes
REVERT: b7c00a6 Enable Boost per default
REVERT: c7e65e5 Install boost in test environment
REVERT: be43409 File-util-normalise-path: don't throw
REVERT: fc2d511 Improve path normalization logic
REVERT: a2ff638 Use boost instead of mkdir -p if available
REVERT: a7022f1 Improve file-util code style
REVERT: 82ace0f Add basic file utilities
REVERT: df36049 Add json->irep deserialization routine
REVERT: 938d739 Java checkcast: fix stack when check disabled
REVERT: dda9efb Add string-infix utility
REVERT: ca45a2b Add goto-program instruction iterator hasher
REVERT: 7428ee5 Merge pull request diffblue#583 from diffblue/master

git-subtree-dir: cbmc
git-subtree-split: 768e8a6
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

10 participants