PLCverif Command Line Arguments

The listed command line (or settings file) arguments are only applicable to the default set of plug-ins. For an up-to-date list please execute the plcverif-cli executable without any parameter.

The format of specifying a setting is the following: -<key>=<value>. If the value contains whitespace, it needs to be quoted: -<key>="<value>". Lists can be defined as -<key>={item1, item2, item3} or as -<key>.0=item1 -<key>.1=item2 -<key>.2=item3. Any empty list shall be defined as -<key>={}.

Any of these arguments can be put in a file, separated by new line characters (i.e., one argument per line). This file can be passed as first argument to plcverif-cli. I.e., calling plcverif-cli -id=ABC -name=DEF is equivalent to calling plcverif-cli settings.txt where the content of settings.txt is

-id=ABC
-name=DEF

If an argument is defined both in the file passed as first argument and as a command line parameter, the latter will have priority.

Common arguments (PLCverif platform settings)

  • -id: ID of the job definition.
    • Type: String
  • -name: Name of the job definition.
    • Type: String (optional)
  • -description: Description of the job definition.
    • Type: String (optional)
  • -job: Job to be executed.
    • Type: String
    • Permitted values: summary, verif
  • -lf: The language frontend to be used.
    • Type: String (optional)
    • Permitted values: step7
  • -reductions: List of reductions to apply. If omitted, all reductions will be used.
    • Type: List (optional)
    • Permitted values: basic_reductions
  • -inline: Forcing CFA inlining. If true, calls will be substituted with the callees, if possible. This may be requested by the verification backend too.
    • Type: Boolean (optional)
    • Permitted values: true, false
  • -sourcefiles: List of files containing the input artifacts. The paths can be relative to the current working directory, and may use wildcards.
    • Type: List
  • -encoding: Encoding to be used to load the input artifacts. If omitted, the local default will be used.
    • Type: List (optional)
  • -output: Output artifact directory. If omitted, a new directory is created automatically.
    • Type: Path (optional)

STEP 7 language frontend (-lf = step7)

Provides language frontend (parser and CFA representation) for the STEP 7 programming languages.

  • -lf.entry: Program block which serves as entry point for the verification. If not defined, a heuristic will be used to find the entry point.
    • Type: String (optional)
  • -lf.compiler: Compiler settings to be used. Not taken into account currently.
    • Type: String (optional)
    • Permitted values: Step7v55, Tia300, Tia1200, Tia1500
    • Default value: Step7v55

Summary report generation job (-job = summaryreport)

Generates a machine-readable representation of the verification results, which can be collected and summarized by the summary job (job=summary). Only applicable if job=verif.

  • -job.summary_files: Summary memento files to be compiled into a summary report. They may contain wildcards (* or ?).
    • Type: List
  • -job.reporters: IDs of summary reporters to be used.
    • Type: List
    • Permitted values: junit-summary, html-summary

JUnit summary reporter (-job.reporters.<ID> = junit-summary)

Summarizes the outputs of previous verification jobs into a summary report in JUnit format. Applicable only if job=summary.

  • -job.reporters.<ID>.unknown_as_error: Treat 'Unknown' results as 'Error'.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false

HTML summary reporter (-job.reporters.<ID> = html-summary)

Summarizes the outputs of previous verification jobs into a summary report in human-readable HTML format. Applicable only if job=summary.

Verification job (-job = verif)

Provides the verification job.

  • -job.backend: Backend to be used.
    • Type: String
    • Permitted values: nusmv, cbmc, theta, esbmc
  • -job.req: Requirement type to be used.
    • Type: String
    • Permitted values: pattern, assertion
  • -job.reporters: List of reporters to be used.
    • Type: List (optional)
    • Permitted values: summary, html, plaintext
  • -job.show_progress: If set, it shows the progress of the job on the console.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.strict: Strictness of the various checks (assertions and validations). If true, more assertions are used for the intermediate states of the CFAs to help diagnosing problems, but it has a strong impact on the performance.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.diagnostic_outputs: Enable diagnostic outputs (such as intermediary models, CFA visualization).
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.max_reduction_iterations: Maximum number of reduction iterations at the verification job level. (This setting will not limit the inner reduction iterations of a given reduction plug-in.)
    • Type: int (optional)
    • Default value: 5

NuSMV verification backend (-job.backend = nusmv)

