1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
Regressions
===========
To insert a new regression, add the file to Subversion, for example:
svn add regress/regress0/testMyFunctionality.cvc
Also add it to the relevant Makefile.am, here, in regress/regress0/Makefile.am.
A number of regressions exist under test/regress that aren't listed in any
Makefile.am. These are regressions that may someday be included in the standard
suite of tests, but aren't yet included (perhaps they test functionality not
yet supported).
If you want to add a new directory of regressions, add the directory name to
SUBDIRS (with . running first, by convention), and set up the new directory
with a new Makefile.am, adding all to the Subversion repository.
=== EXPECTED OUTPUT, ERROR, AND EXIT CODES ===
In the case of CVC input, you can specify expected stdout, stderr, and exit
codes with the following lines directly in the CVC regression file:
% EXPECT: stdout
% EXPECT-ERROR: stderr
% EXIT: 0
expects an exit status of 0 from cvc4, the single line "stderr" on stderr,
and the single line "stdout" on stdout. You can repeat EXPECT and EXPECT-ERROR
lines as many times as you like, and at different points of the file. This is
useful for multiple queries:
% EXPECT: INVALID
QUERY FALSE;
% EXPECT: VALID
QUERY TRUE;
% EXPECT-ERROR: CVC4 Error:
% EXPECT-ERROR: Parse Error: regress.cvc:7.13: Unexpected token: 'error'.
syntax error;
% EXIT: 1
Use of % gestures in CVC format is natural, as these are comments and ignored
by the CVC presentation language lexer. In SMT and SMT2 formats, you can do the
same, putting % gestures in the file. However, the run_regression script
separates these from the benchmark before running cvc4, so the cvc4 SMT and SMT2
lexers never see (and get tripped up on) the % gestures. But there's then the
annoyance that you can't run SMT and SMT2 regressions from the command line
without the aid of the run_regression script. So, if you prefer, you can separate
the benchmark from the output expectations yourself, putting the benchmark in
(e.g.) regress/regress0/benchmark.smt, and the % EXPECT: lines in
regress/regress0/benchmark.smt.expect, which is specifically looked for by
the run_regression script. If such an .expect file exists, the benchmark
is left verbatim (and never processed to remove the % EXPECT: lines) by the
run_regression script.
-- Morgan Deters <mdeters@cs.nyu.edu> Thu, 01 Jul 2010 13:36:53 -0400
|
