Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / AeneasVerif/aeneas issues and pull requests

#355 - Fix `InterpreterPaths.access_projection`

Issue - State: open - Opened by sonmarcho 5 days ago
Labels: bug

#354 - Rework place access function

Pull Request - State: open - Opened by Nadrieril 5 days ago

#352 - Fix a bug in the pre-pass which eliminates loop breaks

Pull Request - State: closed - Opened by sonmarcho 7 days ago

#351 - Bug in loop fixed-point computation

Issue - State: open - Opened by sonmarcho 7 days ago
Labels: bug

#349 - Make Aeneas call Charon

Issue - State: open - Opened by sonmarcho 9 days ago

#348 - Mark saturating_add/sub as a builtin, and add Lean models to Primitives

Pull Request - State: closed - Opened by R1kM 11 days ago - 2 comments

#348 - Mark saturating_add/sub as a builtin, and add Lean models to Primitives

Pull Request - State: closed - Opened by R1kM 11 days ago - 2 comments

#347 - Update Aeneas to remove the marker traits

Issue - State: open - Opened by sonmarcho 11 days ago - 3 comments

#346 - Add saturating add/sub to the standard library

Issue - State: closed - Opened by sonmarcho 11 days ago - 1 comment

#345 - Nit: Correctly indent abort-on-error option description

Pull Request - State: closed - Opened by R1kM 11 days ago

#345 - Nit: Correctly indent abort-on-error option description

Pull Request - State: closed - Opened by R1kM 11 days ago

#344 - Update charon

Pull Request - State: closed - Opened by Nadrieril 12 days ago

#344 - Update charon

Pull Request - State: closed - Opened by Nadrieril 12 days ago

#343 - Update charon

Pull Request - State: closed - Opened by Nadrieril 24 days ago

#343 - Update charon

Pull Request - State: closed - Opened by Nadrieril 24 days ago

#342 - Support asserts with messages

Issue - State: open - Opened by zhassan-aws about 2 months ago

#341 - Update Aeneas following changes in Charon

Pull Request - State: closed - Opened by sonmarcho about 2 months ago

#340 - Distinguish statements and sequences of statements in LLBC

Issue - State: open - Opened by sonmarcho about 2 months ago

#339 - Update charon

Pull Request - State: closed - Opened by Nadrieril 2 months ago

#338 - Update Charon

Pull Request - State: closed - Opened by R1kM 2 months ago

#337 - Make the backward functions not fail

Issue - State: open - Opened by sonmarcho 2 months ago

#336 - Minimize the parameters of globals/constants

Issue - State: open - Opened by sonmarcho 2 months ago

#335 - Update charon

Pull Request - State: closed - Opened by Nadrieril 2 months ago

#334 - Update charon

Pull Request - State: closed - Opened by Nadrieril 2 months ago

#333 - Use implicit parameters in the generated code

Pull Request - State: closed - Opened by sonmarcho 2 months ago

#332 - Propagate Float literal changes from Charon

Pull Request - State: closed - Opened by R1kM 2 months ago - 1 comment

#331 - Update charon

Pull Request - State: closed - Opened by Nadrieril 2 months ago

#330 - Make minor updates to the tutorial

Pull Request - State: closed - Opened by sonmarcho 3 months ago

#329 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#328 - chore(lean): minimize imports in `Base/Arith`

Pull Request - State: open - Opened by RaitoBezarius 3 months ago - 1 comment

#327 - Turn the ICFP tutorial into a Lean game

Issue - State: open - Opened by RaitoBezarius 3 months ago - 3 comments

#326 - Update the comment for `TypesUtils.ty_is_copyable`

Issue - State: open - Opened by sonmarcho 7 months ago - 2 comments

#325 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#324 - Rename `assumed` to `builtin`

Issue - State: open - Opened by sonmarcho 3 months ago

#323 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#322 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#321 - Adds "support" for float

Pull Request - State: closed - Opened by EschericHya 3 months ago

#320 - test(bst): add BST as an example

Pull Request - State: closed - Opened by RaitoBezarius 3 months ago - 4 comments

#319 - Update betree's `Cargo.lock`

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#317 - Give the possibility of extracting the source code as comments

Issue - State: open - Opened by sonmarcho 3 months ago - 1 comment

#316 - Update the Lean library to 4.11.0-rc2

Pull Request - State: closed - Opened by sonmarcho 3 months ago

#315 - Improve the `progress` tactic

Issue - State: open - Opened by sonmarcho 3 months ago

#313 - Fix the loops of `simp_all` in `scalar_tac`

Issue - State: open - Opened by sonmarcho 3 months ago

#312 - Fetch latest commits in `make setup-charon`

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#311 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#310 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#308 - Use `Nat` and `Int` instead of `Usize` and `Isize`

Issue - State: open - Opened by sonmarcho 3 months ago

