summaryrefslogtreecommitdiff
path: root/src/reporting.ml
AgeCommit message (Expand)Author
2021-03-05Add more location information to IRAlasdair
2020-05-12Add support for instrumenting generated C with branch coverage metricsAlasdair
2020-05-12Support for user-defined state and headers in new codegenAlasdair
2019-11-11Make sure we include LEXP_cast register refs when slicing the specificationAlasdair Armstrong
2019-06-28Add a warning for potentially unsafe castsAlasdair
2019-05-29Fix sail_truncate error message in SMTAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-04-11SMT: Add property and counterexample directiveAlasdair Armstrong
2019-04-05Lem: Make generated assertion messages look nicer in prover outputAlasdair
2018-12-26Some cleanupAlasdair Armstrong
2018-12-26More error messages improvmentsAlasdair Armstrong
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-11-20Add messages for assert failures without user defined messagesAlasdair Armstrong
2018-11-19Don't re-check AST repeatedly in exp_lift_assign re-writeAlasdair Armstrong
2018-10-31Remove Parse_ast.Int, add unique locationsAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong