aarch64 orphanage: handleHypervisorFault_no_orphans #2881

Sign in to view logs

Triggered via push March 1, 2024 20:49

lsf37

aarch64

Status Success

Total duration 30s

Artifacts –

push.yml

on: push

Annotations

7 errors

Unfinished proof: proof/crefine/AARCH64/Fastpath_C.thy#L1755

This command indicates an unfinished or aborted proof.

Unfinished proof: proof/crefine/AARCH64/Fastpath_C.thy#L2571

This command indicates an unfinished or aborted proof.

Unfinished proof: proof/crefine/AARCH64/Fastpath_Equiv.thy#L549

This command indicates an unfinished or aborted proof.

Unfinished proof: proof/crefine/AARCH64/Fastpath_Equiv.thy#L1423

This command indicates an unfinished or aborted proof.

Axioms: proof/crefine/AARCH64/Init_C.thy#L17

Locales or definitions should usually be preferred to axioms, because axioms may make the logic inconsistent. Merely introducing a new constant (without new laws) is fine, though.

Unfinished proof: proof/crefine/AARCH64/IpcCancel_C.thy#L2775

This command indicates an unfinished or aborted proof.

Unfinished proof: proof/crefine/AARCH64/IpcCancel_C.thy#L2950

This command indicates an unfinished or aborted proof.