Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for floating-point arithmetic added #6

Open
wants to merge 34 commits into
base: master
Choose a base branch
from

Conversation

dannem1337
Copy link

@dannem1337 dannem1337 commented Oct 18, 2023

This PR adds basic support for Float, Double and Long Double using the theory of rationals.

What has been added:

  • Support for floating-point and operations between them, the new file Floating-Point has been added which adds support the floating-point types and allowing operations is added in CCBinaryExpressions
  • Regression tests of all floating-point data types

What is missing:

  • Operations causing NaN and Inf. Both NaN and Inf are supported, however, operations such as Con1/0 or 0/0 do not cause them
  • Conversion of Data-types
  • The function longFoubleToFraction does not have a correct implementation of long doubles

dannem1337 and others added 30 commits March 28, 2023 20:35
.attach_pid35637 Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There seem to be some empty files added by mistake.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please call make on the ACSL parser and commit the new jar file as well (that's not built as part of the build process).

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Empty file.

def isNeginf(t: ITerm): IFormula = longDoubleADT.hasCtor(t, 3)
}

object LongDoubles {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should avoid making CCReader longer than it already is :-) The new classes/objects you add can be in a new file.

import CCReader._
import ccreader._
import tricera.params.TriCeraParameters
import tricera.concurrency.CCReader
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The changes in this file seem unnecessary.

@zafer-esen
Copy link
Collaborator

zafer-esen commented Oct 18, 2023

@dannem1337 Thank you for creating this PR! I added some quick comments , would be nice if you could address them! It would also be helpful to provide a more detailed PR description.

@dannem1337
Copy link
Author

Hello,
I've made the changes according to the review and changed the description to be a bit more detailed! :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants