GV

GeezerVison

The World Wide Web, restored to 800 pixels of glory.

Home|About|Gaming cabinet|Archives|How it works|Starter sites

On this site

  • Sign in
  • ActionsCI/CD and automation
  • CodespacesCloud development environments
  • All Features
  • Documentation
  • Training
  • Certifications
  • Build with Copilot
  • Customize Copilot
  • Integrations
  • Trending repos
  • GitHub Sponsors
  • Developer articles
  • Enterprises

This view

  • Original page
  • New address

GeezerVison is showing github.com — wrong precision for floats · Issue #59 · kframework/java-semantics

wrong precision for floats #59

New issue
Copy link
New issue
Copy link
Open
Open
wrong precision for floats#59
Copy link

Description

@rschumi0
rschumi0
opened on Feb 29, 2020
Issue body actions

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 could observe that in some calculations, K-Java produces results that significantly diverge from the results of Java. Moreover, K-Java sometimes produces a concrete value, whereas Java returns Infinity, which is shown in the following example:

float a = (float) 1 - 1473150328275393513L / 0.16f * 6854191149854506640L * -128033296 * 23412341234123414L;
System.out.println("" + a); //K-Java shows 1.8916947877681303e+62, Java shows Infinity

double b = (double) 1 - 1473150328275393513L / 0.16 * 6854191149854506640L * -128033296 * 23412341234123414L;
System.out.println("" + b); //K-Java and Java shows 1.8916947877681303e+62

Additionally, I noticed that K-Java wrongly represents the infinity value (e.g. -Infinity.0) of double or float calculations and also the exponent representation is a bit different to Java.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions

      You are visitor 01402520 — GeezerVison does not store the pages you look up.
      Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.