rem-verification 0.1.0

Verification tool for the REM toolchain. Built to be implemented into the VSCode extension for REM. Relies on AENEAS and CoQ
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

//! Implements specific error handling for the Verification System

use std::fmt;
use std::error::Error;

#[derive(Debug)]
pub enum AENEASError {
    RuntimeError,
    InvalidPathConversion
}

impl fmt::Display for AENEASError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            AENEASError::RuntimeError => { write!(f, "AENEAS Failed to run. Terminating verification") }
            AENEASError::InvalidPathConversion => { write!(f, "Failed to convert LLBC path to a CoQ path") }
        }
    }
}

impl Error for AENEASError {}