Constant Field Values

Contents

• dev.civl.*

dev.civl.*

dev.civl.mc.analysis.IF.Analysis

Modifier and Type	Constant Field	Value
public static final String	ABS	"abs"

dev.civl.mc.config.IF.CIVLConstants

Modifier and Type	Constant Field	Value
public static final String	ASSERT	"assert.h"
public static final String	ASSERT_SRC	"assert.cvl"
public static final String	bar	"==================="
public static final String	BUNDLE	"bundle.cvh"
public static final String	BUNDLE_SRC	"bundle.cvl"
public static final String	CIVL_CUDA	"civl-cuda.cvh"
public static final String	CIVL_CUDA_SRC	"civl-cuda.cvl"
public static final String	CIVL_MPI	"civl-mpi.cvh"
public static final String	CIVL_MPI_BLOCKING	"civl-mpi-blocking.cvh"
public static final String	CIVL_MPI_BLOCKING_SRC	"civl-mpi-blocking.cvl"
public static final String	CIVL_MPI_NONBLOCKING	"civl-mpi-nonblocking.cvh"
public static final String	CIVL_MPI_NONBLOCKING_SRC	"civl-mpi-nonblocking.cvl"
public static final String	CIVL_OMP	"civl-omp.cvh"
public static final String	CIVL_OMP_SRC	"civl-omp.cvl"
public static final String	CIVL_OMP2_SRC	"civl-omp2.cvl"
public static final String	CIVL_PTHREAD	"civl-pthread.cvh"
public static final String	CIVL_PTHREAD_SRC	"civl-pthread.cvl"
public static final String	CIVL_STDIO	"civl-stdio.cvh"
public static final String	CIVLC	"civlc.cvh"
public static final String	CIVLC_SRC	"civlc.cvl"
public static final String	CIVLREP	"CIVLREP"
public static final String	civlSystemFunction	"main"
public static final String	COLLATE	"collate.cvh"
public static final String	COLLATE_SRC	"collate.cvl"
public static final String	COMM	"comm.cvh"
public static final String	COMM_SRC	"comm.cvl"
public static final String	COMM2	"comm2.cvh"
public static final String	COMPLEX	"complex.h"
public static final String	CONCURRENCY	"concurrency.cvh"
public static final String	CONCURRENCY_CONTRACT	"concurrency_contract.cvh"
public static final String	CONCURRENCY_SRC	"concurrency.cvl"
public static final int	consoleUpdatePeriod	15
public static final String	CONTRACT_CHECK_ALL	"_CIVL_CONTRACT_ALL"
public static final String	CONTRACT_CHECK_NONE	"_CIVL_CONTRACT_NONE"
public static final String	CTYPE	"ctype.h"
public static final String	CUDA	"cuda.h"
public static final String	CUDA_RUNTIME_API	"cuda_runtime_api.h"
public static final String	CUDA_SRC	"cuda.cvl"
public static final String	date	"2023-10-09"
public static final String	DOMAIN	"domain.cvh"
public static final int	EOS	0
public static final String	ERRNO	"errno.h"
public static final String	FENV	"fenv.h"
public static final String	FLOAT	"float.h"
public static final String	FORTRAN_ARRAY	"fortran_array.cvh"
public static final String	FORTRAN_ARRAY_SRC	"fortran_array.cvl"
public static final String	FORTRAN_SIGP	"fortran_sigp.cvh"
public static final String	FORTRAN_SIGP_SRC	"fortran_sigp.cvl"
public static final String	GD	"gd.h"
public static final String	GD_IO	"gd_io.h"
public static final String	GDFX	"gdfx.h"
public static final String	GNUC	"gnuc.h"
public static final String	INT_DIV_NO_CHECKING_SRC	"int_div_no_checking.cvl"
public static final String	INT_DIV_SRC	"int_div.cvl"
public static final String	INTTYPES	"inttypes.h"
public static final String	ISO646	"iso646.h"
public static final String	LIBRARY_PREFIX	"dev.civl.mc.library."
public static final String	LIMITS	"limits.h"
public static final String	LOCALE	"locale.h"
public static final String	LOOP_ASSIGNS_GEN	"loop_assigns_gen.cvh"
public static final String	LOOP_ASSIGNS_GEN_SRC	"loop_assigns_gen.cvl"
public static final String	MATH	"math.h"
public static final String	MATH_SRC	"math.cvl"
public static final String	MEM	"mem.cvh"
public static final String	MEMORY	"memory.cvh"
public static final String	MPI	"mpi.h"
public static final String	MPI_SRC	"mpi.cvl"
public static final String	OMP	"omp.h"
public static final String	OMP_SRC	"omp.cvl"
public static final String	OP	"op.h"
public static final String	POINTER	"pointer.cvh"
public static final String	PTHREAD	"pthread.h"
public static final String	PTHREAD_SRC	"pthread.cvl"
public static final String	ROOT_RESOURCE_PATH_STR	"dev/civl/"
public static final String	SCHED	"sched.h"
public static final String	SCHED_SRC	"sched.cvl"
public static final String	SCOPE	"scope.cvh"
public static final String	SEQ	"seq.cvh"
public static final String	SEQ_SRC	"seq.cvl"
public static final String	SETJMP	"setjmp.h"
public static final String	SIGNAL	"signal.h"
public static final String	statsBar	"==="
public static final String	STDALIGN	"stdalign.h"
public static final String	STDARG	"stdarg.h"
public static final String	STDATOMIC	"stdatomic.h"
public static final String	STDBOOL	"stdbool.h"
public static final String	STDDEF	"stddef.h"
public static final String	STDING_SRC	"stding.cvl"
public static final String	STDINT	"stdint.h"
public static final String	STDIO	"stdio.h"
public static final String	STDIO_SRC	"stdio.cvl"
public static final String	STDLIB	"stdlib.h"
public static final String	STDLIB_SRC	"stdlib.cvl"
public static final String	STDNORETURN	"stdnoreturn.h"
public static final String	STRING	"string.h"
public static final String	STRING_SRC	"string.cvl"
public static final String	STRINGS	"strings.h"
public static final String	SVCOMP	"svcomp.h"
public static final String	SVCOMP_SRC	"svcomp.cvl"
public static final String	SYS_MMAN	"sys/mman.h"
public static final String	SYS_RESOURCE	"sys/resource.h"
public static final String	SYS_TIME	"sys/time.h"
public static final String	SYS_TIME_SRC	"sys-time.cvl"
public static final String	SYS_TIMES	"sys/times.h"
public static final String	SYS_TYPES	"sys/types.h"
public static final String	TGMATH	"tgmath.h"
public static final String	THREADS	"threads.h"
public static final String	TIME	"time.h"
public static final String	TIME_SRC	"time.cvl"
public static final String	TIMES_SRC	"times.cvl"
public static final String	UCHAR	"uchar.h"
public static final String	UNISTD	"unistd.h"
public static final String	UNISTD_SRC	"unistd.cvl"
public static final String	UNSIGNED_ARITH_SRC	"unsigned_arith.cvl"
public static final String	version	"1.22"
public static final String	WCHAR	"wchar.h"
public static final String	WCTYPE	"wctype.h"
public static final int	webUpdatePeriod	1

