summaryrefslogtreecommitdiff
path: root/src (unfollow)
Commit message (Expand)AuthorFilesLines
2022-09-22Update src/ExtractToFStar.mlSon HO1-1/+1
2022-09-22Update src/ExtractToFStar.mlSon HO1-1/+1
2022-09-22Update src/ExtractToFStar.mlSon HO1-1/+1
2022-09-22Update src/ExtractToFStar.mlSon HO1-1/+1
2022-09-22Update src/ExtractToFStar.mlSon HO1-1/+1
2022-09-22Update src/ExtractToFStar.mlSon HO1-1/+1
2022-09-22Update src/SymbolicAst.mlSon HO1-1/+1
2022-09-22Update src/TypesUtils.mlSon HO1-1/+1
2022-09-22Update src/Translate.mlSon HO1-1/+1
2022-08-11Correct last PR remarksSidney Congard2-23/+17
2022-08-11Correct assertion for stateless globalsSidney Congard1-1/+1
2022-08-10Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard8-24/+31
2022-08-08Register global names, one error remainingSidney Congard4-4/+23
2022-07-29Create global declaration group, address PR changes but introduce bugsSidney Congard10-83/+134
2022-07-28Always put can_fail to true, specialize global traduction to concrete functio...Sidney Congard2-9/+18
2022-07-25Apply minor changes from PR commentsSidney Congard5-17/+23
2022-07-18Address much stuff of the PR, throw exceptions at remaining placesSidney Congard16-112/+172
2022-07-13Apply small changes from the PRSidney Congard4-9/+12
2022-07-05Remove last prints, adapt JSONSidney Congard2-6/+3
2022-06-30Traduct globals body separately (WIP)Sidney Congard11-66/+208
2022-06-30Take failing rvalues into account in FunsAnalysis.analyze_fun_declsSon Ho4-19/+22
2022-06-29Make minor modificationsSon Ho4-6/+46
2022-06-27Add `can_end` in `abs` and use it for the return abs when generating theSon Ho5-33/+59
2022-06-27Update eval_operand_prepare to not give a value to the continuationSon Ho4-109/+181
2022-06-23adapt to new LLBC (without OperandConstantValue)Sidney Congard2-33/+27
2022-06-21concrete & symbolic evaluation work with new LLBC formatSidney Congard22-307/+260
2022-06-13crude generation working - missing unit tests & special constants handlingSidney Congard5-52/+70
2022-06-08read globals from LLBC JSON into functionsSidney Congard20-80/+161
2022-05-16Fix an issue when extracting assumed valuesSon Ho1-1/+1
2022-05-15Add a pass to cleanup the deconstructed ADTs and fix a small issueSon Ho3-12/+112
2022-05-15Treat integer casts in a general mannerSon Ho9-50/+75
2022-05-15Add AggregatedOptionSon Ho5-8/+37
2022-05-10Make minor modificationsSon Ho3-8/+10
2022-05-10Use the core_unix package instead of coreSon Ho2-2/+2
2022-05-06Update the extraction to set the fuel to 1 in the Z3 optionsSon Ho1-2/+2
2022-05-06Don't use the Rust disambiguators when generating names at extractionSon Ho2-3/+12
2022-05-06Add an option to eagerly end abstractions if a function has return typeSon Ho4-2/+61
2022-05-06Factorize some code in InterpreterBorrows*Son Ho2-49/+77
2022-05-06Add comments in FunsAnalysisSon Ho1-2/+8
2022-05-05Make minor fixesSon Ho3-4/+28
2022-05-05Update the translation so that we use a state only in the functionsSon Ho2-35/+42
2022-05-04Start implementing divergence, can_fail, statefullness analysesSon Ho5-36/+135
2022-05-04Make minor modificationsSon Ho5-29/+24
2022-05-04Make minor modificationsSon Ho4-35/+28
2022-05-04Fix various issues when using a stateSon Ho2-30/+12
2022-05-04Fix more issuesSon Ho2-32/+12
2022-05-04Fix some issues when using statesSon Ho3-72/+84
2022-05-04Make progress updating the codeSon Ho5-194/+76
2022-05-04Start updating the way the function return type (with errors and states)Son Ho4-182/+278
2022-05-01Move the type-checking functions for pure AST to PureTypeCheck.mlSon Ho3-149/+179
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 21:34:31 +0000