Download the Plugin Development Guide - Frama-C

Transcript
CHAPTER 4. ADVANCED PLUG-IN DEVELOPMENT
So we rst run the tests suite corresponding to
plug-in
in order to display what tests have
been modied by the changes. After checking the displayed dierences, we validate the changes
by updating the oracles. Finally we run all the test suites in order to ensure that the changes
do not break anything else in Frama-C.
Example 4.7
For adding a new test, the typical sequence of command is the following.
$ ./ b i n / p t e s t s . byte -show t e s t s / plug - i n / new_test . c
$ ./ b i n / p t e s t s . byte - update t e s t s / plug - i n / new_test . c
$ make t e s t s
We rst ask ptests to print the output of the test on the command line, check that it corresponds
to what we expect, and then take it as the initial oracle. If some changes have been made to
the code in order to let
new_test.c
pass, we must of course launch the whole test suite and
check that all existing tests are alright.
If you're creating a whole new test suite suite, don't forget to create the sub-directories
suite/result and suite/oracle where ptests will store the current results and the oracles
for all the tests in suite
4.6.2 Conguration
In order to exactly perform the test that you wish, some directives can be set in three dierent
places. We indicate rst these places and next the possible directives.
The places are:
ˆ
inside le
tests/test_config;
ˆ
inside le
tests/subdir/test_config
ˆ
inside each test le, in a special comment of the form
(for each sub-directory
subdir
of
tests);
or
/* run . config
... directives ...
*/
In each of the above case, the conguration is done by a list of directives. Each directive has
to be on one line and to have the form
CONFIG_OPTION : value
There is exactly one directive by line.
CONFIG_OPTION)
The dierent directives (i.e.
possibilities for
are detailed in Section 4.6.5.
Note that some specic congurations require dynamic linking, which is not available on
all platforms for native code.
that the
OPT
or
EXECNOW
ptests
takes care of reverting to bytecode when it detects
options of a test require dynamic linking. This occurs currently
in the following cases:
ˆ OPT
contains the option
-load-script
ˆ OPT
contains the option
-load-module
ˆ EXECNOW
use
make
to create a
.cmxs
48