summaryrefslogtreecommitdiff
path: root/compiler/InterpreterStatements.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-04Propagated changes to statement from Charon (#223)Escherichia1-0/+1
2024-06-03Fix a bug when composing the continuations in eval_statementSon Ho1-113/+108
2024-06-03feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209Lucas Franceschino1-0/+1
2024-05-30Remove the cps.eval_result typeSon Ho1-2/+6
2024-05-30Remove the options from the functions synthesizing the symbolic ASTSon Ho1-34/+10
2024-05-24Rename meta into spanAymeric Fromherz1-215/+215
2024-05-23Update the interpreter so that it is not written in CPS style (#120)Escherichia1-635/+645
2024-04-22Reformat some filesSon Ho1-5/+5
2024-04-18item_metaNadrieril1-6/+6
2024-04-07Improve the error messages furtherSon Ho1-1/+12
2024-03-29Add some missing error messagesSon Ho1-2/+2
2024-03-29formatting and changed save_error condition for failing from b to not bEscherichia1-5/+13
2024-03-29added file and line arg to craise and cassertEscherichia1-53/+53
2024-03-28formattingEscherichia1-88/+133
2024-03-28Should answer all comments, there are still some TODO: error message leftEscherichia1-32/+32
2024-03-28Added sanity_check and sanity_check_opt_meta helpers and changed sanity check...Escherichia1-8/+7
2024-03-28added a meta option field to norm_ctx and changed the meta used by some asser...Escherichia1-1/+1
2024-03-28Inverted meta and config argument orders (from meta -> config to config -> meta)Escherichia1-77/+77
2024-03-28Still need to fill the TODO: error message and check some meta but it buildsEscherichia1-1/+1
2024-03-28WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...Escherichia1-91/+91
2024-03-28WIP: does not compile yet because we need to propagate the meta variable.Escherichia1-23/+23
2024-03-28WIP Beginning working on better errors: began replacing raise (Failure) and a...Escherichia1-132/+134
2024-03-20Improve the generation of pretty name and the micro passesSon Ho1-1/+3
2024-03-18Make good progress on adding generics to global constantsSon Ho1-13/+19
2024-03-17Make minor updatesSon Ho1-7/+8
2024-03-17Fix a small issue ollowing updates in CharonSon Ho1-3/+8
2024-03-08Add logging informationSon Ho1-0/+7
2023-12-22Fix an issue when merging the fwd/back functions of trait methodsSon Ho1-9/+24
2023-12-21Make good progress on merging the fwd/back functionsSon Ho1-17/+30
2023-12-18Rename some definitionsSon Ho1-6/+6
2023-12-13Update the interpreter to handle optional otherwise branchesSon Ho1-1/+4
2023-12-05Remove the type sv_kind ("symbolic value kind")Son Ho1-2/+2
2023-12-05Update following changes in CharonSon Ho1-383/+413
2023-11-21Add span information to the generated codeSon Ho1-1/+1
2023-11-21Rename PrimitiveValues to ValuesSon Ho1-1/+0
2023-11-15Start updating the name type, cleanup the names and the module abbrevsSon Ho1-226/+212
2023-11-13Make minor modificationsSon Ho1-3/+27
2023-11-13Add RegionsHierarchy.mlSon Ho1-1/+1
2023-11-12Add the "V" prefix to most variants related to valuesSon Ho1-19/+19
2023-11-12Prefix variants related to types with "T"Son Ho1-4/+4
2023-11-12Remove the 'r type variable from the ty type definitionSon Ho1-64/+54
2023-10-24Add some debugging informationSon Ho1-0/+7
2023-10-23Remove some assumed types and add more support for builtin definitionsSon Ho1-94/+6
2023-10-20Start updating to handle function pointersSon Ho1-34/+44
2023-10-13Add supSon Ho1-1/+1
2023-09-19Cleanup a bitSon Ho1-10/+10
2023-09-17Normalize the function signatures before translation to pureSon Ho1-61/+0
2023-09-17Make progress on correctly extracting trait method callsSon Ho1-13/+20
2023-09-17Update the handling of calls to trait impl methodsSon Ho1-8/+67
2023-09-17Fix a minor issueSon Ho1-2/+2