index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
|
*
|
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
|
/
/
*
|
Merge pull request #149 from RaitoBezarius/reexport-our-charon
Guillaume Boisseau
2024-05-29
2
-0
/
+20
|
\
\
|
*
|
chore: explain a Nix-powered workflow
Ryan Lahfa
2024-05-29
2
-0
/
+20
|
/
/
*
|
Merge pull request #218 from AeneasVerif/ci-check-pin
Guillaume Boisseau
2024-05-29
5
-2
/
+31
|
\
\
|
*
|
ci: Check correctness of the charon pinned commit
Nadrieril
2024-05-29
5
-2
/
+31
|
/
/
*
|
Merge pull request #222 from AeneasVerif/son/readme
Son HO
2024-05-29
1
-6
/
+7
|
\
\
|
*
|
Update the README
Son Ho
2024-05-29
1
-6
/
+7
|
/
/
*
|
Merge pull request #221 from AeneasVerif/son/builtins
Son HO
2024-05-29
2
-163
/
+124
|
\
\
|
*
\
Merge branch 'main' into son/builtins
Son HO
2024-05-29
0
-0
/
+0
|
|
\
\
|
|
/
/
|
/
|
|
*
|
|
Merge pull request #220 from AeneasVerif/son/collisions
Son HO
2024-05-29
3
-25
/
+23
|
\
\
\
|
*
\
\
Merge branch 'main' into son/collisions
Son HO
2024-05-29
0
-0
/
+0
|
|
\
\
\
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge pull request #219 from AeneasVerif/son/infinite
Son HO
2024-05-28
5
-5
/
+77
|
\
\
\
\
|
|
|
*
|
Factor out code in ExtractBuiltin.ml
Son Ho
2024-05-29
2
-163
/
+124
|
|
|
/
/
|
|
*
/
Fix an issue with some names being ignored when generating unique variable names
Son Ho
2024-05-28
3
-25
/
+23
|
|
/
/
|
*
|
Reactivate the infinite-loop.rs test
Son Ho
2024-05-28
4
-1
/
+76
|
*
|
Fix a bug in SymbolicToPure.translate_loop
Son Ho
2024-05-28
1
-4
/
+1
|
/
/
*
|
Merge pull request #213 from AeneasVerif/cleanup-tests
Guillaume Boisseau
2024-05-28
84
-4396
/
+839
|
\
\
|
*
|
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
31
-365
/
+361
|
*
|
tests: Merge the hashmap test files
Nadrieril
2024-05-27
42
-3992
/
+279
|
/
/
*
|
Merge pull request #209 from AeneasVerif/negative-tests
Guillaume Boisseau
2024-05-27
8
-47
/
+159
|
\
\
|
*
|
runner: Add `no-check-output` option for unstable outputs
Nadrieril
2024-05-27
3
-27
/
+31
|
*
|
runner: Support negative tests
Nadrieril
2024-05-27
9
-26
/
+123
|
*
|
runner: Correctly catch command exit status
Nadrieril
2024-05-27
2
-29
/
+40
|
/
/
*
|
Merge pull request #184 from RaitoBezarius/unsigned-max
Son HO
2024-05-27
1
-0
/
+39
|
\
\
|
*
\
Merge branch 'main' into unsigned-max
Son HO
2024-05-27
118
-1449
/
+1626
|
|
\
\
|
|
/
/
|
/
|
|
*
|
|
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
*
|
|
|
Merge pull request #194 from AeneasVerif/afromher/recursive_projectors
Son HO
2024-05-24
5
-69
/
+106
|
\
\
\
\
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Update an .opam file
Son Ho
2024-05-24
1
-1
/
+1
|
*
|
|
Factor out the code for Lean and Coq
Son Ho
2024-05-24
1
-143
/
+41
|
*
|
|
Merge branch 'main' into afromher/recursive_projectors
Son Ho
2024-05-24
147
-8592
/
+10661
|
|
\
\
\
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge pull request #204 from AeneasVerif/test-harness4
Guillaume Boisseau
2024-05-24
69
-1379
/
+1480
|
\
\
\
\
|
*
|
|
|
Update test outputs
Nadrieril
2024-05-24
51
-1219
/
+1219
|
*
|
|
|
runner: Pass options in special comments
Nadrieril
2024-05-24
17
-82
/
+150
|
*
|
|
|
Fix running individual tests
Nadrieril
2024-05-24
1
-3
/
+7
|
*
|
|
|
runner: define an Input module
Nadrieril
2024-05-24
1
-90
/
+92
|
*
|
|
|
runner: Strongly typed Backend enum
Nadrieril
2024-05-24
3
-62
/
+89
|
/
/
/
/
[prev]
[next]