java-semantics
java-semantics copied to clipboard
kframework
The semantics of Java in K
K-Java seems to wrongly represent (negative) floating point numbers that are close to zero, it produces "-0e+00.0" instead of just "-0.0". (Similarly infinity values are incorrectly represented, e.g., "-Infinity.0".)
There seems to be an issue when a cast is performed from a floating-point number that is larger than the maximum Integer to an Integer. In this case, the value...
I noticed that kjtest.sh produces a generator error, when a division by zero is performed, which makes it really difficult to find the problem. Would it be possible that kjtest...
I discovered that simply defining a string `new String("test")` with the new keyword leads to a timeout.
There is an issue when octal values are used in double or float arrays, but they can be used in Integer arrays without any problems. `double[][] vCIFHa = {{0.54,-0x1.83e3a5cp26},{-0x1.013a519cp30,014371144027}};` And...
I discovered a parsing issue for the hexadecimal representation of floats or doubles. When a literal is starting with 0x1.a ... 0x1.f then there is an error, but they get...
Some of my tests showed that K-Java has a wrong precision for float values. I assume that float values were just encoded as double precision values. As a result, I...
There seems to be an issue with the modulo operator. The computation is wrong for all negative doubles and floats, i.e. it produces inconsistent values compared to Java and also...
It's really confusing to just get an empty `*.pkast` file and an inner parser error at the start of exec semantics when the prep semantics times out.
OK, I am copying 20harshita's issue here harshita@harshita-VPCEH25EN:~/java-semantics/src$ kjkompile.sh Preprocessing semantics: [Error] Internal: Uncaught exception thrown of type AssertionError. Please rerun your program with the --debug flag to generate a...
