@@ -0,0 +1,2198 @@
+package edu.kit.iti.formal.pse.worthwhile.prover;%0A%0Aimport org.junit.Assert;%0Aimport org.junit.Test;%0A%0Aimport edu.kit.iti.formal.pse.worthwhile.common.tests.TestASTProvider;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.Program;%0A%0A/**%0A * Test for %7B@link DivisionByZeroAssertionInserter%7D which ensures that Divisions by zero cause the proof to fail.%0A * %0A * @author Leon Handreke%0A */%0Apublic class DivisionByZeroAssertionInserterTest %7B%0A%0A%09/**%0A%09 * Test if division by a zero literal causes the proof to fail.%0A%09 */%0A%09@Test%0A%09public final void testDivisionByZeroLiteral() %7B%0A%09%09Program p = TestASTProvider.getRootASTNode(%22Integer a := 1/0%5Cn_assert(true)%5Cn%22);%0A%09%09SpecificationChecker checker = new SpecificationChecker();%0A%09%09Validity validity = checker.checkProgram(p);%0A%09%09Assert.assertEquals(Validity.INVALID, validity);%0A%09%7D%0A%0A%09/**%0A%09 * Test if division by a variable set to zero causes the proof to fail.%0A%09 */%0A%09@Test%0A%09public final void testDivisionByZeroVariable() %7B%0A%09%09Program p = TestASTProvider.getRootASTNode(%22Integer a := 0%5CnInteger b := 42 / a%5Cn_assert(true)%5Cn%22);%0A%09%09SpecificationChecker checker = new SpecificationChecker();%0A%09%09Validity validity = checker.checkProgram(p);%0A%09%09Assert.assertEquals(Validity.INVALID, validity);%0A%09%7D%0A%0A%09/**%0A%09 * Test if division by a variable that was previously set to zero causes the proof to succeed like it should.%0A%09 */%0A%09@Test%0A%09public final void testDivisionByMultipleZeroVariables() %7B%0A%09%09Program p = TestASTProvider%0A%09%09                .getRootASTNode(%22Integer a := 2%5CnInteger b := 42 / a%5Cna := 0%5Cnb := 42 / 1%5Cn_assert(true)%5Cn%22);%0A%09%09SpecificationChecker checker = new SpecificationChecker();%0A%09%09Validity validity = checker.checkProgram(p);%0A%09%09Assert.assertEquals(Validity.VALID, validity);%0A%09%7D%0A%0A%09/**%0A%09 * Test if Divisions by zero inside the condition of a Conditional cause the proof to fail.%0A%09 */%0A%09@Test%0A%09public final void testDivisionByZeroInConditional() %7B%0A%09%09Program p = TestASTProvider.getRootASTNode(%22Integer a := 0%5Cnif(10 / a = 2) %7B%5Cn    a := 0%5Cn%22%0A%09%09                + %22    Integer b := 42 / 1%5Cn%7D%5Cn_assert(true)%5Cn%22);%0A%09%09SpecificationChecker checker = new SpecificationChecker();%0A%09%09Validity validity = checker.checkProgram(p);%0A%09%09Assert.assertEquals(Validity.INVALID, validity);%0A%09%7D%0A%7D%0A

Add test for division by zero