vcg 0.1.0

Utilities for manipulating verification conditions.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

use std::str::FromStr;
use std::fs;
use std::path::PathBuf;
use vcg::{BoundedResult,Program};

pub static REFTESTS_DIR: &str = "tests/files";

// Include the programmatically generated test file.
include!(concat!(env!("OUT_DIR"), "/srcfile_tests.rs"));

/// Run a specific test by loading the file out of the reference tests
/// repository and attempting to parse it.  All reference tests should
/// parse correctly.
fn check(test: &str) {
    // Construct filename
    let mut path = PathBuf::from(REFTESTS_DIR);
    path.push(test);
    let filename = path.as_path().to_str().unwrap();
    // Read the test file
    let input = fs::read_to_string(filename).unwrap();
    // Convert into a program
    let program = Program::from_str(&input).unwrap();
    // Print out errors
    for r in program.check() {
    	match r {
    	    BoundedResult::Ok(_) => {}
    	    BoundedResult::Err(_) => {
    		assert!(false,"verification shouldn't have failed");
    	    }
    	    BoundedResult::OutOfResource => {
    		assert!(false,"verification out-of-resource");
    	    }
    	}
    }
}