| Commit message (Expand) | Author | Files | Lines |
2023-11-29 | Update the code following changes in the NameMatcher | Son Ho | 1 | -0/+2 |
2023-11-20 | Use the name matcher implemented in Charon | Son Ho | 1 | -2/+8 |
2023-11-16 | Finish propagating the changes to the names and cleaning | Son Ho | 1 | -2/+2 |
2023-11-15 | Do more cleanup | Son Ho | 1 | -3/+3 |
2023-11-15 | Start updating the name type, cleanup the names and the module abbrevs | Son Ho | 1 | -4/+4 |
2023-11-12 | Remove the 'r type variable from the ty type definition | Son Ho | 1 | -2/+2 |
2023-11-09 | Make the traits work for Coq | Son Ho | 1 | -3/+4 |
2023-10-26 | Fix some issues and regenerate the HashmapMain example for Lean | Son Ho | 1 | -5/+6 |
2023-10-26 | Improve the handling of saved function effects in ExtractBuiltin.ml | Son Ho | 1 | -11/+17 |
2023-10-24 | Handle properly the builtin, non fallible functions | Son Ho | 1 | -15/+19 |
2023-10-23 | Remove some assumed types and add more support for builtin definitions | Son Ho | 1 | -1/+1 |
2023-10-22 | Add more support for numeric operations, xor, rotate | Jonathan Protzenko | 1 | -3/+21 |
2023-10-20 | Start updating to handle function pointers | Son Ho | 1 | -1/+1 |
2023-08-31 | Start adding support for traits | Son Ho | 1 | -5/+10 |
2022-11-16 | Do not introduce match on the fuel for non-recursive functions | Son Ho | 1 | -7/+22 |
2022-11-14 | Make [Result::Failure] type an [Error] parameter | Son Ho | 1 | -1/+1 |
2022-11-10 | Implement the generation of stateful backward functions (controlled by an opt... | Son Ho | 1 | -1/+1 |
2022-10-28 | Move the AssignGlobal case from statement to rvalue | Son Ho | 1 | -1/+1 |
2022-10-28 | Make minor updates to account for Charon's changes | Son Ho | 1 | -2/+1 |
2022-10-27 | Reformat the code | Son Ho | 1 | -5/+5 |
2022-10-27 | Reorganize a bit the project | Son Ho | 1 | -0/+0 |
2022-10-13 | Rename Modules to Crates | Son Ho | 1 | -2/+2 |
2022-09-22 | Make minor cleanup | Son Ho | 1 | -5/+5 |
2022-09-22 | Update FunsAnalysis | Son Ho | 1 | -24/+26 |
2022-09-22 | Update src/FunsAnalysis.ml | Son HO | 1 | -0/+1 |
2022-09-22 | Update src/FunsAnalysis.ml | Son HO | 1 | -1/+1 |
2022-08-11 | Correct assertion for stateless globals | Sidney Congard | 1 | -1/+1 |
2022-07-29 | Create global declaration group, address PR changes but introduce bugs | Sidney Congard | 1 | -3/+10 |
2022-07-28 | Always put can_fail to true, specialize global traduction to concrete functio... | Sidney Congard | 1 | -0/+2 |
2022-07-25 | Apply minor changes from PR comments | Sidney Congard | 1 | -8/+1 |
2022-07-18 | Address much stuff of the PR, throw exceptions at remaining places | Sidney Congard | 1 | -3/+3 |
2022-07-13 | Apply small changes from the PR | Sidney Congard | 1 | -0/+3 |
2022-07-05 | Remove last prints, adapt JSON | Sidney Congard | 1 | -3/+0 |
2022-06-30 | Traduct globals body separately (WIP) | Sidney Congard | 1 | -34/+43 |
2022-06-30 | Take failing rvalues into account in FunsAnalysis.analyze_fun_decls | Son Ho | 1 | -0/+8 |
2022-06-21 | concrete & symbolic evaluation work with new LLBC format | Sidney Congard | 1 | -1/+0 |
2022-06-08 | read globals from LLBC JSON into functions | Sidney Congard | 1 | -0/+1 |
2022-05-06 | Add comments in FunsAnalysis | Son Ho | 1 | -2/+8 |
2022-05-04 | Start implementing divergence, can_fail, statefullness analyses | Son Ho | 1 | -0/+111 |