index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tests
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge branch 'main' into son/loops2
Son Ho
2024-06-04
169
-5583
/
+2423
|
\
|
*
Improve the tests README
Nadrieril
2024-05-30
2
-14
/
+22
|
*
runner: Factor out backend-specific options
Nadrieril
2024-05-30
2
-49
/
+56
|
*
runner: Split up into multiple files
Nadrieril
2024-05-30
6
-198
/
+191
|
*
runner: make the backend map a submodule of `Backend`
Nadrieril
2024-05-30
1
-36
/
+48
|
*
tests: Add a README
Nadrieril
2024-05-30
1
-0
/
+67
|
*
Fix an issue with some names being ignored when generating unique variable names
Son Ho
2024-05-28
2
-4
/
+4
|
*
Reactivate the infinite-loop.rs test
Son Ho
2024-05-28
4
-1
/
+76
|
*
tests: Rename hashmap_utils -> utils
Nadrieril
2024-05-28
13
-42
/
+40
|
*
Add some tests
Nadrieril
2024-05-28
8
-0
/
+178
|
*
runner: Store options for crate tests in a separate file
Nadrieril
2024-05-28
2
-30
/
+14
|
*
tests: Rename betree_main -> betree
Nadrieril
2024-05-28
30
-363
/
+359
|
*
tests: Merge the hashmap test files
Nadrieril
2024-05-27
42
-3992
/
+279
|
*
runner: Add `no-check-output` option for unstable outputs
Nadrieril
2024-05-27
3
-27
/
+31
|
*
runner: Support negative tests
Nadrieril
2024-05-27
7
-20
/
+113
|
*
runner: Correctly catch command exit status
Nadrieril
2024-05-27
2
-29
/
+40
|
*
Merge pull request #206 from AeneasVerif/subdir
Guillaume Boisseau
2024-05-24
85
-609
/
+633
|
|
\
|
|
*
Rename some subdirectories for consistency
Nadrieril
2024-05-24
50
-13
/
+7
|
|
*
Update output files
Nadrieril
2024-05-24
26
-554
/
+554
|
|
*
runner: Specify subdirectory in magic comments
Nadrieril
2024-05-24
9
-15
/
+24
|
|
*
runner: Factor out useful `BackendMap` operations
Nadrieril
2024-05-24
1
-33
/
+26
|
|
*
runner: Allow per-backend skipping
Nadrieril
2024-05-24
1
-19
/
+46
|
|
*
runner: Allow filenames with dashes
Nadrieril
2024-05-24
2
-1
/
+2
|
|
*
fix generated file
Nadrieril
2024-05-24
1
-1
/
+1
|
*
|
Update an .opam file
Son Ho
2024-05-24
1
-1
/
+1
|
*
|
Merge branch 'main' into afromher/recursive_projectors
Son Ho
2024-05-24
88
-3301
/
+5623
|
|
\
|
|
|
*
Update test outputs
Nadrieril
2024-05-24
51
-1219
/
+1219
|
|
*
runner: Pass options in special comments
Nadrieril
2024-05-24
16
-78
/
+150
|
|
*
runner: define an Input module
Nadrieril
2024-05-24
1
-90
/
+92
|
|
*
runner: Strongly typed Backend enum
Nadrieril
2024-05-24
2
-62
/
+88
|
|
*
Downgrade the version of dune
Son Ho
2024-05-24
1
-1
/
+1
|
*
|
Regenerate Lean files for betree
Aymeric Fromherz
2024-05-23
1
-0
/
+4
|
*
|
Regenerate Lean files for betree following extraction changes
Aymeric Fromherz
2024-05-23
2
-47
/
+46
*
|
|
Add a test
Son Ho
2024-06-03
4
-103
/
+123
*
|
|
Regenerate tests
Aymeric Fromherz
2024-05-31
13
-35
/
+35
*
|
|
Regenerate test output
Aymeric Fromherz
2024-05-31
19
-108
/
+2588
*
|
|
Implement two phases of loops join + collapse
Aymeric Fromherz
2024-05-30
19
-2588
/
+108
*
|
|
Add type and set/map for marker and borrow id
Aymeric Fromherz
2024-05-28
1
-1
/
+1
*
|
|
Downgrade the version of dune
Son Ho
2024-05-24
1
-1
/
+1
|
|
/
|
/
|
*
|
runner: Use full path and use an enum for crate vs file
Nadrieril
2024-05-24
1
-42
/
+54
*
|
runner: Do both steps of generation at once
Nadrieril
2024-05-24
1
-22
/
+24
*
|
Auto-detect test cases
Nadrieril
2024-05-24
2
-17
/
+23
*
|
Use runner to generate llbc
Nadrieril
2024-05-24
1
-20
/
+104
*
|
Tweak a path
Nadrieril
2024-05-24
51
-1219
/
+1219
*
|
Import test suite from charon
Nadrieril
2024-05-24
25
-1
/
+4016
*
|
Remove secondary betree test
Nadrieril
2024-05-24
9
-2100
/
+4
*
|
Let the runner choose which backends to use
Nadrieril
2024-05-24
1
-15
/
+23
*
|
Cleanup test runner
Nadrieril
2024-05-24
1
-99
/
+124
*
|
Set all options in the test runner
Nadrieril
2024-05-24
1
-0
/
+57
*
|
Move the subdirectory selection to the test runner
Nadrieril
2024-05-24
1
-3
/
+26
[next]