summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2018-07-17Coq: handle E_constraint properlyBrian Campbell
Adds missing constraints for aarch64
2018-07-16Coq: fix false existential problemBrian Campbell
2018-07-16Coq: we also unfold lengthBrian Campbell
2018-07-16Coq: handle simple type variable matches properly and nat typeBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
As a result, add proof to pow2.
2018-07-13Merge branch 'sail2' of github.com:rems-project/sail into sail2Brian Campbell
2018-07-13Coq: avoid a couple of common identifiersBrian Campbell
2018-07-12Handle failures during interpreting betterAlasdair Armstrong
Changes to the interpreter to better support constant folding during compilation mean it can now throw exceptions to the caller, allow the caller to handle the error, rather than simply printing an error. This broke the ARM interpreter test because exit() is handled by throwing an Exit exception in the interpreter.
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ↵Robert Norton
interpreter implementations of same.
2018-07-12Coq: get rid of syntax error on exception handlingBrian Campbell
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: more autocast insertionBrian Campbell
2018-07-12Coq: tuple matching in loopsBrian Campbell
2018-07-12Coq: more accurate autocast insertionBrian Campbell
2018-07-12Fix bug for large integers in OCaml compilationAlasdair Armstrong
2018-07-12Minor fix to support OCaml 4.02.3Shaked Flur
2018-07-12Fixes for ARM Sail tests, and get_time_ns for interpreterAlasdair
2018-07-11RISC-V model fixes for RMEMJon French
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
On second thought, this change should not really make a difference; the CHERI test suite still passes without it. Moreover, using unsigned conversion of the vector argument leads to more convenient lemmas for the provers.
2018-07-11Fix some signedness bugsThomas Bauereiss
add_vec_int and similar functions in the Lem library used unsigned instead of signed conversion.
2018-07-10fix constructor typoJon French
2018-07-10Only put static qualifier on valspecs when -static flag is usedAlasdair Armstrong
2018-07-10disable printing when compiling to Lem to keep rmem happyJon French
2018-07-10Aarch64 mono script updateBrian Campbell
2018-07-09Initialize fresh memory to 0 in the OCaml backend.Prashanth Mundkur
This makes it consistent with the C backend, and also makes it easier to compare traces across execution re-runs.
2018-07-09Lem: prefer type variables to constants when looking for equivalent nexpsBrian Campbell
If we have an nexp that we can't print, look for an equivalent type variable before looking for a constant - the constant may only be valid locally (e.g., under an if) while the type variable will be valid throughout the function. Fixes a problem with aget_Mem on aarch64.
2018-07-09Changes for anonymisation. Ensure headers are in correct format. Remove some ↵Robert Norton
redundant files.
2018-07-09Coq: remove some unnecessary castsBrian Campbell
2018-07-09Fix bug in rewriting of try-catch-blocks with variable updatesThomas Bauereiss
2018-07-09Tweak rewriting of literal patterns for LemThomas Bauereiss
2018-07-09Add explanatory comment to guard rewritingThomas Bauereiss
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list.
2018-07-08Add -static flag that controls whether generated C functions are staticAlasdair
By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
2018-07-07Coq: precise generic vectorsBrian Campbell
(probably still some pattern matching to do, but I don't think the models use that)
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
2018-07-06Coq: support assertions inside and outside of blocksBrian Campbell
2018-07-06Coq: avoid nexp simplification when deciding whether a cast is neededBrian Campbell
2018-07-06Coq: Avoid clashes with the monad name, MBrian Campbell
2018-07-06Coq: feed assertions into the contextBrian Campbell
2018-07-06Coq: reduce use of sumbool_of_bool to relevant constraintsBrian Campbell
2018-07-06Coq: missing existential building for rangesBrian Campbell
2018-07-06Coq: turn off partial support for dropping true constraints, fix stringsBrian Campbell
2018-07-05Fix equality comparisons for variants in CAlasdair
Makes sure equality comparisons for variants are compiled correctly. Needed for CHERI and mips, which have structs containing variants. Also make sure that struct equality works for structs containing other structs.
2018-07-05Fix equality comparisons for structsAlasdair
Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any builtin type in sail.h.
2018-07-05Fix CHERI test that was failing when compiled to CAlasdair Armstrong
Non bitvector literals for decreasing vectors were not being reversed correctly, so the list of capability registers was effectively in reverse order. Added a test case to test/c/ based on this aspect of CHERI
2018-07-05make many generated c functions static -- this gives the compiler a chance ↵Robert Norton
to notice if they are dead or inline them if appropriate, cleaning up coverage reports and potentially improving execution speed.
2018-07-05restore missing RISC-V fence types in sail2; ignore io bits in fences more ↵Jon French
cleanly
2018-07-03Fix a bug in foreach loopsAlasdair Armstrong
We should test before the first iteration in case 'to' starts out as less than 'from'.
2018-07-03Fix letbind_effects on LEXP_deref with an effectful subexpressionBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:05:16 +0000