Description:

1. This is a readme file for developers

1.1 How it works?
The `ant test` tool reads the config.xml (current directory) which
contains all the current tests for K Framework, and runs all of 
them in parallel. It was to designed to be used by developers of
the K tool. It is also used by our Jenkins server for testing.

1.2 Running default tests (location: trunk):
    $ ant test

1.2 Running custom configuration file
    $ ant test -Dcfg=path/to/mycfgfile.xml

1.3 Some notes on the current test suite

Sadly, for a lot of complicated and unfortunate reasons, the current state of the test suite is not particularly excellent in terms of coverage. While many of the common cases in terms of parsing and execution are covered, there have been and probably continue to be several minor corner cases of features that are not covered by the test suite. Moreover, the majority of the tests in the test suite assert that a particular definition will compile, and that all programs in that definition will rewrite without creating errors, but say very little about what they should rewrite into or what the resulting configuration should look like when represented in text. There are, however, several notable exceptions to this:

(1) If a test in dist/examples/cink/ltlmc fails, there may be a bug involving model checking
(2) If a test in dist/examples/logik fails, there may be a bug involving search
(3) If dist/tutorial/4_imp++/lesson_3/imp.k fails for the program div.imp, or if tests/regression/unparsing fails, it is highly likely there is some kind of change (either expected or a bug) in the textual output format that krun uses to pretty-print output terms and search results.
(4) If dist/examples/imp-reachability or dist/examples/imp-symbolic fail, there may be a bug involving the symbolic backend, or, instead, there may simply be a bug involving the ground parser provided by kast.

2. Adding new tests for `ant test`

2.2 Specifying a test

In order to add a test you must add a new XML tag <test> having
the following attributes:

Mandatory attributes:
a. language - specifying the .k file you want to test
   	      by its path relative to trunk
b. folder - specify the programs path; note that `ant test` will
   	    search recursively into this folder for files having 
	    the specified extension; this path must be relative to
	    trunk
c. extension - specify a list of program extensions separated 
   	       by whitespaces

Optional attributes:
d. exclude - the programs meant to be excluded from testing (e.g. 
   	     programs which do not terminate) separated by whitespace;
	     note that program paths must be relative to path specified 
	     by folder attribute; if this attribute is missing then none
	     of the programs is excluded
e. results - specifies the results folder; this folder may contain files
   	     which specify programs input/output/error; we make the 
	     following assumption: if the program name is test.lang then 
	     the corresponding input/output/error files are 
	     test.lang.in/test.lang.out/test.lang.err; `ant test` will 
	     send on the input buffer the content of test.lang.in and will
	     compare the program output/error buffer with the content of 
	     test.lang.out/test.lang.err; if none of these files is
	     specified then the test will successfull if the exit value
	     of krun is 0.

An example of a test sml specification is shown below:

  <test
      language="dist/tutorial/4_imp++/lesson_4/imp.k"
      folder="dist/tutorial/2_imp dist/tutorial/4_imp++"
      extensions="imp"
      exclude="lesson_7/spawn.imp"
      results="tests/tutorial/4_imp++/lesson_4"
      />
 

2.3 Special sub-tags of <test>

2.3.1 Specify kompile options

Tag <kompile-option> has two attributes name (the name of the komptile option)
and value (the value of the kompile option). Multiple options are specified 
by multiple <kompile-option> tags:

      <kompile-option name="-superheat" value="division" />
      <kompile-option name="-supercool" value="lookup increment" />
 

2.3.2 Change default krun options for all programs

The default options for krun are:
   --no-color
   --output-mode=none

If you want to change the default options for krun then use the 
<all-programs> tag like below:

    <all-programs>
      <krun-option name="--search" />
      <krun-option name="--bound" value="2" />
    </all-programs>

As for <kompile-option>, the <krun-option> tag specifies the name and the 
value of krun options.

2.3.3 Change the default krun options for a program

There are cases when special programs must be run with specific options. 
This can be achived using the <program> tag having the mandatory attribute
name for the program name. An example is shown below:
 
     <program name="dist/tutorial/4_imp++/lesson_1/div.imp">
        <krun-option name="-output-mode" value="pretty" />
        <krun-option name="-search" />
        <krun-option name="-no-color" />
      </program>