- Sep 29, 2020
-
-
Marek Chalupa authored
Was buggy.
-
Marek Chalupa authored
Assert that createState() returns a clean state
-
Marek Chalupa authored
We must set also the original object as read-only.
-
Marek Chalupa authored
-
Marek Chalupa authored
And prepare for invariants strengthening.
-
Marek Chalupa authored
-
Marek Chalupa authored
For easiser debugging.
-
- Sep 28, 2020
-
-
Marek Chalupa authored
-
Marek Chalupa authored
It may happen that the state do not have the substituted value.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We do not want to set the pc in that case.
-
Marek Chalupa authored
-
Marek Chalupa authored
Do not return the Relation object but AssertAnnotation
-
- Sep 27, 2020
-
-
Marek Chalupa authored
We want annotations that should hold in the starting point of the path, not in the last point of the path.
-
Marek Chalupa authored
It is going to be handy for annotations of CFG.
-
- Sep 26, 2020
-
-
Marek Chalupa authored
And prepare for extending.
-
Marek Chalupa authored
We are going to extend them to other types of annotations.
-
Marek Chalupa authored
-
Marek Chalupa authored
isReady -> isReady()
-
Marek Chalupa authored
takes states and adds them into the result
-
Marek Chalupa authored
-
Marek Chalupa authored
Lessen the dependencies on naive kindse.
-
Marek Chalupa authored
Instance of executor adjusted to executing paths.
-
- Sep 25, 2020
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We have problems with empty prefixes. Now we must just adjust the invariant generation.
-
Marek Chalupa authored
-
Marek Chalupa authored
We are going to put in their place our code anyway.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
So that we do not fail the induction proof due to a state that is not error but is e.g., terminated.
-
Marek Chalupa authored
we always printed that the step is {1}...
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Indent the output of the nested executor.
-
Marek Chalupa authored
Show the whole path, i.e., the prefix and also the blocks that correspond to the step.
-
Marek Chalupa authored
-