Added a new option "-p" to test.pl to request printing failure logs instead of
doing so via an external script. This simplifies various Makefiles and enables
use in cmake builds.
When checking for success or failure of a test, the number of iterations
in the actual test should be irrelevant. As MiniSAT and PicoSAT seem to
disagree on this number, do not check for it, so that the testis pass
again.
Cbmc can potentialy run out of memory if no maximum string length is
set. This happens more often with the new version of check axioms
because a concretization step is made to be more precise in the check.
Also amend tests that are perturbed by this.
They used to require a specific goal marked as success, but when they become
simple enough that the simplifier solves the problem by itself the goal list is
not printed. Therefore just look for VERIFICATION SUCCESSFUL.
Also modify a test that was looking for a null pointer failure, since the
phrasing of them has changed.
The relevant tests implemented in diffblue/test-gen/pull/479 (StringContains3 and StringContains4) for test-gen have been adapted and added as StringContains01 and StringContains02 resp. They have been marked as future in accordance to the standard for other tests. A contains smoke test already exists and is active, which was extended.
Add test java_intern
Adapt test.desc to new output format
Make more robust java tests.
Add test for parseint.
Correction in the hacks to use refined strings in C programs
Add smoke tests for java string support
Quick set of tests.
Created by modifying the existing development tests.
Longer tests are run when using 'make testall'.
Format of java files was adapted.
No change to the validation tests (written by Lucas Cordeiro).
Update smoke tests
Add a series of performance tests that check that the negation of the
assertions found in the smoke tests indeed fail.
Update java_char_array_init/test_init.class
Add first fixed_bugs test
For bug #95
Update test description with new option name
String refinement option name has changed to --refine-strings
Formatting in cprover-string-hack.h
Move smoke tests to regression folder.
Move fixed bugs tests to strings folder
Move string perfomance tests to strings directory
These are not really performance tests, only tests that are longer than
the smoke tests.
Adapt Makefile for new location of smoke tests
Now directly test individual lines with perls regex matching rather than
calling out to grep. Some changes were required:
- escape (, ) if we want to match them
- unescape (, ) if we want to use them as regex bracket groups
- escape +, $ if we want to use them as actual characters
- unescape + to use as a regex +
We are going to add a string-refine option to CBMC, (instead a pass
option as used in previous version of the tests).
We changed the test description file accordingly and added a few
extra tests (for java char arrays).
Also changed the flag in string regression from CORE to FUTURE:
Since the string solver is not yet part of this branch, we mark the
tests for string functions as FUTURE. They will be changed to CORE
once the corresponding features are integrated in CBMC.
I also changed the Makefile for being able to test tests marked as
future.
Michael Tautschnig