Programs containing floating point cannot be verified on Windows/Mac
Checking programs containing floating-point operation via ValueAnalysis or PredicateAnalysis is not possible on Windows 10 due to unavailibility of the FloatingPoints library:
Exception in thread "main" java.lang.UnsatisfiedLinkError: no FloatingPoints in java.library.path: C:\Programs\eclipse\plugins\org.eclipse.justj.openjdk.hotspot.jre.full.win32.x86_64_17.0.6.v20230204-1729\jre\bin;C:\Windows\Sun\Java\bin;C:\Windows\system32;C:\Windows;C:/Programs/eclipse//plugins/org.eclipse.justj.openjdk.hotspot.jre.full.win32.x86_64_17.0.6.v20230204-1729/jre/bin/server;C:/Programs/eclipse//plugins/org.eclipse.justj.openjdk.hotspot.jre.full.win32.x86_64_17.0.6.v20230204-1729/jre/bin;C:\Program Files\Common Files\Oracle\Java\javapath;C:\Windows\system32;C:\Windows;(...redacted...).
at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2429)
at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:818)
at java.base/java.lang.System.loadLibrary(System.java:1989)
at org.sosy_lab.common.NativeLibraries.loadLibrary(NativeLibraries.java:200)
at org.sosy_lab.cpachecker.util.floatingpoint.CFloatNativeAPI.<clinit>(CFloatNativeAPI.java:25)
at org.sosy_lab.cpachecker.util.floatingpoint.CFloatNative.<init>(CFloatNative.java:19)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTLiteralConverter.parseFloatLiteral(ASTLiteralConverter.java:172)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTLiteralConverter.convert(ASTLiteralConverter.java:83)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionWithSideEffectsNotSimplified(ASTConverter.java:483)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionWithSideEffects(ASTConverter.java:434)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:2818)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:2725)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.createDeclaration(ASTConverter.java:2029)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:1911)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.createEdgeForDeclaration(CFAFunctionBuilder.java:354)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.handleSimpleDeclaration(CFAFunctionBuilder.java:332)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.visit(CFAFunctionBuilder.java:305)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTSimpleDeclaration.accept(CASTSimpleDeclaration.java:94)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTDeclarationStatement.accept(CASTDeclarationStatement.java:82)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTCompoundStatement.accept(CASTCompoundStatement.java:89)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTFunctionDefinition.accept(CASTFunctionDefinition.java:141)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.handleFunctionDefinition(CFABuilder.java:408)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.createCFA(CFABuilder.java:356)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.buildCFA(EclipseCParser.java:338)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseSomething(EclipseCParser.java:130)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseString(EclipseCParser.java:149)
at org.sosy_lab.cpachecker.cfa.CParserWithLocationMapper.parseFiles(CParserWithLocationMapper.java:215)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseToCFAs(CFACreator.java:731)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseFileAndCreateCFA(CFACreator.java:495)
at org.sosy_lab.cpachecker.core.CPAchecker.parse(CPAchecker.java:455)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:320)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:169)
The exception is triggered whenever parsing a floating-point literal, so the following code throws an exception:
int main() {
float foo = 0.f;
}
Just declaring a floating-point variable is fine:
int main() {
float foo;
}
Upon further inspection, the responsible library is a part of CPAchecker, source code located in lib/native/source/cFloatingPointlib.c
. x64 Linux and Mac OS X precompiled libraries are available under lib/native
as well (in case of Mac OS X, for FloatingPoints only, which signifies its ubiquity).
The FloatingPoints library seems to be a simple single-file C library called from Java via JNI. It is called from org.sosy_lab.cpachecker.util.floatingpoint.CFloatNative
which is deprecated (the reason is not specified). Most of its functionality seems to have been absorbed into CFloatImpl
from the same package. Apart from tests, the only construction of CFloatNative
(which triggers the loading of the library via a static block) is in org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTLiteralConverter.parseFloatLiteral
:
...
// TODO: replace CFloatNative-class by CFloatImpl when available
CFloat cFloat;
if (pValueStr.endsWith("L") || pValueStr.endsWith("l")) {
cFloat = new CFloatNative(pValueStr, CFloatNativeAPI.FP_TYPE_LONG_DOUBLE);
} else if (pValueStr.endsWith("F") || pValueStr.endsWith("f")) {
cFloat = new CFloatNative(pValueStr, CFloatNativeAPI.FP_TYPE_SINGLE);
} else {
// literal has no suffix declared
cFloat = new CFloatNative(pValueStr, CFloatNativeAPI.FP_TYPE_DOUBLE);
}
...
The constructor of CFloatImpl
converting a string literal to float exists, though the question is whether it is correct. Issue #575 seems to pertain to it. In my opinion, the best course of action would be make sure the CFloatImpl constructor from literal works well and finish replacing CFloatNative by CFloatImpl.