Quickchecking of domains from my bachelor's thesis#86
Conversation
…bitrary to PMap, Normal, Variables
# Conflicts: # src/domains/domainProperties.ml
# Conflicts: # src/analyses/mCP.ml # src/framework/analyses.ml # src/framework/constraints.ml # src/framework/control.ml
|
If I run this in its current state, it reports hundreds of errors |
* Integers isn't a lattice. * Lifted isn't an abstraction of IntegerSet.
|
That was about right. I pushed a change to remove improper domains ( To see which domains and properties fail it's nicer to use The biggest issues are with circular intervals, DefExc and Enums. I haven't looked into them though. Could also have something to do with the ranges of those. |
# Conflicts: # goblint.opam.locked # make.sh # src/cdomains/intDomain.ml
vesalvojdani
left a comment
There was a problem hiding this comment.
Good. This will now run domain tests on the CI, but a lot of the domains are commented out. Please create new ticket for that.
This runs the test only in the Github CI and not on Travis, right? Any reasons for that? |
|
The selfish reason is that it was easiest to add to GitHub Actions. You can also add it to the Travis scripts if you want. This also raises the question of whether we need both CI-s running the same tests and maintaining both, each with its own possible oddities. |
No, having only the Github actions would be fine with me. Anyone sees a reason for keeping Travis around? @vesalvojdani @vogler @jerhard ? |
|
Any CI (there's also this dockercloud) should just have to call |
|
On GitHub Actions I added the domain tests as a separate step so they show up nicely as a separate block. Adding it to |
|
No strong opinion. Can we keep the files around and disable all but GitHub Actions? I see Travis as an app that can be disabled, but this docker integration seems to be just picked up from the file. |
Closes #84.
Besides testing lattice properties, there are also properties for testing the validity of integer domain operations as abstraction of sets of integers.
Usage
make domaintest./goblint.domaintest.See
--helpfor other useful flags provided by qcheck, e.g.-vor--long.Possible improvements
arbitraryout ofPrintable.S. This would separate the testing code from actual functionality. And it might be necessary anyway to use AFL for that purpose instead. Could be hard though because of functors.srcdirectory to maybeunittest. The property tests might integrate with OUnit.