Este es el comando Spark que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
Spark: examina los programas SPARK y genera condiciones de verificación.
SINOPSIS
chispa [OPCIONES] [FILE_LIST o @METAFILE]
DESCRIPCIÓN
El examinador de SPARK, chispa, analiza los archivos de origen dados en busca de errores e infracciones
del subconjunto SPARK y (opcionalmente) genera condiciones de verificación y ruta muerta
conjeturas necesarias para probar la ausencia de excepciones en tiempo de ejecución y corrección parcial.
Esta página de manual solo resume el chispa banderas de la línea de comandos, consulte el
Manual del examinador para obtener más información.
OPCIONES
Estas opciones no siguen la sintaxis habitual de la línea de comandos de GNU. Todas las opciones comienzan
con un solo guión en lugar de los dos habituales y también se pueden abreviar, siempre que
la abreviatura es única. Por ejemplo -ayuda puede abreviarse como -él pero no -h ya que esto
choca con -html.
-source_extension =Tipo de archivo
Especifica la extensión del archivo de origen (predeterminada 'ada')
-noindex_file, -index_file =especificación_archivo
Especifica el archivo de índice. De forma predeterminada, no se utiliza ningún archivo de índice.
-archivo_de_nowarning, -warning_file =especificación_archivo
Especifica el archivo de control de advertencias. De forma predeterminada, no se utiliza ningún archivo de control de advertencia.
-noconfig_file, -config_file =especificación_archivo
Especifica el archivo de configuración del examinador. Por defecto, no hay ningún archivo de configuración
usado.
-sin interruptor
Ignore el archivo spark.sw, si existe.
-nolistas, -listing_extension =Tipo de archivo
De forma predeterminada, todos los archivos de listas tienen la extensión 'lst'. Estas opciones se pueden utilizar para
deshabilitar la generación de archivos de lista o cambiar la extensión predeterminada.
-noreport_file, -report_file =especificación_archivo
Por defecto, el informe se llamará 'SPARK.REP'. Estas opciones se pueden utilizar para
cambie el nombre predeterminado o para deshabilitar la generación de informes.
-html, -html =especificación_dir
Genere listados HTML y archivo de informe.
-output_directory =especificación_dir
Genere archivos de informes, listas y pruebas en el directorio especificado.
-salida_plana
No aparecerán fechas, líneas o números de error en los archivos de salida.
-lenguaje =L
Puede ser uno de 83, 95 (predeterminado) o 2005.
-profile =P
Elija entre el perfil de idioma secuencial (predeterminado) o ravenscar.
-noduración
No predefinir Duración estándar.
-sintaxis_check
Realice solo una verificación de sintaxis. Sin controles semánticos.
-análisis_flujo =TIPO
Elija entre información o datos.
-política =TIPO
Seleccione la política de seguridad o protección para el análisis de flujo.
-vcg Genere VC.
-dpc Genere DPC.
-rules =ELECCIÓN
Seleccione la política para la generación de reglas de prueba constantes compuestas. Puede ser uno de ninguno
(predeterminado), perezoso, entusiasta o todo.
-annotation_character =CHAR
Seleccione un carácter de anotación alternativo. El valor predeterminado es '#'.
-noeco
Suprime la salida de pantalla.
-nosli No genere archivos SLI.
-sparklib
Utilice la biblioteca SPARK estándar.
-noestadísticas, -estadística
Agregue las estadísticas de uso de la tabla Examiner al archivo de informe. Por defecto no lo hacemos
esta.
-fdl_identifiers =OPCIÓN
Controlar el tratamiento de los identificadores FDL cuando se encuentran en la fuente SPARK. Puede ser uno de
'rechazar' (predeterminado) o 'aceptar' o .
-versión
Imprima el banner y las estadísticas del examinador y luego salga.
-ayuda Imprime el resumen y las opciones de la línea de comandos.
-errores_flujo_originales
Imprima errores de flujo de información en formato original, menos compacto.
-error_explanations =AJUSTE
Imprima explicaciones después de los mensajes de error. La configuración puede estar desactivada (por defecto),
first_occurrence o every_occurrence.
-opción_justificación =TIPO
Seleccione la política para la justificación de errores. Los valores pueden ser completos (predeterminado), breves
o ignorar.
-caja, -casing =ELECCIÓN
Verifique la carcasa para ver las referencias de los identificadores y verifique la carcasa del paquete Estándar
identificadores. También es posible especificar i o s para verificar solo uno de estos.
Use Spark en línea usando los servicios de onworks.net
