Fix #431, add in range assumption in library mode (#611)

ultimate-pa · Jan 16, 2023 · c2bf16b · c2bf16b
1 parent 04fb33c
commit c2bf16b
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 4 deletions.
diff --git a/...src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java b/...src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java
@@ -364,6 +364,8 @@ public class CHandler {
 
 	private final DataRaceChecker mDataRaceChecker;
 
+	private final boolean mIsInLibraryMode;
+
 	/**
 	 * Constructor for CHandler in pre-run mode.
 	 *
@@ -447,6 +449,7 @@ public CHandler(final ILogger logger, final ICACSL2BoogieBacktranslatorMapping b
 				mFunctionToIndex, mTypeSizes, mSymbolTable, mStaticObjectsHandler, mSettings, mProcedureManager,
 				mMemoryHandler, mInitHandler, mFunctionHandler, this);
 
+		mIsInLibraryMode = false;
 	}
 
 	/**
@@ -539,6 +542,7 @@ public CHandler(final CHandler prerunCHandler, final ProcedureManager procedureM
 		mPostProcessor = new PostProcessor(mLogger, mExpressionTranslation, mTypeHandler, mReporter, mAuxVarInfoBuilder,
 				mFunctionToIndex, mTypeSizes, mSymbolTable, mStaticObjectsHandler, mSettings, procedureManager,
 				mMemoryHandler, mInitHandler, mFunctionHandler, this);
+		mIsInLibraryMode = !prerunCHandler.mProcedureManager.hasProcedure(mSettings.getEntryMethod());
 
 	}
 
@@ -1476,7 +1480,7 @@ public Result visit(final IDispatcher main, final IASTFunctionDefinition node) {
 		mCurrentDeclaredTypes.pop();
 		assert declResult.getDeclaration().getType() instanceof CFunction;
 		return mFunctionHandler.handleFunctionDefinition(main, mMemoryHandler, node, declResult.getDeclaration(),
-				mContract);
+				mContract, mIsInLibraryMode);
 	}
 
 	public Result visit(final IDispatcher main, final IASTGotoStatement node) {

diff --git a/...urg/informatik/ultimate/cdt/translation/implementation/base/chandler/FunctionHandler.java b/...urg/informatik/ultimate/cdt/translation/implementation/base/chandler/FunctionHandler.java
@@ -260,10 +260,12 @@ public Result handleFunctionDeclarator(final IDispatcher main, final ILocation l
 	 * @param node
 	 *            the node to translate.
 	 * @param contract
+	 * @param isInLibraryMode
 	 * @return the translation result.
 	 */
 	public Result handleFunctionDefinition(final IDispatcher main, final MemoryHandler memoryHandler,
-			final IASTFunctionDefinition node, final CDeclaration cDec, final List<ACSLNode> contract) {
+			final IASTFunctionDefinition node, final CDeclaration cDec, final List<ACSLNode> contract,
+			final boolean isInLibraryMode) {
 
 		final ILocation loc = mLocationFactory.createCLocation(node);
 		final String definedProcName = cDec.getName();
@@ -376,7 +378,7 @@ public Result handleFunctionDefinition(final IDispatcher main, final MemoryHandl
 			final ExpressionResultBuilder bodyResultBuilder = new ExpressionResultBuilder();
 
 			// 1)
-			handleFunctionsInParams(main, loc, memoryHandler, bodyResultBuilder, node);
+			handleFunctionsInParams(main, loc, memoryHandler, bodyResultBuilder, node, isInLibraryMode);
 			// 2)
 			final ExpressionResult bodyResult = (ExpressionResult) main.dispatch(node.getBody());
 			bodyResultBuilder.addAllExceptLrValue(bodyResult);
@@ -874,9 +876,11 @@ private VarList[] processInParams(final ILocation loc, final CFunction cFun, fin
 	 * @param stmt
 	 *            the statement list to append to.
 	 * @param parent
+	 * @param isInLibraryMode
 	 */
 	private void handleFunctionsInParams(final IDispatcher main, final ILocation loc, final MemoryHandler memoryHandler,
-			final ExpressionResultBuilder resultBuilder, final IASTFunctionDefinition parent) {
+			final ExpressionResultBuilder resultBuilder, final IASTFunctionDefinition parent,
+			final boolean isInLibraryMode) {
 		final VarList[] inparamVarListArray =
 				mProcedureManager.getCurrentProcedureInfo().getDeclaration().getInParams();
 		IASTNode[] paramDecs;
@@ -945,6 +949,10 @@ private void handleFunctionsInParams(final IDispatcher main, final ILocation loc
 						inParamAuxVarType, inparamBId, new DeclarationInformation(StorageClass.IMPLEMENTATION_INPARAM,
 								mProcedureManager.getCurrentProcedureInfo().getProcedureName()));
 
+				if (isInLibraryMode) {
+					mExpressionTranslation.addAssumeValueInRangeStatements(loc, rhsId, cvar, resultBuilder);
+				}
+
 				final ILocation igLoc = LocationFactory.createIgnoreLocation(loc);
 				if (isOnHeap && !(cvar instanceof CArray)) {
 					final VariableLHS tempLHS = ExpressionFactory.constructVariableLHS(loc,