summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-11-21Coq: add equality for records and polymorphic vectorsBrian Campbell
2018-11-21Escape string literals in coq backend. Note that 71020c2f460e6031776df17cf8f2...Robert Norton
2018-11-21Escape strings literals in lem pretty printer.Robert Norton
2018-11-20Add messages for assert failures without user defined messagesAlasdair Armstrong
2018-11-19Fix Lem untupling to correctly identify when multiple arguments are usedBrian Campbell
2018-11-19Don't re-check AST repeatedly in exp_lift_assign re-writeAlasdair Armstrong
2018-11-19Ensure sizeof re-writing occurs for configuration registersAlasdair Armstrong
2018-11-19Merge branch 'latex' into sail2Robert Norton
2018-11-16Canonicalise functions types in val specsAlasdair Armstrong
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-11-15When outputing latex do not expand type synonyms in val specs during type check.Robert Norton
2018-11-15Add simple valspec printing in latex that drops effects and other extraneous ...Robert Norton
2018-11-15ast_utils: simplify numeric constraints in inequalities.Robert Norton
2018-11-14Use code style For [id] refs in doc comments.Robert Norton
2018-11-14latex: use callback macro saildocxxx (one per top-level category) to give use...Robert Norton
2018-11-13Make pretty printer stricter with brace placementAlasdair Armstrong
2018-11-12Infer tuple l-expressions types if all components are inferrableAlasdair Armstrong
2018-11-12Make type checker smarter at inferring l-expressionsAlasdair Armstrong
2018-11-12Add referencing commands to generated latexAlasdair Armstrong
2018-11-12Fix numbers in constructor argumentsAlasdair Armstrong
2018-11-12Improve latex naming scheme and avoid collisionsAlasdair Armstrong
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-11-07Move inline forall in function definitionsAlasdair Armstrong
2018-11-07Move inline forall in function definitionsAlasdair Armstrong
2018-11-06Fix bug with loop indices not being mapped to int64 in CAlasdair Armstrong
2018-11-05Ensure function quantifier is in scope when generating C return typeAlasdair Armstrong
2018-11-05Ensure type-synonyms are handled correctly in register dependenciesAlasdair Armstrong
2018-11-05Make sure undefined_type functions are generated before registersAlasdair Armstrong
2018-11-02Add code to analyse function return typesAlasdair Armstrong
2018-11-02Coq: add more autocasts for different but equal kidsBrian Campbell
2018-11-01Changes to enable analysing type errors in ASL parserAlasdair Armstrong
2018-10-31Add rewriting pass for not-patternsAlasdair Armstrong
2018-10-31Remove Parse_ast.Int, add unique locationsAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-10-31Improve error messages for unsolved function quantifiersAlasdair Armstrong
2018-10-29Pretty printer tweaks for ASL parserAlasdair Armstrong
2018-10-24Add constraint synonymsAlasdair Armstrong
2018-10-22Coq: use function type more carefully in untuplingBrian Campbell
2018-10-22Coq: work around constructors with tupled argumentsBrian Campbell
2018-10-22Fix lem arguments for functions with tuple argumentsAlasdair Armstrong
2018-10-22Pretty_print_lem.untuple_args_pat: temporary hack to allow functions that act...Jon French
2018-10-16Re-implement space-related mapping functions in Sail rather than backendsJon French
2018-10-16rewrites: remove now-unnecessary temporary string hack from rewrite_defs_pat_...Jon French
2018-10-11Change the function type in the ASTAlasdair
2018-10-10refer to Util.list_init.ml rather than List.init in sail_lib.mlChristopher Pulte
2018-10-08Produce lists of constructors and ast building functions for test generationBrian Campbell
2018-10-05interpreter: Remove boxes (no longer used)Jon French
2018-10-05fix bug in infer_mpat losing types of identifiers inferred from other_envJon French
2018-10-04Merge branch 'ocaml-instruction-generation' into sail2Brian Campbell
2018-10-04Bit of commentary, proper TODO errorBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:41:46 +0000