Solves the verification problem by using the NuSMV/nuXmv model checker. Only applicable if job=verif.

  • -job.backend.timeout: Timeout of the verification backend, in seconds.
    • Type: int (optional)
    • Default value: 5
  • -job.backend.binary_path: Full path of the NuSMV/nuXmv binary.
    • Type: Path
    • Default value: .\tools\nuxmv\nuxmv.exe
  • -job.backend.algorithm: Selects the algorithm (family) to be used by NuSMV.
    • Type: String (optional)
    • Permitted values: Classic, Ic3
    • Default value: Classic
  • -job.backend.dynamic: Enables dynamic reordering of variables in the backend.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: true
  • -job.backend.df: Disables the computation of the set of reachable states.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: true
  • -job.backend.req_as_invar: Enables the representation of the requirements as invariants, if possible.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.backend.locref_req_strategy: Use location reference in the requirement (instead of variable-based cycle end detection).
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false

CBMC verification backend (-job.backend = cbmc)

Solves the verification problem by using the CBMC model checker. Only applicable if job=verif.

  • -job.backend.timeout: Timeout of the verification backend, in seconds.
    • Type: int (optional)
    • Default value: 5
  • -job.backend.binary_path: Full path of the CBMC binary.
    • Type: Path
    • Default value: .\tools\cbmc\cbmc.exe
  • -job.backend.timeout_executor_path: Full path of the TimeoutExecutor binary.
    • Type: Path (optional)
    • Default value: .\tools\cbmc\TimeoutExecutor.dll
  • -job.backend.vs_init_batch: Path to the vcvars64.bat of Visual Studio (Windows only, not taken into account on other platforms).
    • Type: Path (optional)
    • Default value: C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat
  • -job.backend.exec_output_to_console: If true, the output of the backend execution's output will be shown on the console.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.backend.unwind: Loop unwind
    • Type: int (optional)
    • Default value: 10
  • -job.backend.verbosity: CBMC output verbosity (1..10). With verbosity levels 1..3 the result of verification is not printed, thus it cannot be parsed by PLCverif.
    • Type: int (optional)
    • Default value: 7
  • -job.backend.model_variant: Model variant (CFA declaration or instance) to be used for the the generation of the C representation.
    • Type: String (optional)
    • Permitted values: CFI, CFD
    • Default value: CFD

Theta verification backend (-job.backend = theta)

Solves the verification problem by using the Theta model checker. Only applicable if job=verif.

  • -job.backend.timeout: Timeout of the verification backend, in seconds.
    • Type: int (optional)
    • Default value: 5
  • -job.backend.binary_path: Full path to the Theta binary (.jar).
    • Type: Path
    • Default value: .\tools\theta\theta-cfa-cli.jar
  • -job.backend.lib_path: Path of the libraries (Z3 DLLs: libz3.dll, libz3java.dll or Z3 SOs: libz3.so, libz3java.so) required by Theta.
    • Type: Path
    • Default value: .\tools\theta
  • -job.backend.domain: Abstract domain. See Theta manual for more details and accepted values.
    • Type: String
    • Default value: PRED_CART
  • -job.backend.refinement: Refinement strategy. See Theta manual for more details and accepted values.
    • Type: String
    • Default value: BW_BIN_ITP
  • -job.backend.search: Search strategy. See Theta manual for more details and accepted values.
    • Type: String
    • Default value: ERR
  • -job.backend.precgranularity: Granularity of the precision of abstraction. See Theta manual for more details and accepted values.
    • Type: String
    • Default value: LOCAL
  • -job.backend.predsplit: Splitting method for new predicates obtained from interpolation. See Theta manual for more details and accepted values.
    • Type: String
    • Default value: WHOLE
  • -job.backend.encoding: Encoding of the CFA. See Theta manual for more details and accepted values.
    • Type: String
    • Default value: LBE
  • -job.backend.maxenum: Maximal successors to enumerate using the SMT solver. See Theta manual for more details and accepted values.
    • Type: String
    • Default value: (empty)
  • -job.backend.initprec: Initial precision of the abstraction. See Theta manual for more details and accepted values.
    • Type: String
    • Default value: EMPTY

Pattern requirement (-job.req = pattern)

Represents the requirement based on a selected and filled requirement pattern.

  • -job.req.pattern_file: Pattern definition XML file to be used. Leave empty to use the built-in patterns.
    • Type: Path (optional)
  • -job.req.pattern_id: ID of the requirement pattern to be used. (The given permitted values do not apply if not the default patterns are used.)
    • Type: String
    • Permitted values: pattern-implication, pattern-invariant, pattern-forbidden, pattern-statechange-duringcycle, pattern-statechange-betweencycles, pattern-reachability, pattern-repeatability, pattern-leadsto
  • -job.req.pattern_params: Parameters to fill the selected pattern. The required number of parameters depends on the selected pattern.
    • Type: String
  • -job.req.inputs: List of (PLC) variable names to be treated as inputs.
    • Type: List (optional)
  • -job.req.params: List of (PLC) variable names to be treated as parameters.
    • Type: List (optional)
  • -job.req.bindings: PLC variable value bindings.
    • Type: RequirementInputBindings (optional)
  • -job.req.bindings.variable: Variables to be bound.
    • Type: List
  • -job.req.bindings.value: Values to be used in binding.
    • Type: List

