Module dev.civl.mc
Package dev.civl.mc.config.IF

Class CIVLConstants

java.lang.Object
dev.civl.mc.config.IF.CIVLConstants
public class CIVLConstants extends Object
This class manages all constant configurations of the system. NOTE: when you add a new option, add it here, give it name ending in "O", like the others, AND add it to the list in method getAllOptions(). And keep them in alphabetical order.

  • Field Details

    • ROOT_RESOURCE_PATH_STR

      public static final String ROOT_RESOURCE_PATH_STR
      The common root of the paths of all resources.
      See Also:

    • CIVL_LIB_SRC_PATH

      public static final File CIVL_LIB_SRC_PATH
      Resource path to the CIVL library implementations files (.cvl).

    • CIVL_LIB_INCLUDE_PATH

      public static final File CIVL_LIB_INCLUDE_PATH
      Where the CIVL header files (suffix .h and .cvh) are located. This path is relative to the class path.

    • LIBRARY_PREFIX

      public static final String LIBRARY_PREFIX
      The prefix of the full name of the class of a library enabler/executor.
      See Also:

    • bar

      public static final String bar
      A string printed before and after titles of sections of output to make them stand out among the clutter.
      See Also:

    • statsBar

      public static final String statsBar
      See Also:

    • EOS

      public static final int EOS
      The int value of the char '\0', which represents the end of string.
      See Also:

    • CIVLREP

      public static final String CIVLREP
      The name of the directory into which CIVL will store the artifacts it generates.
      See Also:

    • consoleUpdatePeriod

      public static final int consoleUpdatePeriod
      Number of seconds between printing of update messages.
      See Also:

    • webUpdatePeriod

      public static final int webUpdatePeriod
      Number of seconds between saving update messages to disk when in web app mode.
      See Also:

    • DEBUG

      public static String DEBUG

    • TIMEOUT

      public static String TIMEOUT

    • ENABLE_PRINTF

      public static String ENABLE_PRINTF

    • ERROR_BOUND

      public static String ERROR_BOUND

    • MAX_PROCS

      public static String MAX_PROCS

    • ERROR_STATE_EQUIV

      public static String ERROR_STATE_EQUIV

    • GUIDED

      public static String GUIDED

    • ID

      public static String ID

    • INPUT

      public static String INPUT

    • MAX_DEPTH

      public static String MAX_DEPTH

    • MIN

      public static String MIN

    • MPI_CONTRACT

      public static String MPI_CONTRACT

    • MPI_MODEL

      public static String MPI_MODEL

    • LOOP_INV

      public static String LOOP_INV

    • CONVERGE_W_MEM_EQ

      public static String CONVERGE_W_MEM_EQ

    • PROC_BOUND

      public static String PROC_BOUND

    • RANDOM

      public static String RANDOM

    • SAVE_STATES

      public static String SAVE_STATES

    • SEED

      public static String SEED

    • ANALYZE_ABS

      public static String ANALYZE_ABS

    • AST

      public static String AST

    • SHOW_AMPLE_SET

      public static String SHOW_AMPLE_SET

    • SHOW_AMPLE_SET_STATES

      public static String SHOW_AMPLE_SET_STATES

    • SHOW_MEM_UNITS

      public static String SHOW_MEM_UNITS

    • SHOW_MODEL

      public static String SHOW_MODEL

    • SHOW_PROVER_QUERIES

      public static String SHOW_PROVER_QUERIES

    • SHOW_QUERIES

      public static String SHOW_QUERIES

    • SHOW_SAVED_STATES

      public static String SHOW_SAVED_STATES

    • SHOW_STATES

      public static String SHOW_STATES

    • SHOW_TIME

      public static String SHOW_TIME

    • SHOW_TRANSITIONS

      public static String SHOW_TRANSITIONS

    • SHOW_UNREACHED

      public static String SHOW_UNREACHED

    • SIMPLIFY

      public static String SIMPLIFY

    • SOLVE

      public static String SOLVE

    • STATELESS_PRINTF

      public static String STATELESS_PRINTF

    • STRICT

      public static String STRICT

    • SYS_INCLUDE_PATH

      public static String SYS_INCLUDE_PATH

    • TRACE

      public static String TRACE

    • USER_INCLUDE_PATH

      public static String USER_INCLUDE_PATH

    • VERBOSE

      public static String VERBOSE

    • GUI

      public static String GUI

    • SHOW_INPUTS

      public static String SHOW_INPUTS

    • PREPROC

      public static String PREPROC

    • PROB

      public static String PROB

    • SHOW_PROGRAM

      public static String SHOW_PROGRAM

    • SHOW_PATH_CONDITION

      public static String SHOW_PATH_CONDITION

    • OMP_NO_SIMPLIFY

      public static String OMP_NO_SIMPLIFY

    • OMP_ONLY_SIMPLIFIER

      public static String OMP_ONLY_SIMPLIFIER

    • COLLECT_OUTPUT

      public static String COLLECT_OUTPUT

    • COLLECT_PROCESSES

      public static String COLLECT_PROCESSES

    • COLLECT_SCOPES

      public static String COLLECT_SCOPES

    • COLLECT_SYMBOLIC_CONSTANTS

      public static String COLLECT_SYMBOLIC_CONSTANTS

    • COLLECT_HEAPS

      public static String COLLECT_HEAPS

    • MACRO

      public static String MACRO

    • WEB

      public static String WEB

    • OMP_LOOP_DECOMP

      public static String OMP_LOOP_DECOMP

    • CIVL_MACRO

      public static String CIVL_MACRO

    • QUIET

      public static String QUIET

    • INT_OPERATION_TRANSFORMER

      public static String INT_OPERATION_TRANSFORMER

    • DIRECT

      public static String DIRECT

    • INTBIT

      public static String INTBIT

    • CYCLES_VIOLATE

      public static String CYCLES_VIOLATE

    • RUNTIME_UPDATE

      public static String RUNTIME_UPDATE

    • PREEMPTION_BOUND

      public static String PREEMPTION_BOUND

    • DISABLE_LOCAL_BLOCK

      public static String DISABLE_LOCAL_BLOCK

    • FAIR

      public static String FAIR

    • DPOR

      public static String DPOR

    • CONTRACT_CHECK_ALL

      public static final String CONTRACT_CHECK_ALL
      Default option value for -mpiContract option mpiContractO
      See Also:

    • CONTRACT_CHECK_NONE

      public static final String CONTRACT_CHECK_NONE
      Default option value for -mpiContract option mpiContractO
      See Also:

    • debugO

      public static final dev.civl.gmc.Option debugO
      Debug option, false by default.

    • timeoutO

      public static final dev.civl.gmc.Option timeoutO

    • enablePrintfO

      public static final dev.civl.gmc.Option enablePrintfO
      Enables printf? true by default. When false, nothing is printed for printf function.

    • errorBoundO

      public static final dev.civl.gmc.Option errorBoundO
      The maximal number of errors allowed before terminating CIVL. 1 by default.

    • maxProcsO

      public static final dev.civl.gmc.Option maxProcsO

    • errorStateEquivO

      public static final dev.civl.gmc.Option errorStateEquivO
      The semantics for used to determine when error states are equivalent; CIVL suppresses logging of equivalent states. All semantics use the kind of error, but they may vary in the portion of the state that is checked. Current options include using the current location (LOC), the call stacks (CALLSTACK), and the full trace (FULL), but others are possible. LOC by default.

    • guidedO

      public static final dev.civl.gmc.Option guidedO
      User guided simulation?

    • idO

      public static final dev.civl.gmc.Option idO
      The id of the trace for replay, 0 by default.

    • inputO

      public static final dev.civl.gmc.Option inputO
      Specify values of input variables.

    • maxdepthO

      public static final dev.civl.gmc.Option maxdepthO
      The maximal depth for search. Infinite by default.

    • minO

      public static final dev.civl.gmc.Option minO
      Search for the minimum counterexample? false by default.

    • mpiContractO

      public static final dev.civl.gmc.Option mpiContractO
      MPI contract mode? Disable by default.

    • mpiModelO

      public static final dev.civl.gmc.Option mpiModelO
      Chooses MPI implementation models (see CIVLConstants.MPIModelKind). CIVLConstants.MPIModelKind.BLOCKING is the default setting.

    • loopO

      public static final dev.civl.gmc.Option loopO
      Enable all settings that are required for verifying with loop invariants. Disable by default.

    • memEqO

      public static final dev.civl.gmc.Option memEqO

    • procBoundO

      public static final dev.civl.gmc.Option procBoundO
      The bound on number of live processes (no bound if negative). No bound by default.

    • probO

      public static final dev.civl.gmc.Option probO
      Use probabilistic techniques for verifying numeric identifies. False by default.

    • randomO

      public static final dev.civl.gmc.Option randomO

    • runtimeUpdateO

      public static final dev.civl.gmc.Option runtimeUpdateO
      set false to disable CIVL
      invalid reference 
      UpdaterRunnable
      thread. The default value is true

    • saveStatesO

      public static final dev.civl.gmc.Option saveStatesO
      Save states during depth-first search? true by default.

    • seedO

      public static final dev.civl.gmc.Option seedO
      Set the random seed for run mode.

    • intBit

      public static final dev.civl.gmc.Option intBit
      Set the upper bound of integers.

    • analyzeAbsO

      public static final dev.civl.gmc.Option analyzeAbsO
      Analyze abs calls? false by default.

    • astO

      public static final dev.civl.gmc.Option astO
      Show the AST of the program? false by default.

    • showAmpleSetO

      public static final dev.civl.gmc.Option showAmpleSetO
      Print the ample set when it contains more than one processes? false by default.

    • showAmpleSetWtStatesO

      public static final dev.civl.gmc.Option showAmpleSetWtStatesO
      Print ample set and state when ample set contains more than one processes? false by default.

    • showMemoryUnitsO

      public static final dev.civl.gmc.Option showMemoryUnitsO
      Print the impact/reachable memory units when the state contains more than one processes? false by default.

    • showModelO

      public static final dev.civl.gmc.Option showModelO
      Show the CIVL model of the program? false by default.

    • showProverQueriesO

      public static final dev.civl.gmc.Option showProverQueriesO
      Show theorem prover queries? false by default.

    • showQueriesO

      public static final dev.civl.gmc.Option showQueriesO
      Show all SARL queries? false by default.

    • showSavedStatesO

      public static final dev.civl.gmc.Option showSavedStatesO
      Show all states that are saved? false by default.

    • showStatesO

      public static final dev.civl.gmc.Option showStatesO
      Show all states? false by default.

    • showTimeO

      public static final dev.civl.gmc.Option showTimeO
      Show the time used by each translation phase? false by default.

    • showTransitionsO

      public static final dev.civl.gmc.Option showTransitionsO
      Show all transitions? false by default;

    • showUnreachedCodeO

      public static final dev.civl.gmc.Option showUnreachedCodeO
      Show unreachable code? false by default;

    • simplifyO

      public static final dev.civl.gmc.Option simplifyO
      Simplify states using path conditions? true by default.

    • solveO

      public static final dev.civl.gmc.Option solveO
      Try to solve for concrete counterexample? false by default.

    • statelessPrintfO

      public static final dev.civl.gmc.Option statelessPrintfO
      Don't modify file system when running printf? true by default.

    • strictCompareO

      public static final dev.civl.gmc.Option strictCompareO
      Print the impact/reachable memory units when the state contains more than one processes? false by default.

    • sysIncludePathO

      public static final dev.civl.gmc.Option sysIncludePathO
      Set the system include path.

    • traceO

      public static final dev.civl.gmc.Option traceO
      File name of trace to replay

    • userIncludePathO

      public static final dev.civl.gmc.Option userIncludePathO
      Sets user include path.

    • verboseO

      public static final dev.civl.gmc.Option verboseO
      Verbose mode? false by default

    • showInputVarsO

      public static final dev.civl.gmc.Option showInputVarsO
      Show the input variables of this model? false by default.

    • preprocO

      public static final dev.civl.gmc.Option preprocO
      Show the preprocessing result? false by default.

    • showProgramO

      public static final dev.civl.gmc.Option showProgramO
      Show the program after all applicable transformations? false by default.

    • showPathConditionO

      public static final dev.civl.gmc.Option showPathConditionO
      Show the path condition of each state? false by default.

    • ompNoSimplifyO

      public static final dev.civl.gmc.Option ompNoSimplifyO
      Don't simplify OpenMP pragmas? false by default.

    • ompOnlySimplifierO

      public static final dev.civl.gmc.Option ompOnlySimplifierO
      Only relies on the OpenMP simplifier ? i.e., either simplify an omp program or report possible data-race

    • collectOutputO

      public static final dev.civl.gmc.Option collectOutputO
      Collect output? false by default.

    • collectProcessesO

      public static final dev.civl.gmc.Option collectProcessesO
      Collect processes? true by default.

    • collectScopesO

      public static final dev.civl.gmc.Option collectScopesO
      Collect scopes? true by default.

    • collectSymbolicConstantsO

      public static final dev.civl.gmc.Option collectSymbolicConstantsO
      Collect symbolic constants ? false by default.

    • collectHeapsO

      public static final dev.civl.gmc.Option collectHeapsO
      Collect heaps? true by default.

    • linkO

      public static final dev.civl.gmc.Option linkO
      Link a source file with the target program.

    • macroO

      public static final dev.civl.gmc.Option macroO
      Define macros.

    • webO

      public static final dev.civl.gmc.Option webO
      Write output for web app? false by default.

    • ompLoopDecompO

      public static final dev.civl.gmc.Option ompLoopDecompO
      Set the loop decomposition strategy for OpenMP transformer. Round robin by default.

    • CIVLMacroO

      public static final dev.civl.gmc.Option CIVLMacroO
      Collect heaps? true by default.

    • quietO

      public static final dev.civl.gmc.Option quietO
      Ignore the output? false by default.

    • intOperationTransformer

      public static final dev.civl.gmc.Option intOperationTransformer
      apply int operation transformer? true by default.

    • direct0

      public static final dev.civl.gmc.Option direct0
      Inject instrumentation to direct the branches at the line numbers in given file so as to explore a sub-space of execution. Note: currently assumes you are given one C file (no linking)

    • preemptionBoundO

      public static final dev.civl.gmc.Option preemptionBoundO

    • disableLocalBlockO

      public static final dev.civl.gmc.Option disableLocalBlockO
      Disable the local block, which optimizes the POR impl. false by default

    • fairO

      public static final dev.civl.gmc.Option fairO
      If this is true, and termination is being checked, then a cycle in which some process remains enabled at each state will not be considered a violation of non-termination (as it is not considered to represent a real execution).

    • dporO

      public static final dev.civl.gmc.Option dporO
      Specifies whether to use DPOR algorithm for model checking. Currently, this is incompatible with the "collectProcesses" option. So when dpor is marked true, process collection is turned off.

    • civlSystemFunction

      public static final String civlSystemFunction
      The name of the CIVL system function, which is the starting point of a CIVL model.
      See Also:

    • SYS_MMAN

      public static final String SYS_MMAN
      Library headers
      See Also:

    • SYS_RESOURCE

      public static final String SYS_RESOURCE
      See Also:

    • SYS_TIME

      public static final String SYS_TIME
      See Also:

    • SYS_TIMES

      public static final String SYS_TIMES
      See Also:

    • SYS_TYPES

      public static final String SYS_TYPES
      See Also:

    • ASSERT

      public static final String ASSERT
      See Also:

    • COMPLEX

      public static final String COMPLEX
      See Also:

    • CTYPE

      public static final String CTYPE
      See Also:

    • CUDA_RUNTIME_API

      public static final String CUDA_RUNTIME_API
      See Also:

    • CUDA

      public static final String CUDA
      See Also:

    • ERRNO

      public static final String ERRNO
      See Also:

    • FENV

      public static final String FENV
      See Also:

    • FLOAT

      public static final String FLOAT
      See Also:

    • GD_IO

      public static final String GD_IO
      See Also:

    • GD

      public static final String GD
      See Also:

    • GDFX

      public static final String GDFX
      See Also:

    • GNUC

      public static final String GNUC
      See Also:

    • INTTYPES

      public static final String INTTYPES
      See Also:

    • ISO646

      public static final String ISO646
      See Also:

    • LIMITS

      public static final String LIMITS
      See Also:

    • LOCALE

      public static final String LOCALE
      See Also:

    • MATH

      public static final String MATH
      See Also:

    • MPI

      public static final String MPI
      See Also:

    • OMP

      public static final String OMP
      See Also:

    • OP

      public static final String OP
      See Also:

    • PTHREAD

      public static final String PTHREAD
      See Also:

    • SCHED

      public static final String SCHED
      See Also:

    • SETJMP

      public static final String SETJMP
      See Also:

    • SIGNAL

      public static final String SIGNAL
      See Also:

    • STDALIGN

      public static final String STDALIGN
      See Also:

    • STDARG

      public static final String STDARG
      See Also:

    • STDATOMIC

      public static final String STDATOMIC
      See Also:

    • STDBOOL

      public static final String STDBOOL
      See Also:

    • STDDEF

      public static final String STDDEF
      See Also:

    • STDINT

      public static final String STDINT
      See Also:

    • STDIO

      public static final String STDIO
      See Also:

    • STDLIB

      public static final String STDLIB
      See Also:

    • STDNORETURN

      public static final String STDNORETURN
      See Also:

    • STRING

      public static final String STRING
      See Also:

    • STRINGS

      public static final String STRINGS
      See Also:

    • TGMATH

      public static final String TGMATH
      See Also:

    • THREADS

      public static final String THREADS
      See Also:

    • TIME

      public static final String TIME
      See Also:

    • UCHAR

      public static final String UCHAR
      See Also:

    • UNISTD

      public static final String UNISTD
      See Also:

    • WCHAR

      public static final String WCHAR
      See Also:

    • WCTYPE

      public static final String WCTYPE
      See Also:

    • BUNDLE

      public static final String BUNDLE
      See Also:

    • CIVLC

      public static final String CIVLC
      See Also:

    • CIVL_CUDA

      public static final String CIVL_CUDA
      See Also:

    • CIVL_MPI

      public static final String CIVL_MPI
      See Also:

    • CIVL_MPI_BLOCKING

      public static final String CIVL_MPI_BLOCKING
      See Also:

    • CIVL_MPI_NONBLOCKING

      public static final String CIVL_MPI_NONBLOCKING
      See Also:

    • CIVL_OMP

      public static final String CIVL_OMP
      See Also:

    • CIVL_PTHREAD

      public static final String CIVL_PTHREAD
      See Also:

    • CIVL_STDIO

      public static final String CIVL_STDIO
      See Also:

    • CMON

      public static final String CMON
      See Also:

    • COMM

      public static final String COMM
      See Also:

    • COMM2

      public static final String COMM2
      See Also:

    • CONCURRENCY

      public static final String CONCURRENCY
      See Also:

    • DOMAIN

      public static final String DOMAIN
      See Also:

    • FORTRAN_ARRAY

      public static final String FORTRAN_ARRAY
      See Also:

    • FORTRAN_SIGP

      public static final String FORTRAN_SIGP
      See Also:

    • LOOP_ASSIGNS_GEN

      public static final String LOOP_ASSIGNS_GEN
      See Also:

    • MEM

      public static final String MEM
      See Also:

    • MPI_DEFS

      public static final String MPI_DEFS
      See Also:

    • POINTER

      public static final String POINTER
      See Also:

    • SCOPE

      public static final String SCOPE
      See Also:

    • SEQ

      public static final String SEQ
      See Also:

    • ASSERT_SRC

      public static final String ASSERT_SRC
      Library source files
      See Also:

    • CUDA_SRC

      public static final String CUDA_SRC
      See Also:

    • MATH_SRC

      public static final String MATH_SRC
      See Also:

    • MPI_SRC

      public static final String MPI_SRC
      See Also:

    • OMP_SRC

      public static final String OMP_SRC
      See Also:

    • PTHREAD_SRC

      public static final String PTHREAD_SRC
      See Also:

    • SCHED_SRC

      public static final String SCHED_SRC
      See Also:

    • STDING_SRC

      public static final String STDING_SRC
      See Also:

    • STDIO_SRC

      public static final String STDIO_SRC
      See Also:

    • STDLIB_SRC

      public static final String STDLIB_SRC
      See Also:

    • STRING_SRC

      public static final String STRING_SRC
      See Also:

    • SYS_TIME_SRC

      public static final String SYS_TIME_SRC
      See Also:

    • TIME_SRC

      public static final String TIME_SRC
      See Also:

    • TIMES_SRC

      public static final String TIMES_SRC
      See Also:

    • UNISTD_SRC

      public static final String UNISTD_SRC
      See Also:

    • BUNDLE_SRC

      public static final String BUNDLE_SRC
      See Also:

    • CIVLC_SRC

      public static final String CIVLC_SRC
      See Also:

    • CIVL_CUDA_SRC

      public static final String CIVL_CUDA_SRC
      See Also:

    • CIVL_MPI_BLOCKING_SRC

      public static final String CIVL_MPI_BLOCKING_SRC
      See Also:

    • CIVL_MPI_NONBLOCKING_SRC

      public static final String CIVL_MPI_NONBLOCKING_SRC
      See Also:

    • CIVL_OMP_SRC

      public static final String CIVL_OMP_SRC
      See Also:

    • CIVL_OMP2_SRC

      public static final String CIVL_OMP2_SRC
      See Also:

    • CIVL_PTHREAD_SRC

      public static final String CIVL_PTHREAD_SRC
      See Also:

    • CMON_SRC

      public static final String CMON_SRC
      See Also:

    • COLLATE_SRC

      public static final String COLLATE_SRC
      See Also:

    • COMM_SRC

      public static final String COMM_SRC
      See Also:

    • CONCURRENCY_SRC

      public static final String CONCURRENCY_SRC
      See Also:

    • FORTRAN_ARRAY_SRC

      public static final String FORTRAN_ARRAY_SRC
      See Also:

    • FORTRAN_SIGP_SRC

      public static final String FORTRAN_SIGP_SRC
      See Also:

    • INT_DIV_NO_CHECKING_SRC

      public static final String INT_DIV_NO_CHECKING_SRC
      See Also:

    • INT_DIV_SRC

      public static final String INT_DIV_SRC
      See Also:

    • LOOP_ASSIGNS_GEN_SRC

      public static final String LOOP_ASSIGNS_GEN_SRC
      See Also:

    • MPI_DEFS_SRC

      public static final String MPI_DEFS_SRC
      See Also:

    • SEQ_SRC

      public static final String SEQ_SRC
      See Also:

    • UNSIGNED_ARITH_SRC

      public static final String UNSIGNED_ARITH_SRC
      See Also:

  • Constructor Details

    • CIVLConstants

      public CIVLConstants()

  • Method Details

    • getAllOptions

      public static final dev.civl.gmc.Option[] getAllOptions()
      Returns all options defined for CIVL in alphabetic order.
      Returns:
      all options defined for CIVL in alphabetic order.

    • getCStdLibHeaders

      public static final Set<String> getCStdLibHeaders()
      Returns:
      all standard c library headers.

    • getCivlLibHeaders

      public static final Set<String> getCivlLibHeaders()
      Returns:
      all CIVL-C library headers.

    • getAllLibHeaders

      public static final Set<String> getAllLibHeaders()
      Returns:
      all library headers, both from CIVL-C and the standard library.

    • getCStdLibSrcs

      public static final Set<String> getCStdLibSrcs()

    • getCivlLibSrcs

      public static final Set<String> getCivlLibSrcs()

    • getAllLibSrcs

      public static final Set<String> getAllLibSrcs()
      Returns:
      all library headers, both from CIVL-C and the standard library.

    • getAllLibFilenames

      public static final Set<String> getAllLibFilenames()