4. Usage

4.1. Ocarina command-line

Ocarina has a rich command-line interface, covering all required steps to parse, instantiate, analyze or generate code from AADL models.

-h, --help

Display help and exit

--version

Display version and exit

-v, --verbose

Output extra verbose information

-q

Quiet mode (default)

-d

Debug mode

-s

Output default search directory, then exit

-aadlv[ARG]

AADL version, ARG = 1 for AADL 1.0, 2 for AADL 2.x

-f

Parse predefined non-standard property sets

-disable-annexes=ARG

Deactivate annex ARG

-r ARG

Use ARG as root system

-o ARG

Specify output file/directory

-y

Automatically load AADL files

-I ARG

Add ARG to the directory search list

-p

Parse and instantiate the model

-i

Instantiate the model

-x

Parse AADL file as an AADL scenario file

-g ARG

Generate code using Ocarina backend ‘ARG’

--list-backends

List available backends

--spark2014

Generate SPARK2014 annotations

-b

Compile generated code

-z

Clean code generated

-k ARG

Set POK flavor (arinc653/deos/pok/vxworks)

-t

Run Ocarina in terminal interactive mode

-real_theorem ARG

Name of the main REAL theorem to evaluate

-real_lib ARG

Add external library of REAL theorems

-real_continue_eval

Continue evaluation of REAL theorems after first failure (REAL backend)

-boundt_process ARG

Generate .tpo file for process ARG (Bound-T backend)

-ec

Compute coverage metrics

-er

Execute system

-asn1

Generate ASN1 deployment file (PolyORB-HI-C only)

-perf

Enable profiling with gprof (PolyORB-HI-C only)

Note

A man page is also installed in Ocarina installation path, in $OCARINA_PATH/share/man/man1/.

4.2. ocarina-config

ocarina-config returns path and library information on Ocarina installation. This script can be used to compile user program that uses Ocarina’s API.

Usage: ocarina-config [OPTIONS]
Options:
        No option:
            Output all the flags (compiler and linker) required
            to compile your program.
        [--prefix[=DIR]]
            Output the directory in which Ocarina architecture-independent 
           files are installed, or set this directory to DIR.
        [--exec-prefix[=DIR]]
            Output the directory in which Ocarina architecture-dependent 
           files are installed, or set this directory to DIR.
        [--version|-v]
            Output the version of Ocarina.
        [--config]
            Output Ocarina's configuration parameters.
        [--runtime[=<Runtime_Name>]]
            Checks the validity and the presence of the given runtime and 
            then, outputs its path. Only one runtime can be requested at 
            a time. If no runtime name is given, outputs the root directory
            of all runtimes.
        [--libs]
            Output the linker flags to use for Ocarina.
        [--projects]
            Output the path to GNAT Project files for Ocarina
        [--properties]
            Output the location of the standard property file.
        [--resources]
            Output the location of resource files 
            (typically the standard properties)
        [--cflags]
            Output the compiler flags to use for Ocarina.
        [--help]
            Output this message