Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Remove the type sv_kind ("symbolic value kind") | Son Ho | 2023-12-05 | 8 | -158/+63 |
| | |||||
* | Merge pull request #48 from AeneasVerif/son_closures | Son HO | 2023-12-05 | 37 | -891/+1315 |
|\ | | | | | Prepare support for function pointers and closures | ||||
| * | Update the flake.lock | Son Ho | 2023-12-05 | 1 | -36/+36 |
| | | |||||
| * | Print error messages when the command line arguments are invalid | Son Ho | 2023-12-05 | 1 | -10/+40 |
| | | |||||
| * | Fix a minor issue with the use of const generics | Son Ho | 2023-12-05 | 6 | -13/+40 |
| | | |||||
| * | Update following changes in Charon | Son Ho | 2023-12-05 | 32 | -826/+1176 |
| | | |||||
| * | Update the code following changes in the NameMatcher | Son Ho | 2023-11-29 | 4 | -6/+23 |
|/ | |||||
* | Merge pull request #39 from AeneasVerif/afromher_shifts | Son HO | 2023-11-29 | 26 | -95/+2000 |
|\ | | | | | Add support for bitshifts | ||||
| * | Update the flake.lock | Son Ho | 2023-11-29 | 1 | -9/+9 |
| | | |||||
| * | Regenerate the other files | Son Ho | 2023-11-29 | 14 | -56/+1570 |
| | | |||||
| * | Generate the Bitwise test files | Son Ho | 2023-11-29 | 3 | -0/+107 |
| | | |||||
| * | Fix a minor issue with the extraction | Son Ho | 2023-11-29 | 1 | -4/+5 |
| | | |||||
| * | Add support for more bitwise operations and update the extraction | Son Ho | 2023-11-29 | 6 | -28/+302 |
| | | |||||
| * | Merge branch 'main' into afromher_shifts | Son Ho | 2023-11-29 | 228 | -20545/+34347 |
| |\ | |/ |/| | |||||
* | | Merge pull request #47 from AeneasVerif/son_panics | Son HO | 2023-11-29 | 8 | -134/+155 |
|\ \ | | | | | | | Update following some changes in Charon | ||||
| * | | Update flake.lock | Son Ho | 2023-11-29 | 1 | -30/+30 |
| | | | |||||
| * | | Regenerate the tests | Son Ho | 2023-11-29 | 4 | -89/+125 |
| | | | |||||
| * | | Regenerate the test files | Son Ho | 2023-11-29 | 3 | -15/+0 |
|/ / | |||||
* | | Merge pull request #46 from AeneasVerif/son_improves | Son HO | 2023-11-28 | 94 | -521/+917 |
|\ \ | | | | | | | Minor improvements for the extraction | ||||
| * | | Update the flake.lock | Son Ho | 2023-11-27 | 1 | -18/+18 |
| | | | |||||
| * | | Fix the issues with the cross-references for OCaml doc | Son Ho | 2023-11-27 | 16 | -35/+35 |
| | | | |||||
| * | | Update a comment | Son Ho | 2023-11-27 | 1 | -1/+2 |
| | | | |||||
| * | | Update the way the Primitives file is copied | Son Ho | 2023-11-27 | 1 | -13/+20 |
| | | | |||||
| * | | Do not activate the sanity (invariant) checks by default | Son Ho | 2023-11-27 | 8 | -19/+16 |
| | | | |||||
| * | | Generate a dedicated file for the external types | Son Ho | 2023-11-27 | 46 | -90/+355 |
| | | | |||||
| * | | Update the generation of files for external definitions and regenerate the tests | Son Ho | 2023-11-27 | 21 | -33/+158 |
| | | | |||||
| * | | Regenerate the files | Son Ho | 2023-11-24 | 12 | -282/+259 |
| | | | |||||
| * | | Add the alloc::string::String type in the builtins | Son Ho | 2023-11-24 | 3 | -5/+16 |
| | | | |||||
| * | | Update a comment | Son Ho | 2023-11-24 | 1 | -2/+3 |
| | | | |||||
| * | | Make a minor fix | Son Ho | 2023-11-24 | 1 | -1/+1 |
| | | | |||||
| * | | Update some assumed type names/variants | Son Ho | 2023-11-24 | 2 | -34/+41 |
| | | | |||||
| * | | Improve the error messages for some name collisions | Son Ho | 2023-11-24 | 1 | -2/+4 |
| | | | |||||
| * | | Make a minor update in ExtractName.pattern_to_extract_name | Son Ho | 2023-11-24 | 1 | -1/+4 |
|/ / | |||||
* | | Merge pull request #45 from AeneasVerif/son_merge_types | Son HO | 2023-11-22 | 153 | -11476/+12488 |
|\ \ | | | | | | | Big cleanup | ||||
| * | | Update the flake.lock | Son Ho | 2023-11-22 | 1 | -3/+2 |
| | | | |||||
| * | | Fix an issue with the nix flake and update the flake.lock | Son Ho | 2023-11-22 | 3 | -32/+18 |
| | | | |||||
| * | | Update the flake.lock | Son Ho | 2023-11-22 | 1 | -18/+18 |
| | | | |||||
| * | | Cleanup a bit | Son Ho | 2023-11-22 | 1 | -87/+0 |
| | | | |||||
| * | | Make a minor modification | Son Ho | 2023-11-22 | 1 | -2/+3 |
| | | | |||||
| * | | Use NameMatcher.NameMatcherMap instead of associative lists | Son Ho | 2023-11-22 | 2 | -18/+22 |
| | | | |||||
| * | | Regenerate the test files | Son Ho | 2023-11-22 | 3 | -131/+186 |
| | | | |||||
| * | | Improve further the generation of parent clause/trait clause names | Son Ho | 2023-11-22 | 8 | -48/+177 |
| | | | |||||
| * | | Regenerate the files | Son Ho | 2023-11-21 | 3 | -61/+71 |
| | | | |||||
| * | | Improve the generation of parent clause names | Son Ho | 2023-11-21 | 3 | -11/+45 |
| | | | |||||
| * | | Update the generation of names for the parent trait clauses | Son Ho | 2023-11-21 | 1 | -4/+29 |
| | | | |||||
| * | | Reorganize the "Extract" files | Son Ho | 2023-11-21 | 7 | -1439/+1299 |
| | | | |||||
| * | | Regenerate the files | Son Ho | 2023-11-21 | 65 | -1578/+3156 |
| | | | |||||
| * | | Make minor updates to the extraction of spans | Son Ho | 2023-11-21 | 1 | -4/+5 |
| | | | |||||
| * | | Add span information to the generated code | Son Ho | 2023-11-21 | 12 | -45/+91 |
| | | | |||||
| * | | Add an `is_local` field to declarations | Son Ho | 2023-11-21 | 5 | -3/+16 |
| | | |