index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
compiler
/
dune
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2023-10-25
Update following the addition of raw pointers
Son Ho
1
-1
/
+1
2023-10-23
Remove some assumed types and add more support for builtin definitions
Son Ho
1
-1
/
+1
2023-09-07
Map some globals like u32::MAX to standard definitions
Son Ho
1
-0
/
+1
2023-08-31
Start adding support for traits
Son Ho
1
-0
/
+1
2023-08-02
Make progress
Son Ho
1
-2
/
+3
2023-06-04
Initial Lean backend, WIP
Jonathan Protzenko
1
-1
/
+1
2023-02-03
Split InterpreterLoops into several files
Son Ho
1
-0
/
+4
2023-02-03
Implement ReorderDecls.ml
Son Ho
1
-0
/
+1
2023-02-03
Add an SCC.ml file for strongly connected components
Son Ho
1
-1
/
+2
2023-02-03
Start implementing support for loops
Son Ho
1
-1
/
+2
2022-11-14
Make minor modifications
Son Ho
1
-2
/
+0
2022-11-14
Make good progress on the Coq backend
Son Ho
1
-2
/
+4
2022-11-14
Reorganize the project to prepare for new backends
Son Ho
1
-1
/
+1
2022-11-10
Implement a Config.ml file which groups all the global options in references
Son Ho
1
-0
/
+1
2022-10-28
Make minor updates to account for Charon's changes
Son Ho
1
-1
/
+0
2022-10-28
Take care of some TODOs
Son Ho
1
-1
/
+0
2022-10-28
Move some files to the Charon project
Son Ho
1
-7
/
+2
2022-10-27
Reformat the code
Son Ho
1
-10
/
+53
2022-10-27
Move constant_value to PrimitiveValues.ml
Son Ho
1
-1
/
+1
2022-10-27
Rename driver.ml to Driver.ml
Son Ho
1
-1
/
+1
2022-10-27
Reorganize a bit the project
Son Ho
1
-0
/
+0
2022-10-26
Start generating documentation
Son Ho
1
-2
/
+25
2022-09-22
Reformat the project with dune
Son Ho
1
-15
/
+19
2022-05-10
Use the core_unix package instead of core
Son Ho
1
-1
/
+1
2022-03-04
Update the code to create missing directories upon export
Son Ho
1
-1
/
+2
2022-01-06
Cleanup a bit more the dependencies and activate more warnings/errors
Son Ho
1
-2
/
+2
2021-12-15
Parsing of command-line arguments
Jonathan Protzenko
1
-2
/
+2
2021-12-03
Add code to derive polymorphic visitors for g_typed_value and typed_value
Son Ho
1
-0
/
+2
2021-12-03
Make minor modifications
Son Ho
1
-1
/
+1
2021-11-29
Start deriving formatters for debugging
Son Ho
1
-1
/
+2
2021-11-29
Start working logging and make progress on printing ASTs
Son Ho
1
-1
/
+1
2021-11-26
Update the env definition to make the frames easier to manipulate
Son Ho
1
-2
/
+2
2021-11-23
Move some definitions to Contexts.ml and reactivate the warnings
Son Ho
1
-2
/
+2
2021-11-23
Activate exception backtrace
Son Ho
1
-1
/
+15
2021-11-18
Remove the automatic derivation of Yojson (de)serializers
Son Ho
1
-2
/
+1
2021-11-17
Use [@@ëerive of_json] on all the types
Son Ho
1
-1
/
+1
2021-11-17
Start working on json deserialization
Son Ho
1
-1
/
+3
2021-11-02
Setup the project
Son Ho
1
-0
/
+2