Skip to content

Commit

Permalink
Added unittest to new xsts functionalities
Browse files Browse the repository at this point in the history
  • Loading branch information
RipplB committed Jun 20, 2024
1 parent e159ab6 commit 9ae884b
Show file tree
Hide file tree
Showing 4 changed files with 66 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -372,7 +372,7 @@ XstsConfig<XstsState<S>, XstsAction, P> buildConfig() {
public MultiAnalysisSide<XstsState<S>, S, XstsState<UnitState>, XstsAction, P, UnitPrec> getMultiSide() {
return new MultiAnalysisSide<>(
getAnalysis(),
XstsBlankInitFuncKt.xstsControlInitFunc(),
XstsControlInitFuncKt.xstsControlInitFunc(),
XstsCombineExtractUtilsKt::xstsCombineStates,
XstsCombineExtractUtilsKt::xstsExtractControlState,
XstsCombineExtractUtilsKt::xstsExtractDataState,
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
* http://www.apache.org/licenses/LICENSE-2.0
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/

package hu.bme.mit.theta.xsts.analysis

import hu.bme.mit.theta.analysis.pred.PredState
import hu.bme.mit.theta.analysis.unit.UnitPrec
import hu.bme.mit.theta.analysis.unit.UnitState
import org.junit.jupiter.api.Test

class XstsCombineExtractUtilsUnitTest {

val dataState = PredState.of()
val controlState = XstsState.of(UnitState.getInstance(), true, false)
val xstsState = XstsState.of(dataState, true, false)

@Test
fun `Utils work as expected`() {
assert(xstsCombineStates(controlState, dataState) == xstsState)
assert(xstsExtractControlState(xstsState) == controlState)
assert(xstsExtractDataState(xstsState) == dataState)
assert(xstsExtractControlPrec(UnitPrec.getInstance()) == UnitPrec.getInstance())
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
* http://www.apache.org/licenses/LICENSE-2.0
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/

package hu.bme.mit.theta.xsts.analysis

import hu.bme.mit.theta.analysis.expl.ExplPrec
import hu.bme.mit.theta.analysis.unit.UnitState
import org.junit.jupiter.api.Test

class XstsControlInitFuncUnitTest {

@Test
fun `Returns single unitstate`() {
val result = xstsControlInitFunc<ExplPrec>().getInitStates(ExplPrec.empty())

assert(result.size == 1)
assert(result.single().state == UnitState.getInstance())
}
}

0 comments on commit 9ae884b

Please sign in to comment.