Skip to content
Snippets Groups Projects
Commit e4585d1b authored by xleroy's avatar xleroy
Browse files

Suppressed axioms Float.eq_zero_{true,false}, since the latter is

wrong because of +0.0 / -0.0.  
Adapted Clight semantics accordingly.  (Truth value of a float is
defined by comparison Float.cmp Ceq with 0.0, no longer by structural
equality.)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent d71a5cfd
No related branches found
No related tags found
No related merge requests found
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment