summaryrefslogtreecommitdiff
path: root/src/type_check.ml
AgeCommit message (Expand)Author
2021-02-17Check if an unbound identifier is bound as a function identifierAlasdair
2021-01-05Don't allow type synonyms with the same name as existing typesAlasdair
2020-09-29Refactor: Change AST type from a union to a structAlasdair
2020-09-28Refactor: Rename 'a defs to 'a astAlasdair
2020-09-28Move the ast defs wrapper into it's own fileAlasdair
2020-09-23Allow more access to parts of Env (needed by minisail)Mark Wassell
2020-08-10Fix a C backend bug with letbindings in guards shadowing body definitionsAlasdair
2020-08-06Fix for last commitAlasdair
2020-08-06Forbid duplicate top-level letbindingsAlasdair
2020-07-15Prevent creation of variant with existing type id and constructors that exist...Mark Wassell
2020-06-23Fix bug with duplicate enum identifiers in patternsAlasdair
2020-06-18Report locations for "default order" errorsBrian Campbell
2020-06-17Make `if cond { ... return() };` assert cond in the type environmentBrian Campbell
2020-06-05Generate nice error messages for patterns woth duplicate bindingsAlasdair
2020-05-21Merge branch 'sail2' into mono-tweaksAlasdair
2020-05-15Add coverage tracking toolAlasdair
2020-04-10Make bounds check for vector subrange assignments stricterThomas Bauereiss
2020-04-10Be more careful when flow-typing loopsThomas Bauereiss
2020-03-19Improve a particularly unhelpful type errorAlasdair
2020-03-18Expose details of failed lexp bounds checksThomas Bauereiss
2020-02-21Make sure we test that struct literals have a complete set of fields. Fixes #60Alasdair Armstrong
2020-01-31Fix soundness bug found by MarkAlasdair
2020-01-16Allow effects on mappingsAlasdair Armstrong
2020-01-16Cleanup type-checking rule for LEXP_fieldAlasdair Armstrong
2019-12-10Introduce new bitfield syntax for ASL translationAlasdair Armstrong
2019-11-05Forbid types declared after a scattered union being used in clausesAlasdair
2019-11-05Improve type error for recursive types slightlyAlasdair Armstrong
2019-11-05Make sure we correctly forbid recursive datatypes that we don't want to supportAlasdair Armstrong
2019-11-01Add a missing well-formedness checkAlasdair
2019-08-05Remove escape/pure effect restriction for mappingAlasdair Armstrong
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-06-28Add a warning for potentially unsafe castsAlasdair
2019-06-26Fix: Make sure to consider NC_app when checking constraints are identicalAlasdair Armstrong
2019-06-26Make sure we take constraint synonyms into account when checking if types are...Alasdair Armstrong
2019-06-13Add AST for greater-than and less-than constraintsBrian Campbell
2019-06-10Add well-formedness check for type schemes in valspecs.Brian Campbell
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
2019-05-20Revert "Add constraints to undefined vector functions to ensure that lengths ...Brian Campbell
2019-05-19Add constraints to undefined vector functions to ensure that lengths areBrian Campbell
2019-05-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-05-07Merge branch 'sail2' into smt_experimentsAlasdair Armstrong
2019-05-07Merge branch 'sc_fix' into sail2Alasdair Armstrong
2019-05-07Preserve more pattern locations during type checkingBrian Campbell
2019-05-01Jib: Refactor V_callAlasdair Armstrong