summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-04-29SMT: Support arbitrary tuple sizesAlasdair Armstrong
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-26Fix some broken interpreter testsAlasdair Armstrong
2019-04-26More constructor monomorphisation supportBrian Campbell
2019-04-25Update coq read_mem/write_mem.Prashanth Mundkur
2019-04-25Fill in missing map_..._annot caseBrian Campbell
2019-04-25More read/write function updatesBrian Campbell
2019-04-25Get basic constructor monomorphisation working againBrian Campbell
2019-04-25Update prelude in mono testsBrian Campbell
2019-04-25Make constructor splitting in monomorphisation obey -dall_split_errorsBrian Campbell
2019-04-25Don't try to insert monomorphisation casts when the types are the sameBrian Campbell
2019-04-25lem gen_lib: update read/write functions to take (dummy) addrsize argument as...Jon French
2019-04-25SMT: Provide a more useful error message when topsort failsAlasdair
2019-04-24SMT: Make sure we clear overflow checks between generating propertiesAlasdair Armstrong
2019-04-24SMT: Can now recheck some simple models via the interpreterAlasdair
2019-04-23SMT: Add some commentsAlasdair
2019-04-23SMT: Only check counterexamples automatically with -smt_auto flagAlasdair Armstrong
2019-04-23SMT: Add parser for generated modelsAlasdair Armstrong
2019-04-23SMT: Add signed builtinThomas Bauereiss
2019-04-20SMT: Support writing to register referencesAlasdair Armstrong
2019-04-20Fix: Reduce constant-fold time for ARM from 20min+ to 10sAlasdair Armstrong
2019-04-19Coq: when replacing n_constraints in types allow for some rearrangementBrian Campbell
2019-04-19Coq: more robust handling of unknown constraintsBrian Campbell
2019-04-18Parameterise memory read/write primitives by address lengthJon French
2019-04-17Add interpreter annots to vector_dec.Prashanth Mundkur
2019-04-17SMT: Automatically get model when $counterexample is used rather than $propertyAlasdair Armstrong
2019-04-17Coq: support pure loops with termination measuresBrian Campbell
2019-04-17SMT: Support register referencesAlasdair Armstrong
2019-04-17now without memory leaksJon French
2019-04-17add unimplemented C platform definitions for platform_read_mem etcJon French
2019-04-17SMT: Support generic vectors and handle lets between specs and functionsAlasdair Armstrong
2019-04-17SMT: Unroll simple foreach loopsAlasdair Armstrong
2019-04-17Merge pull request #42 from crabtw/sail2Robert Norton
2019-04-17Add base64 package constraintJyun-Yan You
2019-04-17Remove obsolete generated files from .gitignore directory so they will show u...Robert Norton
2019-04-17Allow libsail to be installed without the other things (for rmem)Shaked Flur
2019-04-17Build libsail again (removed Bytcode and Share_directory)Shaked Flur
2019-04-16Temporarily remove Makefile part that is making Jenkins failAlasdair Armstrong
2019-04-16Fix: Don't repeat ctyp_of_typ callAlasdair Armstrong
2019-04-16Remove unnecessary assertThomas Bauereiss
2019-04-16SMT: Support toplevel letbindingsAlasdair Armstrong
2019-04-16SMT: Fix inlining issuesAlasdair Armstrong
2019-04-16Code for testing builtins with CoqBrian Campbell
2019-04-16Coq: make bools_of_int (and hence get_slice_int) compute wellBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 06:55:44 +0000