#307 - `progress*`

Issue - State: open - Opened by sonmarcho 3 months ago

#306 - Implement a congruence closure tactic

Issue - State: open - Opened by sonmarcho 3 months ago

#303 - Improve `scalar_eq_nf`

Issue - State: open - Opened by sonmarcho 3 months ago

#302 - Improve `scalar_tac`

Issue - State: open - Opened by sonmarcho 3 months ago

#301 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#300 - `make setup-charon` can fail when the OID doesn't exist in Charon

Issue - State: closed - Opened by RaitoBezarius 3 months ago - 3 comments

#299 - Add a conference tutorial

Pull Request - State: closed - Opened by sonmarcho 3 months ago

#298 - Make minor updates

Pull Request - State: closed - Opened by sonmarcho 3 months ago

#297 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#296 - Test crates fail to build in CI

Issue - State: closed - Opened by sonmarcho 3 months ago - 1 comment

#294 - docs: init first sketch

Pull Request - State: open - Opened by RaitoBezarius 3 months ago - 5 comments

#293 - Incorrect/missing translation for non-bool '!'

Issue - State: closed - Opened by simonjwinwood 3 months ago - 3 comments

#292 - Update charon

Pull Request - State: closed - Opened by Nadrieril 3 months ago

#291 - Update charon

Pull Request - State: closed - Opened by Nadrieril 4 months ago

#290 - Update charon

Pull Request - State: closed - Opened by Nadrieril 4 months ago

#289 - New workflow to deploy Aeneas user docs to GitHub pages

Pull Request - State: closed - Opened by pnmadelaine 4 months ago

#288 - Update charon

Pull Request - State: closed - Opened by Nadrieril 4 months ago

#287 - hotfix: drop the "build userdocs"

Pull Request - State: closed - Opened by RaitoBezarius 4 months ago - 10 comments

#286 - Cleanup generics

Pull Request - State: closed - Opened by Nadrieril 4 months ago

#285 - doc: initialize a user-facing mdbook

Pull Request - State: closed - Opened by RaitoBezarius 4 months ago - 8 comments

#284 - interest in isabelle backend?

Issue - State: open - Opened by stuebinm 5 months ago - 3 comments

#283 - Add the AVL tree example

Pull Request - State: closed - Opened by sonmarcho 5 months ago

#282 - Update `scalar_tac` to use the `aesop` tactic

Pull Request - State: closed - Opened by sonmarcho 5 months ago - 1 comment

#281 - feat: progress with a term

Pull Request - State: open - Opened by RaitoBezarius 5 months ago - 2 comments

#280 - Update the Makefile to filter more files when running tests

Pull Request - State: closed - Opened by sonmarcho 5 months ago

#279 - Update Lean to 4.10.0-rc1

Pull Request - State: closed - Opened by sonmarcho 5 months ago - 1 comment

#278 - Update charon

Pull Request - State: closed - Opened by Nadrieril 5 months ago - 1 comment

#277 - feat: progress? to say which theorem has been used

Pull Request - State: closed - Opened by RaitoBezarius 5 months ago - 1 comment

#276 - tests: add AVL example

Pull Request - State: closed - Opened by RaitoBezarius 5 months ago

#275 - Update the lean toolchain to 4.9.0

Pull Request - State: closed - Opened by sonmarcho 5 months ago

#274 - Update charon

Pull Request - State: closed - Opened by Nadrieril 5 months ago

#273 - Fix a minor issue with the loops fixed-point computation

Pull Request - State: closed - Opened by sonmarcho 5 months ago

#272 - Remove redundant `llbc_name` field

Pull Request - State: closed - Opened by Nadrieril 5 months ago

#271 - Update charon

Pull Request - State: closed - Opened by Nadrieril 5 months ago

#270 - Unreachable List Loop

Issue - State: closed - Opened by Thanhson89 5 months ago - 1 comment

#269 - Missing function during analysis pop up

Issue - State: closed - Opened by RaitoBezarius 5 months ago - 1 comment

#268 - Extraction of scalar pattern matching has regressed

Issue - State: closed - Opened by RaitoBezarius 5 months ago - 1 comment

#267 - `core.mem.swap` has invalid type

Issue - State: closed - Opened by RaitoBezarius 5 months ago - 1 comment

#266 - `Option.take` extraction is failing

Issue - State: closed - Opened by RaitoBezarius 5 months ago - 2 comments

#264 - Tweak formatting options

Pull Request - State: closed - Opened by Nadrieril 5 months ago

#263 - Update charon

Pull Request - State: closed - Opened by Nadrieril 5 months ago

#262 - Unexpected name clash

Issue - State: open - Opened by sonmarcho 5 months ago - 4 comments

#261 - Bump Lean to v4.9.0rc3

Pull Request - State: closed - Opened by sonmarcho 5 months ago