Merge pull request diffblue#270 from diffblue/smowton/cleanup/move_benchmarks_to_pytest

Move simple benchmarks to run under Pytest

Author: smowton

.gitignore

@@ -15,6 +15,7 @@ driver/.idea
 driver/*.pyc
 build
 dist
+doc
 
 # Ignoring boost
 boost/*
@@ -27,3 +28,11 @@ boost/*
 *.obj
 *.a
 *.lib
+
+# emacs backups and temporaries
+\#*
+*~
+
+# pytest temporaries
+__pycache__
+.cache

.travis.yml

@@ -227,13 +227,12 @@ jobs:
 install:
   - ccache --max-size=1G
   - cmake . -Bbuild "-DCMAKE_CXX_COMPILER=${COMPILER}" "-DCMAKE_BUILD_TYPE=${BUILD_TYPE}" "-Denable_security_tests=${RUN_SECURITY_TESTS}" "-Denable_cbmc_tests=${RUN_CBMC_TESTS}"
-  - ( cd build; make install -j2 )
+  - ( cd build; make -j2 )
 
 # LOCAL CHANGES: Added cbmc/ prefix, and added unit and regression tests to the end of the list.
 
 script:
   - ( cd build; ctest -V -L CORE )
-  - scripts/travis_run_regression_tests.sh
 
 before_cache:
   - ccache -s

benchmarks/README.txt

@@ -10,33 +10,20 @@ sub-directories in this directory:
     Here we store genuine Java web applications, i.e. those used in practice.
     These benchmarks serve us for evaluation of the tool in conditions similar
     to those, when the tools is deployed to a customer.
-    
+
     NOTE: These benchmarks are not suitable as data for regression test due to
           their size.
 
-  * TRAINING
-
-    These benchmarks classified as "tiny and feature/bug oriented Java web
-    applications". Their purpose is to aid development of the tool. They are
-    supposed to be real web applications (in the sense of GENUINE benchmarks),
-    however, they should be as miniature as possible to maximise effectiveness
-    of developments and/or debugging of desired feature.
-    
-    NOTE: These benchmarks may/should also serve as data for regression tests.
-          We keep the benchmarks separatelly from regresions tests, as one
-          benchmark can be used in several regression tests.
-    
   * LIBRARIES
-  
+
     This directory stores libraries commonly used in Java web applications.
     So, here we do not store benchmarks, but Java code we include in analysis
     of benchmarks in sub-directories GENUINE and TRAINING.
-    
+
     NOTE: There is already going work on model of Java standard library for
           CMBC. This model and similar should be stored here and used in
           benchmarks.
 
 Not all benchmarks or libraries are immediatelly redy to use. Majority of them
 actually require installation. These installation steps are described in details
 in "README.txt" files located in relevant locations in the sub-directories.
-