summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-05-19Coq: remove unhelpful type printing restriction on early returnsBrian Campbell
2019-05-19Add constraints to undefined vector functions to ensure that lengths areBrian Campbell
2019-05-17SMT: Finish adding all memory builtins from lib/regfp.sailAlasdair Armstrong
2019-05-16Fix: Add a feature symbol for new constant type variable syntaxAlasdair Armstrong
2019-05-16SMT: Tweak SMT generation interfaceAlasdair Armstrong
2019-05-16SMT: Improve simplification for generated SMTAlasdair Armstrong
2019-05-1594f445 introduced a new name for _ref_deref, add it to the effect rewritingBrian Campbell
2019-05-14SMT: Allow printing SMT with an optional variable prefixAlasdair Armstrong
2019-05-14Various bugfixesAlasdair Armstrong
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14SMT: Add comment explaining path conditionalsAlasdair Armstrong
2019-05-14Fix: Issue a warning for any unrecognised directiveAlasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
2019-05-13Merge branch 'sail2' into smt_experimentsAlasdair
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-05-13Interpreter: update memory intrinsics to include addrsize argumentJon French
2019-05-13Changes to toFromInterp backend to support aarch64_smallJon French
2019-05-13don't emit cache_op_kind enum in LemJon French
2019-05-13add more primops for aarch64_small (sub_nat, append_list)Jon French
2019-05-13move simple_string_of_loc to Ast_utilJon French
2019-05-10SMT: Implement memory events for read_mem and write_memAlasdair
2019-05-10SMT: Experiment with symbolic memory reads and writesAlasdair Armstrong
2019-05-10SMT: Fix error in get_pathcondAlasdair Armstrong
2019-05-10SMT: Lazily compute efficient path conditionalsAlasdair
2019-05-09SMT: Add explicit terminators to SSA graphAlasdair Armstrong
2019-05-09SMT: Make path conditionals more preciseAlasdair Armstrong
2019-05-08SMT: Add test for various real number propertiesAlasdair Armstrong
2019-05-08SMT: Add reals and strings to SMT backendAlasdair Armstrong
2019-05-07Move parser combinators shared by property and model parsing to separate fileAlasdair Armstrong
2019-05-07SMT: Use builtin_type_error consistently across builtin definitionsAlasdair Armstrong
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-06Handle type variables generated while inferring applications in monomorphisationBrian Campbell
2019-05-06Avoid degenerate construction monomorphisation, use # in generated namesBrian Campbell
2019-05-06Apply constructor monomorphisation in preference to variable splitsBrian Campbell
2019-05-06Calculate some type variable substitutions during constant propagationBrian Campbell
2019-05-06Handle global constants in monomorphisationBrian Campbell
2019-05-06Cope with irrelevant existentials when monomorphising constructorsBrian Campbell
2019-05-06Don't initialise registers in interpreter when register accesses not allowedBrian Campbell
2019-05-06Expand constraints while looking for sets during monomorphisationBrian Campbell
2019-05-05C: Add option to compile using __int128 rather than GMPAlasdair
2019-05-03Jib: Optimize set_slice for ARM v8.5Alasdair Armstrong
2019-05-03Jib: Fix optimizations for SMT IR changesAlasdair Armstrong
2019-05-01SMT: Fix some C optimisations that were disabledAlasdair Armstrong
2019-05-01Jib: Refactor V_callAlasdair Armstrong
2019-04-30SMT: Allow custom queriesAlasdair Armstrong
2019-04-30SMT: Fix dead-code FIXME in jib_compileAlasdair Armstrong
2019-04-30SMT: Simplify and generalise checking eventsAlasdair Armstrong
2019-04-29SMT: Refactor overflow checks into generic event checking systemAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 11:13:03 +0000