Complete Examples
Simple Ada Example
polyspace-ada \
-main a_project.root_procedure \
-prog myProject \
-O1 \
-sources directory/*.ad[bs] \
-modules-precision sri:O2,types:O0
Back to Top
HDCA Server Example
An Ada example. Note that we try to minimize verification time
in going to pass2 and O0. Note also the list of files (no spaces in
that file list!).
polyspace-ada \
-prog HDCA_Server \
-main hdca_main.HDCA_Server \
-O0 \
-from scratch -to pass2 \
-keep-all-files \
-no-automatic-stubbing \
-continue-with-red-error \
-results-dir RESULTS \
-sources \
$working_version/hdca/clock_and_date.ada,\
$working_version/hdca/cpu_usage.ada,\
$working_version/hdca/exception_log.ada,\
$working_version/hdca/hdca_main.ada,\
$working_version/screen/monitor.ada,\
$working_version/common/utilities/letter_box.ada,\
$working_version/common/utilities/library_functions.ada,\
$working_version/common/utilities/catalog_tools.ada,\
$working_version/common/utilities/configuration.ada,\
$working_version/common/utilities/converting.ads\
$working_version/common/utilities/converting.adb
Back to Top
airplane2 Example
An Ada Example with Tasks
polyspace-ada \
-target m68k \
-entry-points Wings.wingSuperVisor,Tail.tailSuperVisor,\
Rudder.rudderSuperVisor \
-to pass2 \
-from scratch \
-prog airplane2 \
-O0 \
-results-dir `pwd`/RESULTS_14_08 \
-main main.pst_main
Back to Top
High Speed Train Example
An Ada example.
polyspace-ada \
-target sparc \
-from scratch \
-array-expansion-size 1 \
-sources "sources/*.[aA]*[a-zA-Z]" \
-prog high_speed_train \
-O0 \
-keep-all-files \
-results-dir RESULTS \
-main root_package.start
Back to Top
 | Examples | | | |
Store 
