summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Also fix implementation of Join-SharedBorrowAymeric Fromherz2024-05-311-3/+3
|
* destructure_abs can be called during collapse: markers should be allowedAymeric Fromherz2024-05-301-4/+0
|
* Correct implementation of Join-MutBorrows: add markers when creating a new ↵Aymeric Fromherz2024-05-301-3/+4
| | | | abstraction
* More lisible sign for proj_right pretty-printingAymeric Fromherz2024-05-301-1/+1
|
* Implement two phases of loops join + collapseAymeric Fromherz2024-05-3023-2971/+660
|
* Compute marker information for borrow/loan mapsAymeric Fromherz2024-05-283-50/+73
|
* Add type and set/map for marker and borrow idAymeric Fromherz2024-05-284-10/+22
|
* Simplify collapse_ctxAymeric Fromherz2024-05-271-6/+5
|
* Simplify reduce_ctxAymeric Fromherz2024-05-271-21/+6
|
* Split collapse into collapse and reduce, rename accordinglyAymeric Fromherz2024-05-274-13/+185
|
* Add projection markers when joining environmentsAymeric Fromherz2024-05-271-0/+59
|
* Add markers everywhere, do not use them yetAymeric Fromherz2024-05-2710-139/+302
|
* Start adding markersSon Ho2024-05-246-50/+94
|
* Downgrade the version of duneSon Ho2024-05-241-1/+1
|
* Merge pull request #202 from AeneasVerif/afromher_debugAymeric Fromherz2024-05-241-1/+16
|\ | | | | Expand debug output in loops fixed points
| * Merge remote-tracking branch 'origin/main' into afromher_debugAymeric Fromherz2024-05-2491-3550/+5686
| |\ | |/ |/|
* | Merge pull request #197 from AeneasVerif/test-harness3Guillaume Boisseau2024-05-2491-3550/+5686
|\ \
| * | 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
|/ /
| * Expand debug output in loops fixed pointsAymeric Fromherz2024-05-241-1/+16
|/
* 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
|/
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 12:02:25 +0000