Alexander Senier comments

Results 33 comments of


                                            Alexander Senier

Non-null state accepted as final state

I forgot about #700 - I agree.

Using Boolean value as condition causes exception in Z3

Looks related to #611

Remove CVC4-only verification

Is there a way to comment it out and add a comment pointing to a `Workaround` so we don't forget to re-enable it in the future?

Remove CVC4-only verification

Then let's leave it open until the issue is fixed.

Decision: Remove `prove_tests_cvc4` make target in `Makefile` and `prove_cvc4` in `tests/spark/Makefile`. This does not make sense right now as we don't have two provers which are able to reliably prove...

Setting a sequence field by referring to a sequence field of a message

@jklmnn Can you please add a small reproducer to this issue?

Coverage check fails due to case-sensitivity

A warning is easily ignored. I think we should got further and adopt something different than case insensitivity. Once you used an identifier with a specific casing, using it with...

Full test coverage of message specifications

@treiher Is this a duplicate of Componolit/RecordFlux#1215?

Full test coverage of message specifications

I see, so Componolit/RecordFlux#1215 is about doing something and Componolit/RecordFlux#1217 is about doing everything. Then we should keep both to track the long-term effort.

Document specification features

This also is related to #223.