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