Assertion requirement (-job.req = assertion)

Represents the requirement based on the assertions present in the source code.

  • -job.req.inputs: List of (PLC) variable names to be treated as inputs.
    • Type: List (optional)
  • -job.req.params: List of (PLC) variable names to be treated as parameters.
    • Type: List (optional)
  • -job.req.bindings: PLC variable value bindings.
    • Type: RequirementInputBindings (optional)
  • -job.req.bindings.variable: Variables to be bound.
    • Type: List
  • -job.req.bindings.value: Values to be used in binding.
    • Type: List
  • -job.req.assertion_to_check: The tag(s) of the assertion(s) to be checked, or '*' if all assertions shall be checked.
    • Type: List (optional)
    • Default value: {*}
  • -job.req.max_expr_size_for_detailed_diagnosis: Maximum expression size that is considered for detailed diagnosis if the assertion has been violated.
    • Type: int (optional)
    • Default value: 250
  • -job.req.assert_representation_strategy: Assertion (error field) representation strategy. If it is 'INT', the violated assertion can be determined, but the state space will be bigger. If it is 'BOOL', the violated assertion cannot be determined (only the fact that an assertion has been violated), but the state space will be smaller.
    • Type: String (optional)
    • Permitted values: INTEGER, BOOLEAN
    • Default value: INTEGER

Summary report serializer (-job.reporters.<ID> = summary)

Provides the verification summary job. It can collect the results of previous verification jobs and produce a summary report.

HTML reporter (-job.reporters.<ID> = html)

Generates a HTML representation of the verification results, including the metadata, configuration and the eventual counterexample. Only applicable if job=verif.

  • -job.reporters.<ID>.min_log_level: Minimum log message severity to report.
    • Type: String (optional)
    • Permitted values: Error, Warning, Info, Debug
    • Default value: Warning
  • -job.reporters.<ID>.include_settings: Include the effective settings in the report.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: true
  • -job.reporters.<ID>.show_logitem_timestapms: Show timestamps for the log items.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.reporters.<ID>.hide_internal_variables: Hides the variables generated for verification purposes, which do not have a corresponding variable in the source code.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: true
  • -job.reporters.<ID>.include_stack_trace: Includes stack traces in the log when available.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.reporters.<ID>.use_lf_value_representation: Uses hints to provide type-specific value representation in the counterexample.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.reporters.<ID>.show_verification_console_output: Shows the console output of the verification tool.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: true

Plain text reporter (-job.reporters.<ID> = plaintext)

Generates a plain text representation of the verification results, including the metadata, configuration and the eventual counterexample. Only applicable if job=verif.

  • -job.reporters.<ID>.min_log_level: Minimum log message severity to report.
    • Type: String (optional)
    • Permitted values: Error, Warning, Info, Debug
    • Default value: Warning
  • -job.reporters.<ID>.include_settings: Include the effective settings in the report.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: true
  • -job.reporters.<ID>.show_logitem_timestapms: Show timestamps for the log items.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -job.reporters.<ID>.write_to_console: If true, writing the report to console is enabled.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: true
  • -job.reporters.<ID>.write_to_file: If true, writing the report to file is enabled.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: true
  • -job.reporters.<ID>.max_output_length: Maximum console output length to be included. Longer console outputs will be truncated.
    • Type: int (optional)
    • Default value: 1000

Basic reductions (-reductions.<ID> = basic_reductions)

Provides basic CFA reductions.

  • -reductions.<ID>.ExpressionPropagation_maxlocations: The number of locations in the largest supported automaton instances for the ExpressionPropagation reduction.
    • Type: int (optional)
    • Default value: 50000
  • -reductions.<ID>.ExpressionPropagation_maxage: The number of transitions through which the expressions will be propagated.
    • Type: int (optional)
    • Default value: 50
  • -reductions.<ID>.ExpressionPropagation_maxexprsize: The maximum size of expression tree that can be created by expression propagation.
    • Type: int (optional)
    • Default value: 100
  • -reductions.<ID>.show_progress: If set, it shows the progress of reductions (each reduction in each iteration) on the console.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false
  • -reductions.<ID>.fine_logging: Enables the fine-grained logging of reduction applications. It may cause significant performance penalty.
    • Type: Boolean (optional)
    • Permitted values: true, false
    • Default value: false

results matching ""

    No results matching ""