Skip to content

Commit

Permalink
Create NullCharsetTest.java
Browse files Browse the repository at this point in the history
Developed UnitTest to address the error from #429
  • Loading branch information
joalen committed Nov 17, 2024
1 parent d48e34d commit 1ee4a1a
Showing 1 changed file with 23 additions and 0 deletions.
23 changes: 23 additions & 0 deletions src/tests/NullCharsetTest.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;
import java.nio.file.Path;

public class NullCharsetTest extends TestJPF
{
@Test
public void testDirectPathEntry()
{
if (verifyNoPropertyViolation())
{
try {
Path.of("/tmp");
} catch (IllegalArgumentException iae)
{
if ("Null charset name".equals(e.getMessage()))
{
fail("IllegalArgumentException with 'Null charset name' encountered");
}
}
}
}
}

0 comments on commit 1ee4a1a

Please sign in to comment.