dev.civl.mc.model.IF.LogicFunction

Modifier and Type	Constant Field	Value
public static final String	RESERVED_PERMUT	"permut"

dev.civl.mc.model.IF.ModelConfiguration

Modifier and Type	Constant Field	Value
public static final String	ANONYMOUS_VARIABLE_PREFIX	"_anon_"
public static final String	ATOMIC_LOCK_VARIABLE_INDEX	"_atomic_lock_var"
public static final String	BARRIER_TYPE	"_barrier"
public static final String	BROKEN_TIME_VARIABLE	"_broken_time_var"
public static final String	BUNDLE_TYPE	"_bundle"
public static final String	COLLATE_STATE	"$collate_state"
public static final String	COLLATOR_TYPE	"$collator"
public static final String	COMM_TYPE	"_comm"
public static final String	COMM_WORLD	"MPI_COMM_WORLD"
public static final String	ContractMPICommRankName	"$mpi_comm_rank"
public static final String	ContractMPICommSizeName	"$mpi_comm_size"
public static final String	ContractResultName	"$result"
public static final int	DECOMP_ALL	0
public static final int	DECOMP_RANDOM	1
public static final int	DECOMP_ROUND_ROBIN	2
public static final int	DYNAMIC_CONSTANT_SCOPE	-1
public static final int	DYNAMIC_NULL_SCOPE	-2
public static final String	DYNAMIC_TYPE	"$dynamic"
public static final String	DYNAMIC_TYPE_NAME	"dynamicType"
public static final int	DYNAMIC_UNDEFINED_SCOPE	-1
public static final String	FILE_STREAM_TYPE	"FILE"
public static final String	FILE_SYSTEM_TYPE	"CIVL_filesystem"
public static final String	FILESYSTEM	"_io_filesystem"
public static final String	GBARRIER_TYPE	"_gbarrier"
public static final String	GCOLLATE_STATE	"$gcollate_state"
public static final String	GCOLLATOR_TYPE	"$gcollator"
public static final String	GCOMM_TYPE	"$gcomm"
public static final String	GCOMM_WORLD	"_mpi_gcomm"
public static final String	GCOMMS	"_mpi_gcomms"
public static final String	GENERAL_ROOT	"_civl_root"
public static final int	HAVOC_PREFIX_INDEX	1
public static final int	HEAP_OBJECT_PREFIX_INDEX	2
public static final String	HEAP_TYPE	"$heap"
public static final String	HEAP_VAR	"_heap"
public static final int	HEAP_VARIABLE_INDEX	0
public static final int	INPUT_PREIFX_INDEX	0
public static final String	INT_ITER_TYPE	"$int_iter"
public static final String	INVALID	"INVALID"
public static final String	MESSAGE_TYPE	"_message"
public static final String	MPI_SYS_STATUS	"_mpi_status"
public static final String	NEXT_TIME_COUNT	"$next_time_count"
public static final String	NPROCS	"_mpi_nprocs"
public static final String	NPROCS_LOWER_BOUND	"_mpi_nprocs_lo"
public static final String	NPROCS_UPPER_BOUND	"_mpi_nprocs_hi"
public static final int	NULL_POINTER_DYSCOPE	-1
public static final int	NULL_POINTER_VID	-1
public static final String	PROC_TYPE	"$proc"
public static final String	PTHREAD_GPOOL	"_pthread_gpool_t"
public static final String	PTHREAD_POOL	"_pthread_pool_t"
public static final String	PTHREAD_THREAD_TYPE	"pthread_t"
public static final String	QUEUE_TYPE	"_queue"
public static final String	RANGE_TYPE	"$range"
public static final String	REAL_FILE_TYPE	"$file"
public static final String	SCOPE_TYPE	"$scope"
public static final int	STATIC_CONSTANT_SCOPE	0
public static final int	STATIC_ROOT_SCOPE	1
public static final String	TIME_COUNT_VARIABLE	"_time_count_var"
public static final String	TIME_LIB	"time.h"
public static final String	TM_TYPE	"tm"
public static final int	UNDEFINED_PROC_ID	-1

