| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-14 | Minor change to x86 specification. | Anthony Fox | |
| 2017-08-10 | Fix bug with subtyping in let bindings | Alasdair Armstrong | |
| 2017-08-10 | Add support for early return to Lem backend | Thomas Bauereiss | |
| Implemented using the exception monad, by throwing and catching the return value | |||
| 2017-08-09 | Pretty-print some more type annotations | Thomas Bauereiss | |
| 2017-08-08 | Fix Lem bindings in test cases | Thomas Bauereiss | |
| Add a test case with the MIPS spec using the TLB stub. Use the sequential monad for Lem testing for now; the free monad (in "prompt.lem") has not been updated for machine words yet. | |||
| 2017-08-08 | Glue together Sail prelude and Lem library | Thomas Bauereiss | |
| 2017-08-08 | Various fixes and improvements for the Lem pretty-printing | Thomas Bauereiss | |
| - Add some missing "wreg" effect annotations in the type checker - Improve pretty-printing of register type definitions: In addition to a "build" function, output an actual type definition, and some getter/setter functions for register fields - Fix a bug in sizeof rewriting that caused it to fail when rewriting nested calls of functions that contained sizeof expressions - Fix pretty-printing of user-defined union types with type variables (cf. test case option_either.sail) - Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to output more type annotations with bitvector lengths - Add (back) some support for specifying Lem bindings in val specs using "val extern ... foo = bar" - Misc bug fixes | |||
| 2017-08-08 | Add x86 decoder. | Anthony Fox | |
| 2017-08-08 | Add add_typ_var to mli file | Alastair Reid | |
| This function is used by asl_to_sail2.ml | |||
| 2017-08-07 | Fixed pretty printing of E_cons | Alasdair Armstrong | |
| 2017-08-07 | Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| sail_new_tc | |||
| 2017-08-07 | Fixed various issues regarding typechecking lists. | Alasdair Armstrong | |
| 2017-08-07 | Merged in acjf3/sail/sail_new_tc (pull request #2) | Anthony Fox | |
| Initial commit of x86 model (ported from L3). | |||
| 2017-08-07 | Initial commit of x86 model (ported from L3). | Anthony Fox | |
| 2017-08-02 | Fix run_tests.sh so it cleans up generated ml files when testing ocaml backend | Alasdair Armstrong | |
| 2017-08-02 | Improve pretty-printing of register declaration and assignment | Thomas Bauereiss | |
| 2017-08-02 | Tune vector_subrange | Thomas Bauereiss | |
| 2017-08-02 | Add debugging option to dump AST after rewriting steps | Thomas Bauereiss | |
| 2017-08-01 | Add missing lexp case to Ocaml pretty-printer | Thomas Bauereiss | |
| 2017-08-01 | Added ocaml generation to run_tests.sh | Alasdair Armstrong | |
| 2017-08-01 | Fixed a bug where type_synonyms were not being expanded properly when ↵ | Alasdair Armstrong | |
| considering possible casts | |||
| 2017-08-01 | Fixed a bug where as patterns weren't binding their variable correctly | Alasdair Armstrong | |
| 2017-08-01 | Added more patterns to ast_util and improved type checking of patterns | Alasdair Armstrong | |
| 2017-08-01 | Remove some hardcoded calls to obsolete Lem library functions | Thomas Bauereiss | |
| 2017-08-01 | Fix some effect propagation bugs in rewriter | Thomas Bauereiss | |
| 2017-07-28 | Add true and false to n_constraint language. Also small tweaks for ASL ↵ | Alasdair Armstrong | |
| generation. | |||
| 2017-07-27 | Rewrite guarded patterns for Lem backend | Thomas Bauereiss | |
| 2017-07-27 | Add cons patterns to pretty-printers | Thomas Bauereiss | |
| 2017-07-27 | Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| sail_new_tc | |||
| 2017-07-27 | Merge branch 'master' into sail_new_tc | Alasdair Armstrong | |
| 2017-07-27 | Some more test cases | Alasdair Armstrong | |
| 2017-07-27 | Parameterise convert_ast by the bitvector order | Alasdair Armstrong | |
| 2017-07-27 | Fixed a bug where sail would run out of file descriptors when passed a large ↵ | Alasdair Armstrong | |
| number of files | |||
| 2017-07-27 | P_cons in monomorphisation | Brian Campbell | |
| 2017-07-27 | Fix up constructor handling in monomorphisation | Brian Campbell | |
| 2017-07-27 | Mirror AST change | Brian Campbell | |
| 2017-07-27 | Add test cases for overlapping record field names | Alasdair Armstrong | |
| 2017-07-27 | Allow local mutable records, and fix bugs with overlapping record field names. | Alasdair Armstrong | |
| 2017-07-27 | Fixed bug with pattern synonyms in Cons and List patterns | Alasdair Armstrong | |
| 2017-07-27 | implement RV64I based on version 2.0 user spec. | Robert Norton | |
| 2017-07-26 | Add right shift to lib/prelude.sail, and add case for E_exit in ↵ | Alasdair Armstrong | |
| Ast_util.string_of_exp | |||
| 2017-07-26 | Allow arbitrary identifiers in nexp expressions | Alasdair Armstrong | |
| Fixed some bugs in the initial check that caused valid code to fail to parse Add a nid utility function that creates an id n-expression, similar to nvar, nconstant etc | |||
| 2017-07-26 | mips_extras.lem: fix references to Interp.V_foo | Jon French | |
| 2017-07-26 | Interpreter doesn't build with new typechecker + changes from master | Alasdair Armstrong | |
| Makes it so that the jenkins buildserver will only try to build sail and not the interpreter for sail_new_tc | |||
| 2017-07-26 | Merge remote-tracking branch 'origin/master' into sail_new_tc | Alasdair Armstrong | |
| 2017-07-26 | Merged in ojno/sail (pull request #1) | Jonathan French | |
| Footprint exhaustive evaluation fixes Approved-by: Jonathan French <me@jonathanfrench.net> | |||
| 2017-07-26 | Improve rewriting of sizeof expressions | Thomas Bauereiss | |
| If some type-level variables in a sizeof expression in a function body cannot be directly extracted from the parameters of the function, add a new parameter for each unresolved parameter, and rewrite calls to the function accordingly | |||
| 2017-07-26 | Merge | Thomas Bauereiss | |
| 2017-07-25 | Fixed bug where strings were not escaped correctly within string | Alasdair Armstrong | |
| literals when pretty printing sail. | |||
| 2017-07-25 | Add instantiation_of helper function to type_check.mli that returns | Alasdair Armstrong | |
| the instantiated type variables in a function application | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |