diff --git a/doc/usr/source/2_input/1_lustre.rst b/doc/usr/source/2_input/1_lustre.rst index 223d6ffaf..6b5adcbe7 100644 --- a/doc/usr/source/2_input/1_lustre.rst +++ b/doc/usr/source/2_input/1_lustre.rst @@ -67,7 +67,7 @@ You can also specify the main node in the command line arguments, with .. code-block:: none - kind2 --lustre_main ... + kind2 --lus_main ... Main nodes specified by the command line option override main nodes annotated in the source code. If any main nodes exist then only main nodes are analyzed (top nodes are not). diff --git a/doc/usr/source/9_other/8_interpreter.rst b/doc/usr/source/9_other/8_interpreter.rst index 1c54cb311..7925dc11b 100644 --- a/doc/usr/source/9_other/8_interpreter.rst +++ b/doc/usr/source/9_other/8_interpreter.rst @@ -6,7 +6,7 @@ Interpreter The interpreter is a special mode where Kind 2 reads input values from a file and prints the computed values for the output and local variables of a node at each step. If the Lustre file contains two or more top nodes, -a single node must be selected with either the command-line option :code:`--lustre_main ` or +a single node must be selected with either the command-line option :code:`--lus_main ` or a single :code:`--%MAIN` annotation in the Lustre file. To use the interpreter, run: diff --git a/src/lustre/lustreInput.mli b/src/lustre/lustreInput.mli index 12479dd11..47c6c92c0 100644 --- a/src/lustre/lustreInput.mli +++ b/src/lustre/lustreInput.mli @@ -41,13 +41,13 @@ The main node is chosen to be, in order of precedence: - - the node with the name given by the [--lustre_main] command-line + - the node with the name given by the [--lus_main] command-line option, - the node with the annotation [--%MAIN], or - the last node in the input. An exception [Invalid_argument] is raised if the node given by - [--lustre_main] is not found, there are two nodes with a [--%MAIN] + [--lus_main] is not found, there are two nodes with a [--%MAIN] annotation, or the input contains no nodes. In particular, the output of the entry point {!LustreParser.main}