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
*
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
|
/
/
/
*
|
|
Merge pull request #203 from AeneasVerif/son/dune
Son HO
2024-05-24
1
-1
/
+1
|
\
\
\
|
*
|
|
Downgrade the version of dune
Son Ho
2024-05-24
1
-1
/
+1
*
|
|
|
Merge pull request #202 from AeneasVerif/afromher_debug
Aymeric Fromherz
2024-05-24
1
-1
/
+16
|
\
\
\
\
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Merge remote-tracking branch 'origin/main' into afromher_debug
Aymeric Fromherz
2024-05-24
91
-3550
/
+5686
|
|
\
\
\
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Expand debug output in loops fixed points
Aymeric Fromherz
2024-05-24
1
-1
/
+16
|
|
*
|
Regenerate Lean files for betree
Aymeric Fromherz
2024-05-23
1
-0
/
+4
|
|
*
|
Add simp, reducible attributes to generated Lean projectors
Aymeric Fromherz
2024-05-23
1
-0
/
+10
|
|
*
|
Regenerate Lean files for betree following extraction changes
Aymeric Fromherz
2024-05-23
2
-47
/
+46
|
|
*
|
Do not expand field projector for recursive structs to a let binding in Lean
Aymeric Fromherz
2024-05-23
1
-5
/
+0
|
|
*
|
Improve formatting of Lean struct projectors
Aymeric Fromherz
2024-05-23
1
-2
/
+6
|
|
*
|
Add printing of projectors for recursive structs in Lean backend
Aymeric Fromherz
2024-05-23
1
-3
/
+130
|
|
|
*
feat: add small pieces of max theory
Ryan Lahfa
2024-05-24
1
-0
/
+39
|
|
_
|
/
|
/
|
|
*
|
|
Merge pull request #197 from AeneasVerif/test-harness3
Guillaume Boisseau
2024-05-24
91
-3550
/
+5686
|
\
\
\
|
|
/
/
|
/
|
|
|
*
|
runner: Use full path and use an enum for crate vs file
Nadrieril
2024-05-24
2
-43
/
+55
|
*
|
runner: Do both steps of generation at once
Nadrieril
2024-05-24
2
-24
/
+25
|
*
|
Auto-detect test cases
Nadrieril
2024-05-24
4
-33
/
+39
|
*
|
Use runner to generate llbc
Nadrieril
2024-05-24
3
-84
/
+126
|
*
|
Tweak a path
Nadrieril
2024-05-24
52
-1221
/
+1220
|
*
|
Import test suite from charon
Nadrieril
2024-05-24
27
-56
/
+4148
|
*
|
Remove secondary betree test
Nadrieril
2024-05-24
10
-2101
/
+4
|
*
|
Let the runner choose which backends to use
Nadrieril
2024-05-24
2
-43
/
+28
|
*
|
Cleanup test runner
Nadrieril
2024-05-24
1
-99
/
+124
|
*
|
Set all options in the test runner
Nadrieril
2024-05-24
2
-51
/
+58
|
*
|
Move the subdirectory selection to the test runner
Nadrieril
2024-05-24
2
-56
/
+28
|
*
|
Add simple test runner
Nadrieril
2024-05-24
8
-6
/
+110
[next]