Show error if entry function does not exist

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);
 	}
 

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<D
 					new UnsupportedSyntaxResult<>(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;

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/exception/EntryFunctionException.java

@@ -0,0 +1,41 @@
+/*
+ * Copyright (C) 2025 Matthias Heizmann ([email protected]>)
+ * 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 <http://www.gnu.org/licenses/>.
+ *
+ * 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 ([email protected]>)
+ */
+public class EntryFunctionException extends CACSL2BoogieTranslationException {
+
+	private static final long serialVersionUID = 1L;
+
+	public EntryFunctionException(final ILocation location, final String msg) {
+		super(location, msg);
+	}
+}

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. "