percikan - Online di Cloud

PROGRAM:

NAMA

spark - memeriksa program SPARK dan menghasilkan kondisi verifikasi

RINGKASAN

percikan [OPSI] [ FILE_LIST atau @METAFILE ]

DESKRIPSI

Penguji untuk SPARK, percikan, menganalisis file sumber yang diberikan untuk kesalahan dan pelanggaran
dari subset SPARK dan (opsional) menghasilkan kondisi verifikasi dan jalur mati
dugaan yang diperlukan untuk bukti tidak adanya pengecualian run-time dan kebenaran sebagian.

Halaman manual ini hanya merangkum percikan bendera baris perintah, silakan lihat lengkap
Manual pemeriksa untuk informasi lebih lanjut.

PILIHAN

Opsi ini tidak mengikuti sintaks baris perintah GNU yang biasa. Semua opsi dimulai
dengan tanda hubung tunggal, bukan dua yang biasa dan mereka juga dapat disingkat, selama
singkatannya unik. Sebagai contoh -bantu dapat disingkat menjadi -dia tapi tidak -h seperti ini
bentrok dengan -html.

-sumber_ekstensi=tipe_file
Menentukan ekstensi file sumber (Default 'ada')

-noindex_file, -file_indeks=file_spec
Menentukan file indeks. Secara default tidak ada file indeks yang digunakan.

-nowarning_file, -peringatan_file=file_spec
Menentukan file kontrol peringatan. Secara default tidak ada file kontrol peringatan yang digunakan.

-noconfig_file, -config_file=file_spec
Menentukan file konfigurasi Pemeriksa. Secara default tidak ada file konfigurasi
bekas.

-tidak beralih
Abaikan file spark.sw, jika ada.

-nolisting, -daftar_ekstensi=tipe_file
Secara default semua file daftar memiliki ekstensi 'lst'. Opsi ini dapat digunakan untuk
nonaktifkan pembuatan file daftar atau untuk mengubah ekstensi default.

-nolaporan_file, -laporan_file=file_spec
Secara default laporan akan diberi nama 'SPARK.REP'. Opsi ini dapat digunakan untuk
mengubah nama default atau menonaktifkan pembuatan laporan.

-html, -html=dir_spec
Hasilkan daftar HTML dan file laporan.

-direktori_keluaran=dir_spec
Hasilkan laporan, daftar, dan file bukti di direktori yang ditentukan.

-keluaran_polos
Tidak ada tanggal, baris atau nomor kesalahan yang akan muncul di file output.

-bahasa=L
Ini bisa berupa salah satu dari 83, 95 (default) atau 2005.

-profil=P
Pilih antara profil bahasa berurutan (default) atau ravenscar.

-nodurasi
Jangan tentukan sebelumnya Standard.Duration.

-sintaks_periksa
Lakukan pemeriksaan sintaks saja. Tidak ada pemeriksaan semantik.

-aliran_analisis=JENIS
Pilih antara informasi atau data.

-kebijakan=JENIS
Pilih kebijakan keamanan atau keselamatan untuk analisis aliran.

-vcg Menghasilkan VC.

-dpc Menghasilkan DPC.

-aturan=PILIHAN
Pilih kebijakan untuk pembuatan aturan pembuktian konstan komposit. Bisa menjadi salah satu dari tidak ada
(default), malas, tajam atau semuanya.

-anotasi_karakter=ARANG
Pilih karakter anotasi alternatif. Standarnya adalah '#'.

-tidak ada gema
Menekan output layar.

-nosli Jangan buat file SLI.

-sparklib
Gunakan perpustakaan SPARK standar.

-nostatistik, - Statistik
Tambahkan statistik penggunaan tabel Pemeriksa ke file laporan. Secara default kami tidak melakukannya
ini.

-fdl_identifier=PILIHAN
Kontrol pengobatan pengidentifikasi FDL ketika ditemukan di sumber SPARK. Bisa menjadi salah satu
'tolak' (default) atau 'terima' atau .

-versi
Cetak spanduk Pemeriksa dan statistik lalu keluar.

-bantu Cetak ringkasan dan opsi baris perintah.

-asli_aliran_kesalahan
Cetak kesalahan aliran informasi dalam format asli, kurang ringkas.

-kesalahan_penjelasan=SETTING
Cetak penjelasan setelah pesan kesalahan. Pengaturan bisa mati (default),
first_occurrence atau every_occurrence.

-pembenaran_option=JENIS
Pilih kebijakan untuk pembenaran kesalahan. Nilai bisa penuh (default), singkat
atau mengabaikan.

-selubung, -casing=PILIHAN
Periksa casing untuk referensi pengidentifikasi dan periksa casing paket Standar
pengenal. Dimungkinkan juga untuk menentukan i atau s untuk memeriksa hanya salah satunya.

Gunakan percikan online menggunakan layanan onworks.net