summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* runner: Use full path and use an enum for crate vs fileNadrieril2024-05-242-43/+55
|
* runner: Do both steps of generation at onceNadrieril2024-05-242-24/+25
|
* Auto-detect test casesNadrieril2024-05-244-33/+39
|
* Use runner to generate llbcNadrieril2024-05-243-84/+126
|
* Tweak a pathNadrieril2024-05-2452-1221/+1220
|
* Import test suite from charonNadrieril2024-05-2427-56/+4148
|
* Remove secondary betree testNadrieril2024-05-2410-2101/+4
| | | | | Opened https://github.com/AeneasVerif/aeneas/issues/196 to remember to add a more adequate replacement test.
* Let the runner choose which backends to useNadrieril2024-05-242-43/+28
|
* Cleanup test runnerNadrieril2024-05-241-99/+124
|
* Set all options in the test runnerNadrieril2024-05-242-51/+58
|
* Move the subdirectory selection to the test runnerNadrieril2024-05-242-56/+28
|
* Add simple test runnerNadrieril2024-05-248-6/+110
|
* Regroup and sort makefile test entriesNadrieril2024-05-241-95/+85
|
* make: deduplicate setting the backendNadrieril2024-05-241-13/+7
|
* Format `flake.nix`Nadrieril2024-05-241-35/+39
|
* Merge pull request #175 from AeneasVerif/afromher/metaSon HO2024-05-2453-2958/+2962
|\ | | | | Rename meta into span
| * update charon pinAymeric Fromherz2024-05-242-4/+4
| |
| * update charon pinAymeric Fromherz2024-05-242-4/+4
| |
| * Rename meta into spanAymeric Fromherz2024-05-2451-2939/+2943
| |
| * Rename span into raw_spanAymeric Fromherz2024-05-244-20/+20
|/
* Merge pull request #200 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-244-6/+7
|\
| * Update charon pinNadrieril2024-05-244-6/+7
|/
* Merge pull request #199 from AeneasVerif/son/errorsSon HO2024-05-242-17/+29
|\ | | | | Print name patterns when ignoring definitions
| * Fix a crash which happens when type definitions are ignoredSon Ho2024-05-241-2/+5
| |
| * Print the name patterns of the definitions which fail to extractSon Ho2024-05-242-15/+24
|/
* Merge pull request #198 from AeneasVerif/son/omegaSon HO2024-05-244-104/+82
|\ | | | | Update scalar_tac to use omega instead of linarith
| * Update scalar_tac to use omega instead of linarithSon Ho2024-05-244-104/+82
|/
* Update the interpreter so that it is not written in CPS style (#120)Escherichia2024-05-2319-2294/+2116
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Start turning the compiler in a style which is less CPS * Update a function in InterpreterExpressions.ml * WIP work on cps * WIP * WIP, currently on InterpreterStatements.ml * WIP * Finished CPS-related modification * Fixed some warning related to documentation comments * Finished loop support, fixed a loop * fixed a typed value * Fixed check_disappeared related error * cleaned check_disappeared related error * Start cleaning up * Do more cleanup * Make some cleanup and fix an issue * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Rename a function * Do more cleanup * Cleanup the loops code and fix some bugs * Cleanup assign_to_place * Make a minor cleanup --------- Co-authored-by: Son Ho <hosonmarc@gmail.com>
* Merge pull request #192 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-2317-25/+25
|\
| * Bump charon versionNadrieril2024-05-2317-25/+25
|/
* Merge pull request #189 from AeneasVerif/son/progressSon HO2024-05-211-0/+13
|\ | | | | Fix an issue in the progress tactic
| * Fix an issue in the progress tacticSon Ho2024-05-211-0/+13
|/
* Merge pull request #183 from RaitoBezarius/coercionsSon HO2024-05-211-0/+12
|\ | | | | feat(backends/lean): make `max`-related coercions nicer
| * Merge branch 'main' into coercionsSon HO2024-05-212-3/+3
| |\ | |/ |/|
* | Merge pull request #187 from AeneasVerif/son/readmeSon HO2024-05-171-2/+2
|\ \ | | | | | | Update the README
| * | Update the READMESon Ho2024-05-171-2/+2
|/ /
* | Merge pull request #186 from AeneasVerif/fix-makeGuillaume Boisseau2024-05-151-1/+1
|\ \
| * | Makefile: `make check-charon` should not try to recreate the commit pin`Nadrieril2024-05-151-1/+1
|/ /
| * feat(backends/lean): make `max`-related coercions nicerRyan Lahfa2024-05-211-0/+12
|/ | | | | | | | | | Situations where you have `coe (max a b) = max (coe a) (coe b)` are often stuck during verification because of the lack of this theorem. With this theorem, `push_cast` works as intended and normalizes even further. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* Merge pull request #172 from AeneasVerif/string-literalsGuillaume Boisseau2024-05-144-4/+10
|\
| * Catch new literal variantsNadrieril2024-05-144-4/+10
|/
* Merge pull request #180 from AeneasVerif/ciGuillaume Boisseau2024-05-141-0/+1
|\ | | | | ci: cancel jobs after force-push to a branch
| * ci: cancel jobs after force-push to a branchNadrieril2024-05-141-0/+1
|/
* Merge pull request #169 from AeneasVerif/charon-pinGuillaume Boisseau2024-05-1410-26/+146
|\
| * Tweak wordingGuillaume Boisseau2024-05-141-3/+3
| | | | | | | | Co-authored-by: Son HO <hosonmarc@gmail.com>
| * Ensure `./charon` points to a valid charon cloneNadrieril2024-05-146-20/+103
| |
| * `./charon-pin` stores the current charon commitNadrieril2024-05-145-4/+41
|/ | | | It is kept up-to-date in CI
* Merge pull request #164 from RaitoBezarius/ofnat_scalarSon HO2024-05-141-0/+5
|\ | | | | | | feat(backend/lean): Raw Lean literals can be parsed into scalars automatically
| * feat(backend/lean): Raw Lean literals can be parsed into scalars automaticallyRyan Lahfa2024-04-301-0/+5
| | | | | | | | | | | | | | We can use coercion to go to integers, build a scalar out of an int via unification and let the user clear up bounds or let Lean decide them. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* | Merge pull request #177 from RaitoBezarius/oops-soundness-i-am-sowwySon HO2024-05-141-1/+4
|\ \ | | | | | | backends/lean: repair definitions of `core.mem.replace`
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 09:50:15 +0000