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
*
Update the test runner to allow the syntax [!lean] and [borrow-check]
Son Ho
2024-06-05
14
-34
/
+65
*
Merge branch 'main' into son/clean-synthesis
Son Ho
2024-06-05
33
-407
/
+418
|
\
|
*
Update charon
Nadrieril
2024-06-05
27
-287
/
+278
|
*
Merge branch 'main' into son/loops2
Son Ho
2024-06-04
169
-5583
/
+2423
|
|
\
|
*
|
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
*
|
|
Remove the options from the functions synthesizing the symbolic AST
Son Ho
2024-05-30
1
-6
/
+6
|
|
/
|
/
|
*
|
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
|
|
/
|
*
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
[next]