backend/hu.bme.mit.semantifyr.backend

Package-level declarations

Types

@Serializable

data class BackendMetrics(val preparationDuration: Duration = Duration.ZERO, val verificationDuration: Duration = Duration.ZERO, val backAnnotationDuration: Duration = Duration.ZERO)

BackendUnsupportedException

class BackendUnsupportedException(message: String, cause: Throwable? = null) : Exception

BackendVerificationRequest

data class BackendVerificationRequest(val inlinedOxsts: InlinedOxsts, val artifactOutputPath: Path, val flatteningInfo: FlatteningInfo? = null, val timeout: Duration = Duration.INFINITE)

BackendVerificationResult

data class BackendVerificationResult(val verdict: VerificationVerdict, val metadata: VerificationMetadata, val metrics: BackendMetrics = BackendMetrics(), val inlinedWitness: InlinedWitness? = null, val message: String? = null, val soundness: SoundnessDirection = SoundnessDirection.Exact, val isTrusted: Boolean = verdict.isDecisive)

SoundnessDirection

enum SoundnessDirection : Enum<SoundnessDirection>

UnsupportedConstruct

class UnsupportedConstruct(val element: EObject, val description: String)

VerificationBackend

abstract class VerificationBackend<T : BackendConfig>

VerificationContext

abstract class VerificationContext<TArtifacts, TRawVerdict>(backendId: String, soundness: SoundnessDirection, request: BackendVerificationRequest)

VerificationMetadata

@Serializable

data class VerificationMetadata(val backendId: String?, val startedAt: Instant)

VerificationVerdict

enum VerificationVerdict : Enum<VerificationVerdict>