[fix] Small fixes

Author: Columpio

lib/Core/MockBuilder.cpp

@@ -193,10 +193,6 @@ void MockBuilder::buildExternalFunctionsDefinitions() {
         llvm::BasicBlock::Create(mockModule->getContext(), "entry", func);
     builder->SetInsertPoint(BB);
 
-    if (!func->getReturnType()->isSized()) {
-      builder->CreateRet(nullptr);
-      continue;
-    }
 
     const auto nameToAnnotations = annotations.find(extName);
     if (nameToAnnotations != annotations.end()) {
@@ -319,6 +315,7 @@ bool tryAlign(llvm::Function *func,
               const std::vector<std::vector<Statement::Ptr>> &statements,
               std::vector<std::vector<Statement::Ptr>> &res) {
   if (func->arg_size() == statements.size()) {
+    res = statements;
     return true;
   }
 
@@ -411,6 +408,10 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
 void MockBuilder::buildAnnotationForExternalFunctionReturn(
     llvm::Function *func, const std::vector<Statement::Ptr> &statements) {
   auto returnType = func->getReturnType();
+  if (!returnType->isSized()) { // void return type
+    builder->CreateRet(nullptr);
+    return;
+  }
   std::string retName = "ret_" + func->getName().str();
 
   auto *mockReturnValue = builder->CreateAlloca(returnType, nullptr);

lib/Module/Annotation.cpp

@@ -63,14 +63,16 @@ void Unknown::initOffset() {
     case '[': {
       size_t posEndExpr = offsetStr.find(']', pos);
       if (posEndExpr == std::string::npos) {
-        klee_error("Annotation: Incorrect offset format \"%s\"", str.c_str());
+        klee_warning("Annotation: Incorrect offset format \"%s\"", str.c_str());
+        continue;
       }
       offset.push_back(offsetStr.substr(pos + 1, posEndExpr - 1 - pos));
       pos = posEndExpr;
       break;
     }
     default: {
-      klee_error("Annotation: Incorrect offset format \"%s\"", str.c_str());
+      klee_warning("Annotation: Incorrect offset format \"%s\"", str.c_str());
+      continue;
     }
     }
   }