Skip to content

Commit

Permalink
Add regression tests for #904.
Browse files Browse the repository at this point in the history
The goal is to ensure that ill-formed JVMSetup blocks are caught
at an early stage by `crucible_jvm_unsafe_assume_spec`.

The tests also include a bunch of known false positives for other
well-formedness checks on JVMSetup blocks that we do not perform
yet.
  • Loading branch information
Brian Huffman committed Nov 25, 2020
1 parent 4c31c07 commit 1928b03
Show file tree
Hide file tree
Showing 5 changed files with 508 additions and 0 deletions.
2 changes: 2 additions & 0 deletions intTests/test_jvm_setup_errors/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
%.class: %.java
javac -g $<
Binary file added intTests/test_jvm_setup_errors/Test.class
Binary file not shown.
17 changes: 17 additions & 0 deletions intTests/test_jvm_setup_errors/Test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
class Test
{
long val;

long get () {
return val;
}
void set (long x) {
val = x;
}
boolean lessThan (Test t) {
return val < t.val;
}
static long lookup (long arr[], int idx) {
return arr[idx];
}
}
Loading

0 comments on commit 1928b03

Please sign in to comment.