isla 0.2.0

Isla is a symbolic execution engine for Sail instruction set architecture specifications.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

default Order dec

$include <prelude.sail>

val "assume" : bool -> unit

struct my_struct = {
  field1: int,
  field2: bits(64),
}

function prop() -> bool = {
  let x: int = undefined;
  assume(x >= 0 & x < 64);
  let y: bits(64) = undefined;
  var z: my_struct = undefined;
  z.field1 = x;
  z.field2 = y;
  z.field1 == x & z.field2 == y
}