summaryrefslogtreecommitdiff
path: root/src/process_file.ml
AgeCommit message (Expand)Author
2017-08-21Modified sizeof rewriting pass so it can correctly deal with existentials.Alasdair Armstrong
2017-08-18Fixed a bug where sizeof re-writing fail for aliased type argumentsAlasdair Armstrong
2017-08-17Add support for register types other than bitvector to state monadThomas Bauereiss
2017-08-10Merge remote-tracking branch 'origin/sail_new_tc' into experimentsAlasdair Armstrong
2017-08-08Add infrastructure to play with new menhir parsers.Alasdair Armstrong
2017-08-02Add debugging option to dump AST after rewriting stepsThomas Bauereiss
2017-07-27Parameterise convert_ast by the bitvector orderAlasdair Armstrong
2017-07-27Fixed a bug where sail would run out of file descriptors when passed a large ...Alasdair Armstrong
2017-07-24Separate monomorphisation from top-level type checkingBrian Campbell
2017-07-24Remove monomorphisation for old type checkerBrian Campbell
2017-07-21Everything moved to new typecheckerAlasdair Armstrong
2017-07-21Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into sa...Alasdair Armstrong
2017-07-21Improvements to sail n_constraintsAlasdair Armstrong
2017-07-21Switch to new typechecker (almost)Thomas Bauereiss
2017-07-13Make new-tc monomorphisation actually workBrian Campbell
2017-07-12Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into sa...Alasdair Armstrong
2017-07-12Removed inital_check_full_astAlasdair Armstrong
2017-07-12Add checks for variable identifiers in pattern subsumptionThomas Bauereiss
2017-07-10Bugfixes and testing new checker on the MIPS specAlasdair Armstrong
2017-06-29Various improvements to typecheckerAlasdair Armstrong
2017-06-22Can now typecheck register declarations and assignmentsAlasdair Armstrong
2017-06-15Prototype Bi-directional type checking algorithm for sailAlasdair Armstrong
2017-02-03fix headersPeter Sewell
2016-12-12cheri sail export progressChristopher Pulte
2016-12-01move interpreter-specific types from Sail_impl_base to Interp_interfaceChristopher Pulte
2016-11-28make sail produce prompt and state version of shallow embedding files at the ...Christopher Pulte
2016-11-27make outcome_s contain the instruction state pretty print rather than the ins...Christopher Pulte
2016-11-14add option -lem_sequential for producing shallow embedding that refers to sta...Christopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-19typeclass instances for converting between shallow and deep embeddingChristopher Pulte
2016-10-18Expose type environment after checking, for use in analysisKathy Gray
2016-10-11move armv8_extras and power_extras to idl/power and idlarm, fixesChristopher Pulte
2016-10-10changed the way registers/register fields work, fixes, nicer names for new le...Christopher Pulte
2016-10-06move type definitions that both interpreter and shallow embedding use to sail...Christopher Pulte
2016-09-07push some lem pp changesChristopher Pulte
2016-06-02improve constraint range checkingKathy Gray
2016-03-02Add new language feature to permit definitions of items of kind Nat, etc as w...Kathy Gray
2016-02-24Small mixups to get the initial check infrastructure working for full ast pro...Kathy Gray
2015-12-21fixes, pp progressChristopher
2015-12-09adapted for Kathy's lexp effect typing changes: register writes should be cor...Christopher
2015-10-28progress on lem backend: auto-generate read_register and write_register funct...Christopher Pulte
2015-10-26add preliminary Sail_values.lem, adapt lem pp to recent Ocaml pp changesChristopher Pulte
2015-10-20Fixing bugs in pretty printer to ocamlKathy Gray
2015-10-06added the preliminary lem output option that for now uses ocaml ppChristopher Pulte
2015-10-06fix generated message to have correct file extensionChristopher Pulte
2015-09-29Boiler plate to generate an ml file from a sail spec. Now debugging the outpu...Kathy Gray
2015-09-28basic untested ocaml boiler plateKathy Gray
2015-06-24Support new memory write events in the sail front end and pretty printerKathy Gray
2015-02-24Fix bug where type parameters weren't pushing down into the body of a functio...Kathy Gray
2015-02-13Actually use new dependency information in generation of lem/etc.Kathy Gray