dev.civl.mc.run.IF.CommandLine

Modifier and Type	Constant Field	Value
public static final String	COMPARE	"compare"
public static final String	CONFIG	"config"
public static final String	GUI	"gui"
public static final String	HELP	"help"
public static final String	REPLAY	"replay"
public static final String	RUN	"run"
public static final String	SHOW	"show"
public static final String	VERIFY	"verify"

dev.civl.mc.run.IF.UserInterface

Modifier and Type	Constant Field	Value
public static final boolean	debug	false

dev.civl.mc.transform.IF.ContractTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"contract"
public static final String	LONG_NAME	"ContractTransformer"
public static final String	SHORT_DESCRIPTION	"transforms C/MPI program to a set of programs each of which verifies a single function"

dev.civl.mc.transform.IF.Cuda2CIVLTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"cuda"

dev.civl.mc.transform.IF.DirectingTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"direct"
public static final String	LONG_NAME	"DirectedSymEx"
public static final String	SHORT_DESCRIPTION	"instruments model to direct sybolic execution"

dev.civl.mc.transform.IF.GeneralTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"general"
public static final String	LONG_NAME	"GeneralTransformer"
public static final String	PREFIX	"_civl_"
public static final String	SHORT_DESCRIPTION	"transforms general features of C programs to CIVL-C"

