summaryrefslogtreecommitdiff
path: root/src/sail.ml
AgeCommit message (Expand)Author
2019-10-17Allow generating C that doesn't hard code any librariesAlasdair Armstrong
2019-10-15More work on bare-metal SailAlasdair Armstrong
2019-10-14Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and bitvector...Alasdair Armstrong
2019-08-22additional option to tweak Coq output to support user-defined monad:pes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-07-31Merge branch 'sail2' into union_barrierAlasdair Armstrong
2019-07-29Add type check after descattering to keep type environments up to dateBrian Campbell
2019-07-18Add a option to check for a feature symbolAlasdair Armstrong
2019-06-19Rewriting improvements for monomorphic aarch64_smallBrian Campbell
2019-06-13Add new option to splice in alternative function definitionsBrian Campbell
2019-06-06SMT: Rename some functions to make usage clearerAlasdair Armstrong
2019-06-06Add an option to pre-compile the axiomatic model for SMTAlasdair Armstrong
2019-06-04SMT: Add a fuzzing tool for the SMT builtinsAlasdair Armstrong
2019-05-31Change specialization interface slightlyAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
2019-05-16SMT: Improve simplification for generated SMTAlasdair Armstrong
2019-05-14Various bugfixesAlasdair Armstrong
2019-05-13Merge branch 'sail2' into smt_experimentsAlasdair
2019-05-13Changes to toFromInterp backend to support aarch64_smallJon French
2019-05-09SMT: Make path conditionals more preciseAlasdair Armstrong
2019-05-05C: Add option to compile using __int128 rather than GMPAlasdair
2019-05-03Jib: Fix optimizations for SMT IR changesAlasdair Armstrong
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-23SMT: Add parser for generated modelsAlasdair Armstrong
2019-04-17SMT: Automatically get model when $counterexample is used rather than $propertyAlasdair Armstrong
2019-04-17SMT: Support register referencesAlasdair Armstrong
2019-04-15SMT: Allow partial specializationsAlasdair Armstrong
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-13SMT: Add count_leading_zeros and more builtinsAlasdair
2019-04-13SMT: More builtinsAlasdair
2019-04-11SMT: Add property and counterexample directiveAlasdair Armstrong
2019-04-09SMT: Experimental Jib->SMT translationAlasdair Armstrong
2019-04-05Fix: Don't remove uncalled polymorphic constructors if they are matched uponAlasdair Armstrong
2019-03-27C: Generate C from sliced specificationsAlasdair Armstrong
2019-03-27Interactive: Refactor sail.ml some moreAlasdair Armstrong
2019-03-27Interactive: Refactor sail.mlAlasdair Armstrong
2019-03-26Rewriter: Expose rewrite passes to interactive modeAlasdair Armstrong
2019-03-19C: Some simplificationAlasdair Armstrong
2019-03-15Add a rewriting pass for constant propagation in mutrecsThomas Bauereiss
2019-03-14C: Some further tweaksAlasdair Armstrong
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-13Remove prover reference from typecheck env when marshalling out defsJon French
2019-03-13C: Improve Jib IR, add SSA representationAlasdair Armstrong
2019-03-09C: Fix miscompilation of constrained struct field accessAlasdair
2019-03-08C: Refactor C backendAlasdair Armstrong
2019-03-06Add an -ir option to print the intermediate representation of a fileAlasdair Armstrong
2019-03-05More optimizations and improvments for C generationAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:19:32 +0000