diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java index dc6a53a84d1..2fe9afde5c4 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java @@ -212,6 +212,7 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitives; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CStructOrUnion; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.EntryFunctionException; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.IncorrectSyntaxException; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.UnsupportedSyntaxException; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.CDeclaration; @@ -578,7 +579,12 @@ public CHandler(final CHandler prerunCHandler, final ProcedureManager procedureM mPostProcessor = new PostProcessor(mLogger, mExpressionTranslation, mTypeHandler, mReporter, mAuxVarInfoBuilder, mFunctions, mTypeSizes, mSymbolTable, mStaticObjectsHandler, mSettings, procedureManager, mMemoryHandler, mInitHandler, mFunctionHandler, this); - mIsInLibraryMode = !prerunCHandler.mProcedureManager.hasProcedure(mSettings.getEntryFunction()); + mIsInLibraryMode = mSettings.getEntryFunction().equals(""); + if (!mIsInLibraryMode && !prerunCHandler.mProcedureManager.hasProcedure(mSettings.getEntryFunction())) { + final String errorMessage = String.format("Specified entry function %s does not exist in program", + mSettings.getEntryFunction()); + throw new EntryFunctionException(null, errorMessage); + } copyGlobalsFromPrerun(prerunCHandler.mSymbolTable); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/MainTranslator.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/MainTranslator.java index 79b426b523b..fdd2c2b5f77 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/MainTranslator.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/MainTranslator.java @@ -57,6 +57,7 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.BitvectorTranslation; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.ExpressionTranslation; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.IntegerTranslation; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.EntryFunctionException; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.IncorrectSyntaxException; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.UndeclaredFunctionException; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.UnsupportedSyntaxException; @@ -126,7 +127,7 @@ private WrapperNode run(final IExtractedCorrectnessWitness witness, final List(Activator.PLUGIN_NAME, e.getLocation(), e.getLocalizedMessage()); commonDoTranslationExceptionHandling(result); return null; - } catch (final UndeclaredFunctionException e) { + } catch (final UndeclaredFunctionException | EntryFunctionException e) { final IResult result = new ExceptionOrErrorResult(Activator.PLUGIN_NAME, e); commonDoTranslationExceptionHandling(result); return null; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/exception/EntryFunctionException.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/exception/EntryFunctionException.java new file mode 100644 index 00000000000..2e1197921af --- /dev/null +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/exception/EntryFunctionException.java @@ -0,0 +1,41 @@ +/* + * Copyright (C) 2025 Matthias Heizmann (matthias.heizmann@iste.uni-stuttgart.de>) + * Copyright (C) 2025 University of Freiburg + * + * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception; + +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; + +/** + * @author Matthias Heizmann (matthias.heizmann@iste.uni-stuttgart.de>) + */ +public class EntryFunctionException extends CACSL2BoogieTranslationException { + + private static final long serialVersionUID = 1L; + + public EntryFunctionException(final ILocation location, final String msg) { + super(location, msg); + } +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java index 57bab3273fc..eccd5589d72 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java @@ -45,8 +45,7 @@ public class CACSLPreferenceInitializer extends UltimatePreferenceInitializer { private static final String MAINPROC_DESC = - "Specify the entry function of the program. " + "Use an empty string for library mode " - + "(i.e., assume all globals are non-deterministic and verify each function in isolation)."; + "If set to a non-empty string (e.g., main), only executions starting from the specified entry function are considered. Global variables are initialized according to their declared initializers. If set to the empty string, executions starting from any function are considered. In this case, global variables are initialized nondeterministically."; public static final String LABEL_ERROR = "Check unreachability of reach_error function"; private static final String DESC_ERROR = "Check if every call to reach_error is unreachable. This is used for the ReachSafety category of SV-COMP. "