dev.civl.mc.transform.IF.IntOperationTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"int_operation"
public static final String	LONG_NAME	"IntOperationTransformer"
public static final String	SHORT_DESCRIPTION	"integer arithmetic operations to its corresponding library functions."

dev.civl.mc.transform.IF.IOTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"io"
public static final String	LONG_NAME	"IOTransformer"
public static final String	SHORT_DESCRIPTION	"transforms C program with IO to CIVL-C"

dev.civl.mc.transform.IF.LoopContractTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"loop"
public static final String	LONG_NAME	"LoopContractTransformer"
public static final String	SHORT_DESCRIPTION	"transforms loops contracts into CIVL IR."

dev.civl.mc.transform.IF.MacroTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"macro"
public static final String	LONG_NAME	"MacroTransformer"
public static final String	SHORT_DESCRIPTION	"recovers macros from C programs to CIVL-C"

dev.civl.mc.transform.IF.MPI2CIVLTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"mpi"
public static final String	LONG_NAME	"MPITransformer"
public static final String	SHORT_DESCRIPTION	"transforms C/MPI program to CIVL-C"

dev.civl.mc.transform.IF.OpenMP2CIVLTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"openmp"

dev.civl.mc.transform.IF.OpenMPSimplifier

Modifier and Type	Constant Field	Value
public static final String	CODE	"omp_simplifier"
public static final String	LONG_NAME	"OpenMPSimplifier"
public static final String	SHORT_DESCRIPTION	"simplifies independent C/OpenMP constructs"

dev.civl.mc.transform.IF.Pthread2CIVLTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"pthread"
public static final String	LONG_NAME	"PthreadTransformer"
public static final String	SHORT_DESCRIPTION	"transforms C/Pthread program to CIVL-C"

dev.civl.mc.transform.IF.ShortCircuitTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"short-circuit"
public static final String	LONG_NAME	"shortCircuitTransformer"
public static final String	PREFIX	"_shcc_"
public static final String	SHORT_DESCRIPTION	"transforms logical AND, logical OR and logical IMPLIES away to lift short circuit evaluation in CIVL backend"

dev.civl.mc.transform.IF.SvcompTransformer

Modifier and Type	Constant Field	Value
public static final String	CODE	"svcomp"
public static final int	INT_BOUND_LO	-5
public static final int	INT_BOUND_UP	5
public static final String	INT_BOUND_UP_NAME	"_svcomp_int_bound_up"
public static final int	UNPP_SCALE_EVEN	4
public static final int	UNPP_SCALE_ODD	3
public static final int	UNSIGNED_BOUND	4
public static final String	UNSIGNED_BOUND_NAME	"_svcomp_unsigned_bound"

dev.civl.mc.util.IF.Utils

Modifier and Type	Constant Field	Value
public static final String	ANSI_BLACK	"\u001b[30m"
public static final String	ANSI_BLUE	"\u001b[34m"
public static final String	ANSI_BOLD	"\u001b[1m"
public static final String	ANSI_CYAN	"\u001b[36m"
public static final String	ANSI_GREEN	"\u001b[32m"
public static final String	ANSI_OVERSTRIKE	"\u001b[9m"
public static final String	ANSI_OVERSTRIKE_OFF	"\u001b[29m"
public static final String	ANSI_PURPLE	"\u001b[35m"
public static final String	ANSI_RED	"\u001b[31m"
public static final String	ANSI_RESET	"\u001b[0m"
public static final String	ANSI_UNDERLINE	"\u001b[4m"
public static final String	ANSI_UNDERLINE_OFF	"\u001b[24m"
public static final String	ANSI_WHITE	"\u001b[37m"
public static final String	ANSI_YELLOW	"\u001b[33m"