From 57aae565103c67f110d40f5c879eb8412cc5ee99 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 25 Jul 2023 11:06:10 +0200 Subject: [PATCH] Added missing c elements --- .../mit/theta/c2xcfa/FrontendXcfaBuilder.kt | 4 ++-- .../theta/c2xcfa/TestFrontendXcfaBuilder.kt | 1 + .../xcfa/c2xcfa/src/test/resources/23exotic.c | 20 +++++++++++++++++++ 3 files changed, 23 insertions(+), 2 deletions(-) create mode 100644 subprojects/xcfa/c2xcfa/src/test/resources/23exotic.c diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index 51ea43a5cf..983ba865b1 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -365,7 +365,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo val breakLoc = param.breakLoc val continueLoc = param.continueLoc val returnLoc = param.returnLoc - return statement.accept(this, ParamPack(builder, lastLoc, breakLoc, continueLoc, returnLoc)) + return statement.statement.accept(this, ParamPack(builder, lastLoc, breakLoc, continueLoc, returnLoc)) } override fun visit(statement: CCompound, param: ParamPack): XcfaLocation { @@ -417,7 +417,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo val breakLoc = param.breakLoc val continueLoc = param.continueLoc val returnLoc = param.returnLoc - return statement.accept(this, ParamPack(builder, lastLoc, breakLoc, continueLoc, returnLoc)) + return statement.statement.accept(this, ParamPack(builder, lastLoc, breakLoc, continueLoc, returnLoc)) } override fun visit(statement: CDoWhile, param: ParamPack): XcfaLocation { diff --git a/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt index 4709409030..73b1678668 100644 --- a/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/test/java/hu/bme/mit/theta/c2xcfa/TestFrontendXcfaBuilder.kt @@ -57,6 +57,7 @@ class TestFrontendXcfaBuilder { arrayOf("/20testinline.c"), arrayOf("/21namecollision.c"), arrayOf("/22nondet.c"), + arrayOf("/23exotic.c"), ) } } diff --git a/subprojects/xcfa/c2xcfa/src/test/resources/23exotic.c b/subprojects/xcfa/c2xcfa/src/test/resources/23exotic.c new file mode 100644 index 0000000000..57c0ff3afb --- /dev/null +++ b/subprojects/xcfa/c2xcfa/src/test/resources/23exotic.c @@ -0,0 +1,20 @@ +extern unsigned int __VERIFIER_nondet_uint(); +int main() { + int i = 0; + do{ + unsigned int add = __VERIFIER_nondet_uint(); + switch(add) { + case 0: + break; + case 1: + i += add; + break; + default: + i += 1; + break; + } + if ( i == 5) continue; + if ( i == 11) break; + } while(i < 10); + if(i < 10) reach_error(); +} \ No newline at end of file