diff --git a/include/revng/ABIAnalyses/Common.h b/include/revng/ABIAnalyses/Common.h
new file mode 100644
index 000000000..80ef0d8cb
--- /dev/null
+++ b/include/revng/ABIAnalyses/Common.h
@@ -0,0 +1,287 @@
+#pragma once
+
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/SmallSet.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/GlobalVariable.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Value.h"
+#include "llvm/Support/Casting.h"
+
+#include "revng/BasicAnalyses/GeneratedCodeBasicInfo.h"
+#include "revng/MFP/MFP.h"
+#include "revng/Model/Binary.h"
+#include "revng/Support/revng.h"
+
+namespace ABIAnalyses {
+
+using Register = model::Register::Values;
+
+enum TransferKind {
+  Read,
+  Write,
+  WeakWrite,
+  TheCall,
+  None,
+};
+
+struct ABIAnalysis {
+private:
+  llvm::SmallSet<llvm::GlobalVariable *, 20> ABIRegisters;
+  llvm::SmallVector<llvm::GlobalVariable *, 20> RegisterList;
+  const llvm::Instruction *CallSite;
+
+public:
+  ABIAnalysis(const GeneratedCodeBasicInfo &GCBI) :
+    ABIAnalysis(nullptr, GCBI){};
+
+  ABIAnalysis(const llvm::Instruction *CS, const GeneratedCodeBasicInfo &GCBI) :
+    RegisterList(), CallSite(CS) {
+
+    for (auto *CSV : GCBI.abiRegisters()) {
+      if (CSV) {
+        ABIRegisters.insert(CSV);
+        RegisterList.emplace_back(CSV);
+      }
+    }
+  };
+
+  const llvm::SmallVector<llvm::GlobalVariable *, 20> getRegisters() const {
+    return RegisterList;
+  }
+
+  bool isABIRegister(const llvm::Value *) const;
+
+  TransferKind classifyInstruction(const llvm::Instruction *) const;
+
+  llvm::SmallVector<const llvm::GlobalVariable *, 1>
+  getRegistersWritten(const llvm::Instruction *) const;
+
+  llvm::SmallVector<const llvm::GlobalVariable *, 1>
+  getRegistersRead(const llvm::Instruction *) const;
+};
+
+inline bool ABIAnalysis::isABIRegister(const llvm::Value *V) const {
+  if (auto *G = dyn_cast<llvm::GlobalVariable>(V)) {
+    return ABIRegisters.count(G) != 0;
+  }
+  return false;
+}
+
+inline bool isCallSiteBlock(const llvm::BasicBlock *B) {
+  if (auto *C = dyn_cast<llvm::CallInst>(&*B->getFirstInsertionPt())) {
+    if (C->getCalledFunction()->getName().contains("precall_hook")) {
+      return true;
+    }
+  }
+  return false;
+}
+
+inline const llvm::Instruction *getPreCallHook(const llvm::BasicBlock *B) {
+  if (isCallSiteBlock(B)) {
+    return &*B->getFirstInsertionPt();
+  }
+  return nullptr;
+}
+
+inline const llvm::Instruction *getPostCallHook(const llvm::BasicBlock *B) {
+  if (isCallSiteBlock(B)) {
+    return B->getTerminator()->getPrevNode();
+  }
+  return nullptr;
+}
+
+inline TransferKind
+ABIAnalysis::classifyInstruction(const llvm::Instruction *I) const {
+  using namespace llvm;
+
+  switch (I->getOpcode()) {
+  case Instruction::Store: {
+    auto *S = cast<StoreInst>(I);
+    if (isABIRegister(S->getPointerOperand())) {
+      return isCallSiteBlock(I->getParent()) ? WeakWrite : Write;
+    }
+    break;
+  }
+  case Instruction::Load: {
+    auto *L = cast<LoadInst>(I);
+    if (isABIRegister(L->getPointerOperand())) {
+      return Read;
+    }
+    break;
+  }
+  case Instruction::Call: {
+    if (I == CallSite) {
+      return TheCall;
+    }
+    break;
+  }
+  }
+  return None;
+}
+
+inline llvm::SmallVector<const llvm::GlobalVariable *, 1>
+ABIAnalysis::getRegistersWritten(const llvm::Instruction *I) const {
+  using namespace llvm;
+
+  SmallVector<const GlobalVariable *, 1> Result;
+  switch (I->getOpcode()) {
+  case Instruction::Store: {
+    auto *S = cast<StoreInst>(I);
+    auto *Pointer = S->getPointerOperand();
+    if (isABIRegister(Pointer)) {
+      Result.push_back(cast<GlobalVariable>(Pointer));
+    }
+    break;
+  }
+  }
+  return Result;
+}
+
+inline llvm::SmallVector<const llvm::GlobalVariable *, 1>
+ABIAnalysis::getRegistersRead(const llvm::Instruction *I) const {
+  using namespace llvm;
+
+  SmallVector<const GlobalVariable *, 1> Result;
+  switch (I->getOpcode()) {
+  case Instruction::Load: {
+    auto *L = cast<LoadInst>(I);
+    auto *Pointer = L->getPointerOperand();
+    if (isABIRegister(Pointer)) {
+      Result.push_back(cast<GlobalVariable>(Pointer));
+    }
+    break;
+  }
+  }
+  return Result;
+}
+
+template<typename CoreLattice>
+struct RegistersMap : public llvm::DenseMap<const llvm::GlobalVariable *,
+                                            typename CoreLattice::LatticeElement> {
+private:
+  using InnerLatticeElement = typename CoreLattice::LatticeElement;
+  using Base = llvm::DenseMap<const llvm::GlobalVariable *,
+                              InnerLatticeElement>;
+
+private:
+  InnerLatticeElement Default {};
+
+public:
+  RegistersMap() : Default {} {}
+  RegistersMap(InnerLatticeElement Default) : Default(Default) {}
+
+public:
+  InnerLatticeElement getOrDefault(const llvm::GlobalVariable *GV) const {
+    auto It = Base::find(GV);
+    if (It == Base::end())
+      return Default;
+    else
+      return It->second;
+  }
+
+public:
+  RegistersMap combine(const RegistersMap &RHS) const {
+    RegistersMap New = *this;
+    for (const auto &[Reg, S] : RHS) {
+      auto LHSValue = New.getOrDefault(Reg);
+      auto RHSValue = RHS.getOrDefault(Reg);
+      New[Reg] = CoreLattice::combineValues(LHSValue, RHSValue);
+    }
+
+    New.Default = CoreLattice::combineValues(New.Default, RHS.Default);
+
+    return New;
+  }
+
+  bool isLessOrEqual(const RegistersMap &RHS) const {
+    const RegistersMap &LHS = *this;
+
+    if (!CoreLattice::isLessOrEqual(LHS.Default, RHS.Default))
+      return false;
+
+    for (auto &[Reg, S] : LHS) {
+      auto LHSValue = LHS.getOrDefault(Reg);
+      auto RHSValue = RHS.getOrDefault(Reg);
+      if (!CoreLattice::isLessOrEqual(LHSValue, RHSValue)) {
+        return false;
+      }
+    }
+    for (auto &[Reg, S] : RHS) {
+      auto LHSValue = LHS.getOrDefault(Reg);
+      auto RHSValue = RHS.getOrDefault(Reg);
+      if (!CoreLattice::isLessOrEqual(LHSValue, RHSValue)) {
+        return false;
+      }
+    }
+    return true;
+  }
+};
+
+template<bool IsForward, typename CoreLattice>
+struct MFIAnalysis : ABIAnalyses::ABIAnalysis {
+  using LatticeElement = RegistersMap<CoreLattice>;
+  using Label = const llvm::BasicBlock *;
+  using GraphType = std::conditional_t<IsForward,
+                                       const llvm::BasicBlock *,
+                                       llvm::Inverse<const llvm::BasicBlock *>>;
+  using GT = llvm::GraphTraits<GraphType>;
+  using LGT = GraphType;
+
+  LatticeElement
+  combineValues(const LatticeElement &LHS, const LatticeElement &RHS) const {
+    return LHS.combine(RHS);
+  };
+
+  bool
+  isLessOrEqual(const LatticeElement &LHS, const LatticeElement &RHS) const {
+    return LHS.isLessOrEqual(RHS);
+  };
+
+  LatticeElement applyTransferFunction(Label L, const LatticeElement &E) const {
+    using namespace llvm;
+
+    LatticeElement New = E;
+    std::vector<const Instruction *> InsList;
+    for (auto &I : make_range(L->begin(), L->end())) {
+      InsList.push_back(&I);
+    }
+
+    for (size_t i = 0; i < InsList.size(); i++) {
+      auto I = InsList[IsForward ? i : (InsList.size() - i - 1)];
+      TransferKind T = classifyInstruction(I);
+      switch (T) {
+      case TheCall: {
+        for (auto &Reg : getRegisters()) {
+          auto RegState = New.getOrDefault(Reg);
+          New[Reg] = CoreLattice::transfer(TheCall, RegState);
+        }
+        break;
+      }
+      case Read:
+        for (auto &Reg : getRegistersRead(I)) {
+          auto RegState = New.getOrDefault(Reg);
+          New[Reg] = CoreLattice::transfer(T, RegState);
+        }
+        break;
+      case WeakWrite:
+      case Write:
+        for (auto &Reg : getRegistersWritten(I)) {
+          auto RegState = New.getOrDefault(Reg);
+          New[Reg] = CoreLattice::transfer(T, RegState);
+        }
+        break;
+      default:
+        break;
+      }
+    }
+    return New;
+  };
+};
+
+} // namespace ABIAnalyses
diff --git a/lib/StackAnalysis/ABIAnalyses/ABIAnalysis.cpp b/lib/StackAnalysis/ABIAnalyses/ABIAnalysis.cpp
new file mode 100644
index 000000000..b0289af24
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/ABIAnalysis.cpp
@@ -0,0 +1,342 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/InstIterator.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/Casting.h"
+#include "llvm/Support/raw_ostream.h"
+
+#include "revng/ABIAnalyses/Common.h"
+#include "revng/ADT/ZipMapIterator.h"
+#include "revng/Model/Binary.h"
+#include "revng/Support/Assert.h"
+#include "revng/Support/Debug.h"
+#include "revng/Support/IRHelpers.h"
+#include "revng/Support/MetaAddress.h"
+
+#include "ABIAnalysis.h"
+#include "Analyses.h"
+
+using namespace llvm;
+
+static Logger<> ABIAnalysesLog("abi-analyses");
+
+namespace ABIAnalyses {
+using RegisterState = model::RegisterState::Values;
+
+template void
+ABIAnalyses::ABIAnalysesResults::dump<Logger<true>>(Logger<true> &,
+                                                    const char *) const;
+
+struct PartialAnalysisResults {
+  // Per function analysis
+  RegisterStateMap UAOF;
+  RegisterStateMap DRAOF;
+
+  // Per call site analysis
+  std::map<std::pair<MetaAddress, BasicBlock *>, RegisterStateMap> URVOFC;
+  std::map<std::pair<MetaAddress, BasicBlock *>, RegisterStateMap> RAOFC;
+  std::map<std::pair<MetaAddress, BasicBlock *>, RegisterStateMap> DRVOFC;
+
+  // Per return analysis
+  std::map<std::pair<MetaAddress, BasicBlock *>, RegisterStateMap> URVOF;
+
+  // Debug methods
+  void dump() const debug_function { dump(dbg, ""); }
+
+  template<typename T>
+  void dump(T &Output, const char *Prefix) const;
+};
+
+// Print the analysis results
+template<typename T>
+void PartialAnalysisResults::dump(T &Output, const char *Prefix) const {
+  Output << Prefix << "UsedArgumentsOfFunction:\n";
+  for (auto &[GV, State] : UAOF) {
+    Output << Prefix << "  " << GV->getName().str() << " = "
+           << model::RegisterState::getName(State).str() << '\n';
+  }
+
+  Output << Prefix << "DeadRegisterArgumentsOfFunction:\n";
+  for (auto &[GV, State] : DRAOF) {
+    Output << Prefix << "  " << GV->getName().str() << " = "
+           << model::RegisterState::getName(State).str() << '\n';
+  }
+
+  Output << Prefix << "UsedReturnValuesOfFunctionCall:\n";
+  for (auto &[Key, StateMap] : URVOFC) {
+    Output << Prefix << "  " << Key.second->getName().str() << '\n';
+    for (auto &[GV, State] : StateMap) {
+      Output << Prefix << "    " << GV->getName().str() << " = "
+             << model::RegisterState::getName(State).str() << '\n';
+    }
+  }
+
+  Output << Prefix << "RegisterArgumentsOfFunctionCall:\n";
+  for (auto &[Key, StateMap] : RAOFC) {
+    Output << Prefix << "  " << Key.second->getName().str() << '\n';
+    for (auto &[GV, State] : StateMap) {
+      Output << Prefix << "    " << GV->getName().str() << " = "
+             << model::RegisterState::getName(State).str() << '\n';
+    }
+  }
+
+  Output << Prefix << "DeadReturnValuesOfFunctionCall:\n";
+  for (auto &[Key, StateMap] : DRVOFC) {
+    Output << Prefix << "  " << Key.second->getName().str() << '\n';
+    for (auto &[GV, State] : StateMap) {
+      Output << Prefix << "    " << GV->getName().str() << " = "
+             << model::RegisterState::getName(State).str() << '\n';
+    }
+  }
+
+  Output << Prefix << "UsedReturnValuesOfFunction:\n";
+  for (auto &[Key, StateMap] : URVOF) {
+    Output << Prefix << "  " << Key.second->getName().str() << '\n';
+    for (auto &[GV, State] : StateMap) {
+      Output << Prefix << "  " << GV->getName().str() << " = "
+             << model::RegisterState::getName(State).str() << '\n';
+    }
+  }
+}
+
+RegisterState combine(RegisterState LH, RegisterState RH) {
+  switch (LH) {
+  case RegisterState::Yes:
+    switch (RH) {
+    case RegisterState::Yes:
+    case RegisterState::YesOrDead:
+    case RegisterState::Maybe:
+      return RegisterState::Yes;
+    case RegisterState::No:
+    case RegisterState::NoOrDead:
+    case RegisterState::Dead:
+    case RegisterState::Contradiction:
+      return RegisterState::Contradiction;
+    case RegisterState::Count:
+    case RegisterState::Invalid:
+      revng_abort();
+    }
+    break;
+
+  case RegisterState::YesOrDead:
+    switch (RH) {
+    case RegisterState::Yes:
+      return RegisterState::Yes;
+    case RegisterState::Maybe:
+    case RegisterState::YesOrDead:
+      return RegisterState::YesOrDead;
+    case RegisterState::Dead:
+    case RegisterState::NoOrDead:
+      return RegisterState::Dead;
+    case RegisterState::No:
+    case RegisterState::Contradiction:
+      return RegisterState::Contradiction;
+    case RegisterState::Count:
+    case RegisterState::Invalid:
+      revng_abort();
+    }
+    break;
+
+  case RegisterState::No:
+    switch (RH) {
+    case RegisterState::No:
+    case RegisterState::NoOrDead:
+    case RegisterState::Maybe:
+      return RegisterState::No;
+    case RegisterState::Yes:
+    case RegisterState::YesOrDead:
+    case RegisterState::Dead:
+    case RegisterState::Contradiction:
+      return RegisterState::Contradiction;
+    case RegisterState::Count:
+    case RegisterState::Invalid:
+      revng_abort();
+    }
+    break;
+
+  case RegisterState::NoOrDead:
+    switch (RH) {
+    case RegisterState::No:
+      return RegisterState::No;
+    case RegisterState::Maybe:
+    case RegisterState::NoOrDead:
+      return RegisterState::NoOrDead;
+    case RegisterState::Dead:
+    case RegisterState::YesOrDead:
+      return RegisterState::Dead;
+    case RegisterState::Yes:
+    case RegisterState::Contradiction:
+      return RegisterState::Contradiction;
+    case RegisterState::Count:
+    case RegisterState::Invalid:
+      revng_abort();
+    }
+    break;
+
+  case RegisterState::Dead:
+    switch (RH) {
+    case RegisterState::Dead:
+    case RegisterState::Maybe:
+    case RegisterState::NoOrDead:
+    case RegisterState::YesOrDead:
+      return RegisterState::Dead;
+    case RegisterState::No:
+    case RegisterState::Yes:
+    case RegisterState::Contradiction:
+      return RegisterState::Contradiction;
+    case RegisterState::Count:
+    case RegisterState::Invalid:
+      revng_abort();
+    }
+    break;
+
+  case RegisterState::Maybe:
+    return RH;
+
+  case RegisterState::Contradiction:
+    return RegisterState::Contradiction;
+
+  case RegisterState::Count:
+  case RegisterState::Invalid:
+    revng_abort();
+  }
+}
+
+void finalizeReturnValues(ABIAnalysesResults &ABIResults) {
+  for (auto &[PC, RSMap] : ABIResults.ReturnValuesRegisters) {
+    for (auto &[CSV, RS] : RSMap) {
+      if (ABIResults.FinalReturnValuesRegisters.count(CSV) == 0)
+        ABIResults.FinalReturnValuesRegisters[CSV] = RegisterState::Maybe;
+
+      ABIResults.FinalReturnValuesRegisters
+        [CSV] = combine(ABIResults.FinalReturnValuesRegisters[CSV], RS);
+    }
+  }
+}
+
+// Run the ABI analyses on the outlined function F. This function must have all
+// the original function calls replaced with a basic block starting with a call
+// to `precall_hook` followed by a summary of the side effects of the function
+// followed by a call to `postcall_hook` and a basic block terminating
+// instruction.
+ABIAnalysesResults analyzeOutlinedFunction(Function *F,
+                                           const GeneratedCodeBasicInfo &GCBI,
+                                           Function *PreCallSiteHook,
+                                           Function *PostCallSiteHook) {
+  namespace UAOF = UsedArgumentsOfFunction;
+  namespace DRAOF = DeadRegisterArgumentsOfFunction;
+  namespace RAOFC = RegisterArgumentsOfFunctionCall;
+  namespace URVOFC = UsedReturnValuesOfFunctionCall;
+  namespace DRVOFC = DeadReturnValuesOfFunctionCall;
+  namespace URVOF = UsedReturnValuesOfFunction;
+
+  ABIAnalysesResults FinalResults;
+  PartialAnalysisResults Results;
+
+  // Initial population of partial results
+  Results.UAOF = UAOF::analyze(&F->getEntryBlock(), GCBI);
+  Results.DRAOF = DRAOF::analyze(&F->getEntryBlock(), GCBI);
+  for (auto &I : instructions(F)) {
+    BasicBlock *BB = I.getParent();
+
+    if (auto *Call = dyn_cast<CallInst>(&I)) {
+      MetaAddress PC;
+      if (isCallTo(Call, PreCallSiteHook) || isCallTo(Call, PostCallSiteHook))
+        PC = MetaAddress::fromConstant(Call->getArgOperand(0));
+
+      if (isCallTo(Call, PreCallSiteHook)) {
+        Results.RAOFC[{ PC, BB }] = RAOFC::analyze(BB, GCBI);
+      } else if (isCallTo(Call, PostCallSiteHook)) {
+        Results.URVOFC[{ PC, BB }] = URVOFC::analyze(BB, GCBI);
+        Results.DRVOFC[{ PC, BB }] = DRVOFC::analyze(BB, GCBI);
+      } else if (auto *R = dyn_cast<ReturnInst>(&I)) {
+        Results.URVOF[{ PC, BB }] = URVOF::analyze(BB, GCBI);
+      }
+    }
+  }
+
+  if (ABIAnalysesLog.isEnabled()) {
+    ABIAnalysesLog << "Dumping ABIAnalyses results for function "
+                   << F->getName() << ": \n";
+    Results.dump();
+  }
+
+  // Finalize results. Combine UAOF and DRAOF.
+  for (auto &[Left, Right] : zipmap_range(Results.UAOF, Results.DRAOF)) {
+    auto *CSV = Left == nullptr ? Right->first : Left->first;
+    RegisterState LV = Left == nullptr ? RegisterState::Maybe : Left->second;
+    RegisterState RV = Right == nullptr ? RegisterState::Maybe : Right->second;
+    FinalResults.ArgumentsRegisters[CSV] = combine(LV, RV);
+  }
+
+  // Add RAOFC.
+  for (auto &[Key, RSMap] : Results.RAOFC) {
+    auto PC = Key.first;
+    FinalResults.CallSites[PC] = ABIAnalysesResults::CallSiteResults();
+    for (auto &[CSV, RS] : RSMap)
+      FinalResults.CallSites[PC].ArgumentsRegisters[CSV] = RS;
+  }
+
+  // Combine URVOFC and DRVOFC.
+  for (auto &[Key, _] : Results.URVOFC) {
+    auto PC = Key.first;
+    for (auto &[Left, Right] :
+         zipmap_range(Results.URVOFC[Key], Results.DRVOFC[Key])) {
+      auto *CSV = Left == nullptr ? Right->first : Left->first;
+      RegisterState LV = Left == nullptr ? RegisterState::Maybe : Left->second;
+      RegisterState RV = Right == nullptr ? RegisterState::Maybe :
+                                            Right->second;
+      FinalResults.CallSites[PC].ReturnValuesRegisters[CSV] = combine(LV, RV);
+    }
+  }
+
+  // Add URVOF.
+  for (auto &[Key, RSMap] : Results.URVOF) {
+    auto PC = Key.first;
+    for (auto &[CSV, RS] : RSMap)
+      FinalResults.ReturnValuesRegisters[PC][CSV] = RS;
+  }
+
+  return FinalResults;
+}
+
+template<typename T>
+void ABIAnalysesResults::dump(T &Output, const char *Prefix) const {
+  Output << Prefix << "Arguments:\n";
+  for (auto &[GV, State] : ArgumentsRegisters) {
+    Output << Prefix << "  " << GV->getName().str() << " = "
+           << model::RegisterState::getName(State).str() << '\n';
+  }
+
+  Output << Prefix << "Call site:\n";
+  for (auto &[PC, StateMap] : CallSites) {
+    Output << Prefix << "  " << PC.address() << '\n';
+    Output << Prefix << "  "
+           << "  "
+           << "Arguments:\n";
+    for (auto &[GV, State] : StateMap.ArgumentsRegisters) {
+      Output << Prefix << "    " << GV->getName().str() << " = "
+             << model::RegisterState::getName(State).str() << '\n';
+    }
+    Output << Prefix << "  "
+           << "  "
+           << "Return values:\n";
+    for (auto &[GV, State] : StateMap.ReturnValuesRegisters) {
+      Output << Prefix << "    " << GV->getName().str() << " = "
+             << model::RegisterState::getName(State).str() << '\n';
+    }
+  }
+
+  Output << Prefix << "Return values:\n";
+  for (auto &[GV, State] : FinalReturnValuesRegisters) {
+    Output << Prefix << "  " << GV->getName().str() << " = "
+           << model::RegisterState::getName(State).str() << '\n';
+  }
+}
+
+} // namespace ABIAnalyses
diff --git a/lib/StackAnalysis/ABIAnalyses/ABIAnalysis.h b/lib/StackAnalysis/ABIAnalyses/ABIAnalysis.h
new file mode 100644
index 000000000..81c98d2fa
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/ABIAnalysis.h
@@ -0,0 +1,60 @@
+#pragma once
+
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/IR/Function.h"
+#include "llvm/IR/InstIterator.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/Casting.h"
+#include "llvm/Support/raw_ostream.h"
+
+#include "revng/BasicAnalyses/GeneratedCodeBasicInfo.h"
+#include "revng/Model/Binary.h"
+#include "revng/Support/Debug.h"
+#include "revng/Support/MetaAddress.h"
+
+namespace ABIAnalyses {
+
+using RegisterStateMap = std::map<const llvm::GlobalVariable *,
+                                  model::RegisterState::Values>;
+
+struct ABIAnalysesResults {
+  // Per function analysis
+  RegisterStateMap ArgumentsRegisters;
+
+  // Per call site analysis
+  struct CallSiteResults {
+    RegisterStateMap ArgumentsRegisters;
+    RegisterStateMap ReturnValuesRegisters;
+  };
+  std::map<MetaAddress, CallSiteResults> CallSites;
+
+  // Per return analysis
+  std::map<MetaAddress, RegisterStateMap> ReturnValuesRegisters;
+  RegisterStateMap FinalReturnValuesRegisters;
+
+  // Debug methods
+  void dump() const debug_function { dump(dbg, ""); }
+
+  template<typename T>
+  void dump(T &Output, const char *Prefix = "") const;
+};
+
+extern template void
+ABIAnalyses::ABIAnalysesResults::dump<Logger<true>>(Logger<true> &,
+                                                    const char *) const;
+
+model::RegisterState::Values
+  combine(model::RegisterState::Values, model::RegisterState::Values);
+
+ABIAnalysesResults analyzeOutlinedFunction(llvm::Function *F,
+                                           const GeneratedCodeBasicInfo &,
+                                           llvm::Function *,
+                                           llvm::Function *);
+
+void finalizeReturnValues(ABIAnalysesResults &);
+
+} // namespace ABIAnalyses
diff --git a/lib/StackAnalysis/ABIAnalyses/Analyses.h b/lib/StackAnalysis/ABIAnalyses/Analyses.h
new file mode 100644
index 000000000..b7f54a968
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/Analyses.h
@@ -0,0 +1,64 @@
+#pragma once
+
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "revng/Model/Binary.h"
+
+#include "MFIGraphs/DeadRegisterArgumentsOfFunction.h"
+#include "MFIGraphs/DeadReturnValuesOfFunctionCall.h"
+#include "MFIGraphs/RegisterArgumentsOfFunctionCall.h"
+#include "MFIGraphs/UsedArgumentsOfFunction.h"
+#include "MFIGraphs/UsedReturnValuesOfFunction.h"
+#include "MFIGraphs/UsedReturnValuesOfFunctionCall.h"
+
+namespace ABIAnalyses {
+
+namespace DeadRegisterArgumentsOfFunction {
+using namespace llvm;
+
+std::map<const GlobalVariable *, model::RegisterState::Values>
+analyze(const BasicBlock *FunctionEntry, const GeneratedCodeBasicInfo &GCBI);
+
+} // namespace DeadRegisterArgumentsOfFunction
+
+namespace DeadReturnValuesOfFunctionCall {
+using namespace llvm;
+
+std::map<const GlobalVariable *, model::RegisterState::Values>
+analyze(const BasicBlock *CallSiteBlock, const GeneratedCodeBasicInfo &GCBI);
+
+} // namespace DeadReturnValuesOfFunctionCall
+
+namespace RegisterArgumentsOfFunctionCall {
+using namespace llvm;
+
+std::map<const GlobalVariable *, model::RegisterState::Values>
+analyze(const BasicBlock *CallSiteBlock, const GeneratedCodeBasicInfo &GCBI);
+
+} // namespace RegisterArgumentsOfFunctionCall
+
+namespace UsedArgumentsOfFunction {
+using namespace llvm;
+
+std::map<const GlobalVariable *, model::RegisterState::Values>
+analyze(const BasicBlock *FunctionEntry, const GeneratedCodeBasicInfo &GCBI);
+
+} // namespace UsedArgumentsOfFunction
+
+namespace UsedReturnValuesOfFunction {
+using namespace llvm;
+
+std::map<const GlobalVariable *, model::RegisterState::Values>
+analyze(const BasicBlock *ReturnBlock, const GeneratedCodeBasicInfo &GCBI);
+} // namespace UsedReturnValuesOfFunction
+
+namespace UsedReturnValuesOfFunctionCall {
+using namespace llvm;
+
+std::map<const GlobalVariable *, model::RegisterState::Values>
+analyze(const BasicBlock *CallSiteBlock, const GeneratedCodeBasicInfo &GCBI);
+} // namespace UsedReturnValuesOfFunctionCall
+
+} // namespace ABIAnalyses
diff --git a/lib/StackAnalysis/ABIAnalyses/CMakeLists.txt b/lib/StackAnalysis/ABIAnalyses/CMakeLists.txt
new file mode 100644
index 000000000..febc8f4a6
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/CMakeLists.txt
@@ -0,0 +1,24 @@
+#
+# This file is distributed under the MIT License. See LICENSE.md for details.
+#
+add_subdirectory(MFIGraphs)
+
+revng_add_analyses_library_internal(revngABIAnalyses
+  ABIAnalysis.cpp
+  DeadRegisterArgumentsOfFunction.cpp
+  DeadReturnValuesOfFunctionCall.cpp
+  RegisterArgumentsOfFunctionCall.cpp
+  UsedArgumentsOfFunction.cpp
+  UsedReturnValuesOfFunction.cpp
+  UsedReturnValuesOfFunctionCall.cpp)
+
+target_link_libraries(revngABIAnalyses
+  revngSupport
+  revngBasicAnalyses
+  revngModel)
+
+target_include_directories(revngABIAnalyses
+  PRIVATE
+  "${CMAKE_CURRENT_BINARY_DIR}")
+
+add_dependencies(revngABIAnalyses abi-analyses-headers)
diff --git a/lib/StackAnalysis/ABIAnalyses/DeadRegisterArgumentsOfFunction.cpp b/lib/StackAnalysis/ABIAnalyses/DeadRegisterArgumentsOfFunction.cpp
new file mode 100644
index 000000000..630a19ecf
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/DeadRegisterArgumentsOfFunction.cpp
@@ -0,0 +1,60 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/GraphTraits.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/iterator_range.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/GlobalVariable.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/Casting.h"
+
+#include "revng/MFP/MFP.h"
+#include "revng/Support/revng.h"
+
+#include "Analyses.h"
+
+namespace ABIAnalyses::DeadRegisterArgumentsOfFunction {
+using namespace llvm;
+using namespace ABIAnalyses;
+
+std::map<const GlobalVariable *, State>
+analyze(const BasicBlock *FunctionEntry, const GeneratedCodeBasicInfo &GCBI) {
+  using MFI = MFIAnalysis<true, CoreLattice>;
+
+  MFI Instance{ { GCBI } };
+  MFI::LatticeElement InitialValue;
+  MFI::LatticeElement ExtremalValue(CoreLattice::ExtremalLatticeElement);
+
+  auto
+    Res = MFP::getMaximalFixedPoint<MFI, MFI::GT, MFI::LGT>(Instance,
+                                                            FunctionEntry,
+                                                            InitialValue,
+                                                            ExtremalValue,
+                                                            { FunctionEntry },
+                                                            { FunctionEntry });
+
+  DenseSet<const GlobalVariable *> RegUnknown{};
+  std::map<const GlobalVariable *, State> RegNoOrDead{};
+
+  for (auto &[BB, Result] : Res) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::Unknown) {
+        RegUnknown.insert(GV);
+      }
+    }
+  }
+
+  for (auto &[BB, Result] : Res) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::NoOrDead && RegUnknown.count(GV) == 0) {
+        RegNoOrDead[GV] = State::NoOrDead;
+      }
+    }
+  }
+  return RegNoOrDead;
+}
+} // namespace ABIAnalyses::DeadRegisterArgumentsOfFunction
diff --git a/lib/StackAnalysis/ABIAnalyses/DeadReturnValuesOfFunctionCall.cpp b/lib/StackAnalysis/ABIAnalyses/DeadReturnValuesOfFunctionCall.cpp
new file mode 100644
index 000000000..e4e3353b5
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/DeadReturnValuesOfFunctionCall.cpp
@@ -0,0 +1,56 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/GraphTraits.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/iterator_range.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/GlobalVariable.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/Casting.h"
+
+#include "revng/MFP/MFP.h"
+#include "revng/Model/Binary.h"
+#include "revng/Support/revng.h"
+
+#include "Analyses.h"
+
+namespace ABIAnalyses::DeadReturnValuesOfFunctionCall {
+using namespace llvm;
+using namespace ABIAnalyses;
+
+std::map<const GlobalVariable *, State>
+analyze(const BasicBlock *CallSiteBlock, const GeneratedCodeBasicInfo &GCBI) {
+  using MFI = MFIAnalysis<true, CoreLattice>;
+
+  std::map<const GlobalVariable *, State> RegNoOrDead{};
+  MFI Instance{ { getPreCallHook(CallSiteBlock), GCBI } };
+  MFI::LatticeElement InitialValue;
+  MFI::LatticeElement ExtremalValue(CoreLattice::ExtremalLatticeElement);
+  auto *Start = CallSiteBlock->getUniqueSuccessor();
+
+  if (!Start)
+    return RegNoOrDead;
+
+  auto
+    Results = MFP::getMaximalFixedPoint<MFI, MFI::GT, MFI::LGT>(Instance,
+                                                                Start,
+                                                                InitialValue,
+                                                                ExtremalValue,
+                                                                { Start },
+                                                                { Start });
+
+  for (auto &[BB, Result] : Results) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::NoOrDead) {
+        RegNoOrDead[GV] = State::NoOrDead;
+      }
+    }
+  }
+  return RegNoOrDead;
+}
+} // namespace ABIAnalyses::DeadReturnValuesOfFunctionCall
diff --git a/lib/StackAnalysis/ABIAnalyses/MFIGraphs/ABIAnalysis.template b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/ABIAnalysis.template
new file mode 100644
index 000000000..cbb3cfa38
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/ABIAnalysis.template
@@ -0,0 +1,43 @@
+#pragma once
+
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+// This file has been automatically generated from scripts/monotone_framework_lattice.py, please don't change it
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Value.h"
+
+#include "revng/ABIAnalyses/Common.h"
+#include "revng/BasicAnalyses/GeneratedCodeBasicInfo.h"
+#include "revng/MFP/MFP.h"
+#include "revng/Model/Binary.h"
+#include "revng/StackAnalysis/StackAnalysis.h"
+#include "revng/Support/revng.h"
+
+namespace ABIAnalyses::%LatticeName% {
+
+using namespace ABIAnalyses;
+using Register = model::Register::Values;
+using State = model::RegisterState::Values;
+
+struct CoreLattice {
+
+%LatticeElement%
+
+static const LatticeElement ExtremalLatticeElement = %ExtremalLatticeElement%;
+
+using TransferFunction = ABIAnalyses::TransferKind;
+
+static %isLessOrEqual%
+
+static %combineValues%
+
+static %transfer%
+
+};
+
+} // namespace ABIAnalyses::%LatticeName%
diff --git a/lib/StackAnalysis/ABIAnalyses/MFIGraphs/CMakeLists.txt b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/CMakeLists.txt
new file mode 100644
index 000000000..1d7f61bbe
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/CMakeLists.txt
@@ -0,0 +1,31 @@
+#
+# This file is distributed under the MIT License. See LICENSE.md for details.
+#
+
+# Code generation requirements
+
+
+# Generate headers for ABI analyses
+set(ABIANALYSIS_TEMPLATE
+  "${CMAKE_CURRENT_SOURCE_DIR}/ABIAnalysis.template")
+
+set(ABIANALYSIS_GRAPHS
+  "DeadRegisterArgumentsOfFunction"
+  "DeadReturnValuesOfFunctionCall"
+  "RegisterArgumentsOfFunctionCall"
+  "UsedArgumentsOfFunction"
+  "UsedReturnValuesOfFunctionCall"
+  "UsedReturnValuesOfFunction")
+
+foreach(GRAPH IN LISTS ABIANALYSIS_GRAPHS)
+  add_custom_command(OUTPUT "${GRAPH}.h"
+    COMMAND "${CMAKE_SOURCE_DIR}/scripts/monotone_framework_lattice.py"
+      ${ABIANALYSIS_TEMPLATE} "${CMAKE_CURRENT_SOURCE_DIR}/${GRAPH}.dot" > "${GRAPH}.h"
+    DEPENDS "${CMAKE_SOURCE_DIR}/scripts/monotone_framework_lattice.py"
+            "${CMAKE_CURRENT_SOURCE_DIR}/${GRAPH}.dot"
+            ${ABIANALYSIS_TEMPLATE}
+    VERBATIM)
+    list(APPEND ABIANALYSIS_HEADERS "${GRAPH}.h")
+endforeach()
+
+add_custom_target(abi-analyses-headers DEPENDS ${ABIANALYSIS_HEADERS})
diff --git a/lib/StackAnalysis/ABIAnalyses/MFIGraphs/DeadRegisterArgumentsOfFunction.dot b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/DeadRegisterArgumentsOfFunction.dot
new file mode 100644
index 000000000..c6fe8f587
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/DeadRegisterArgumentsOfFunction.dot
@@ -0,0 +1,20 @@
+#
+# This file is distributed under the MIT License. See LICENSE.md for details.
+#
+
+digraph DeadRegisterArgumentsOfFunction {
+  NoOrDead;
+  Maybe [peripheries=2];
+  Unknown;
+
+  # Lattice
+  NoOrDead->Maybe;
+  Maybe->Unknown;
+
+  # Transfer functions
+  Maybe->NoOrDead [label="Write"];
+  Maybe->NoOrDead [label="WeakWrite"];
+  Maybe->Unknown [label="Read"];
+
+  Maybe->Maybe [label="None"];
+}
diff --git a/lib/StackAnalysis/ABIAnalyses/MFIGraphs/DeadReturnValuesOfFunctionCall.dot b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/DeadReturnValuesOfFunctionCall.dot
new file mode 100644
index 000000000..475f66b08
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/DeadReturnValuesOfFunctionCall.dot
@@ -0,0 +1,21 @@
+#
+# This file is distributed under the MIT License. See LICENSE.md for details.
+#
+
+digraph DeadReturnValuesOfFunctionCall {
+  NoOrDead;
+  Maybe [peripheries=2];
+  Unknown;
+
+  # Lattice
+  NoOrDead->Maybe;
+  Maybe->Unknown;
+
+  # Transfer functions
+  Maybe->NoOrDead [label="Write"];
+  Maybe->NoOrDead [label="WeakWrite"];
+  Maybe->Unknown [label="Read"];
+  Maybe->Unknown [label="TheCall"];
+
+  Maybe->Maybe [label="None"];
+}
diff --git a/lib/StackAnalysis/ABIAnalyses/MFIGraphs/RegisterArgumentsOfFunctionCall.dot b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/RegisterArgumentsOfFunctionCall.dot
new file mode 100644
index 000000000..c74a0830d
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/RegisterArgumentsOfFunctionCall.dot
@@ -0,0 +1,27 @@
+#
+# This file is distributed under the MIT License. See LICENSE.md for details.
+#
+
+digraph RegisterArgumentsOfFunctionCall {
+  Bottom;
+  Maybe [peripheries=2];
+  Yes;
+  Unknown;
+
+  # Lattice
+  Bottom->Yes;
+  Bottom->Maybe;
+  Yes->Unknown;
+  Maybe->Unknown;
+
+  # Transfer functions
+  Maybe->Yes [label="Write"];
+  Maybe->Unknown [label="Read"];
+  Maybe->Unknown [label="TheCall"];
+
+  # Prevent return values to become arguments right away
+  Maybe->Maybe [label="WeakWrite"];
+
+  Maybe->Maybe [label="None"];
+
+}
diff --git a/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedArgumentsOfFunction.dot b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedArgumentsOfFunction.dot
new file mode 100644
index 000000000..4fe3d705f
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedArgumentsOfFunction.dot
@@ -0,0 +1,23 @@
+#
+# This file is distributed under the MIT License. See LICENSE.md for details.
+#
+
+# This analysis works both for registers and stack slots
+
+digraph UsedArgumentsOfFunction {
+  Unknown;
+  Maybe [peripheries=2];
+  Yes;
+
+  # Lattice
+  Unknown->Maybe;
+  Maybe->Yes;
+
+  # Transfer functions
+  Maybe->Yes [label="Read"];
+  Maybe->Unknown [label="Write"];
+  Maybe->Unknown [label="WeakWrite"];
+
+  Maybe->Maybe [label="None"];
+
+}
diff --git a/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedReturnValuesOfFunction.dot b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedReturnValuesOfFunction.dot
new file mode 100644
index 000000000..6e9b42353
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedReturnValuesOfFunction.dot
@@ -0,0 +1,23 @@
+#
+# This file is distributed under the MIT License. See LICENSE.md for details.
+#
+
+digraph UsedReturnValuesOfFunction {
+  Bottom;
+  Maybe [peripheries=2];
+  YesOrDead;
+  Unknown;
+
+  # Lattice
+  Bottom->YesOrDead;
+  Bottom->Maybe;
+  YesOrDead->Unknown;
+  Maybe->Unknown;
+
+  # Transfer functions
+  Maybe->YesOrDead [label="Write"];
+  Maybe->Unknown [label="Read"];
+  Maybe->Unknown [label="WeakWrite"];
+  Maybe->Maybe [label="None"];
+
+}
diff --git a/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedReturnValuesOfFunctionCall.dot b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedReturnValuesOfFunctionCall.dot
new file mode 100644
index 000000000..554863c2b
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/MFIGraphs/UsedReturnValuesOfFunctionCall.dot
@@ -0,0 +1,22 @@
+#
+# This file is distributed under the MIT License. See LICENSE.md for details.
+#
+
+digraph UsedReturnValuesOfFunctionCall {
+  Unknown;
+  Maybe [peripheries=2];
+  Yes;
+
+  # Lattice
+  Unknown->Maybe;
+  Maybe->Yes;
+
+  # Transfer functions
+  Maybe->Yes [label="Read"];
+  Maybe->Unknown [label="Write"];
+  Maybe->Unknown [label="WeakWrite"];
+  Maybe->Unknown [label="TheCall"];
+
+  Maybe->Maybe [label="None"];
+
+}
diff --git a/lib/StackAnalysis/ABIAnalyses/RegisterArgumentsOfFunctionCall.cpp b/lib/StackAnalysis/ABIAnalyses/RegisterArgumentsOfFunctionCall.cpp
new file mode 100644
index 000000000..37343b561
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/RegisterArgumentsOfFunctionCall.cpp
@@ -0,0 +1,64 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseSet.h"
+#include "llvm/ADT/GraphTraits.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/iterator_range.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/GlobalVariable.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/Casting.h"
+
+#include "revng/MFP/MFP.h"
+#include "revng/Support/revng.h"
+
+#include "Analyses.h"
+
+namespace ABIAnalyses::RegisterArgumentsOfFunctionCall {
+using namespace llvm;
+using namespace ABIAnalyses;
+
+std::map<const GlobalVariable *, State>
+analyze(const BasicBlock *CallSiteBlock, const GeneratedCodeBasicInfo &GCBI) {
+  using MFI = MFIAnalysis<false, CoreLattice>;
+
+  MFI Instance{ { getPostCallHook(CallSiteBlock), GCBI } };
+  MFI::LatticeElement InitialValue;
+  MFI::LatticeElement ExtremalValue(CoreLattice::ExtremalLatticeElement);
+
+  auto *Start = CallSiteBlock->getUniquePredecessor();
+  auto
+    Results = MFP::getMaximalFixedPoint<MFI, MFI::GT, MFI::LGT>(Instance,
+                                                                Start,
+                                                                InitialValue,
+                                                                ExtremalValue,
+                                                                { Start },
+                                                                { Start });
+
+  DenseSet<const GlobalVariable *> RegUnknown{};
+  std::map<const GlobalVariable *, State> RegYes{};
+
+  for (auto &[BB, Result] : Results) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::Unknown) {
+        RegUnknown.insert(GV);
+      }
+    }
+  }
+
+  for (auto &[BB, Result] : Results) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::Yes && RegUnknown.count(GV) == 0) {
+        RegYes[GV] = State::Yes;
+      }
+    }
+  }
+
+  return RegYes;
+}
+} // namespace ABIAnalyses::RegisterArgumentsOfFunctionCall
diff --git a/lib/StackAnalysis/ABIAnalyses/UsedArgumentsOfFunction.cpp b/lib/StackAnalysis/ABIAnalyses/UsedArgumentsOfFunction.cpp
new file mode 100644
index 000000000..de8125d8c
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/UsedArgumentsOfFunction.cpp
@@ -0,0 +1,52 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/GraphTraits.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/iterator_range.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/GlobalVariable.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/Casting.h"
+
+#include "revng/MFP/MFP.h"
+#include "revng/Support/revng.h"
+
+#include "Analyses.h"
+
+namespace ABIAnalyses::UsedArgumentsOfFunction {
+using namespace llvm;
+using namespace ABIAnalyses;
+
+std::map<const GlobalVariable *, State>
+analyze(const BasicBlock *FunctionEntry, const GeneratedCodeBasicInfo &GCBI) {
+  using MFI = MFIAnalysis<true, CoreLattice>;
+  MFI Instance{ { GCBI } };
+  MFI::LatticeElement InitialValue;
+  MFI::LatticeElement ExtremalValue(CoreLattice::ExtremalLatticeElement);
+
+  auto
+    Res = MFP::getMaximalFixedPoint<MFI, MFI::GT, MFI::LGT>(Instance,
+                                                            FunctionEntry,
+                                                            InitialValue,
+                                                            ExtremalValue,
+                                                            { FunctionEntry },
+                                                            { FunctionEntry });
+
+  std::map<const GlobalVariable *, State> RegYes{};
+
+  for (auto &[BB, Result] : Res) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::Yes) {
+        RegYes[GV] = State::Yes;
+      }
+    }
+  }
+
+  return RegYes;
+}
+} // namespace ABIAnalyses::UsedArgumentsOfFunction
diff --git a/lib/StackAnalysis/ABIAnalyses/UsedReturnValuesOfFunction.cpp b/lib/StackAnalysis/ABIAnalyses/UsedReturnValuesOfFunction.cpp
new file mode 100644
index 000000000..2f0700087
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/UsedReturnValuesOfFunction.cpp
@@ -0,0 +1,61 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/GraphTraits.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/iterator_range.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/GlobalVariable.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/Casting.h"
+
+#include "revng/MFP/MFP.h"
+#include "revng/Support/revng.h"
+
+#include "Analyses.h"
+
+namespace ABIAnalyses::UsedReturnValuesOfFunction {
+using namespace llvm;
+using namespace ABIAnalyses;
+
+std::map<const GlobalVariable *, State>
+analyze(const BasicBlock *ReturnBlock, const GeneratedCodeBasicInfo &GCBI) {
+  using MFI = MFIAnalysis<false, CoreLattice>;
+
+  MFI Instance{ { GCBI } };
+  MFI::LatticeElement InitialValue;
+  MFI::LatticeElement ExtremalValue(CoreLattice::ExtremalLatticeElement);
+
+  auto Res = MFP::getMaximalFixedPoint<MFI, MFI::GT, MFI::LGT>(Instance,
+                                                               ReturnBlock,
+                                                               InitialValue,
+                                                               ExtremalValue,
+                                                               { ReturnBlock },
+                                                               { ReturnBlock });
+
+  DenseSet<const GlobalVariable *> RegUnknown{};
+  std::map<const GlobalVariable *, State> RegYesOrDead{};
+
+  for (auto &[BB, Result] : Res) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::Unknown) {
+        RegUnknown.insert(GV);
+      }
+    }
+  }
+
+  for (auto &[BB, Result] : Res) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::YesOrDead && RegUnknown.count(GV) == 0) {
+        RegYesOrDead[GV] = State::YesOrDead;
+      }
+    }
+  }
+
+  return RegYesOrDead;
+}
+} // namespace ABIAnalyses::UsedReturnValuesOfFunction
diff --git a/lib/StackAnalysis/ABIAnalyses/UsedReturnValuesOfFunctionCall.cpp b/lib/StackAnalysis/ABIAnalyses/UsedReturnValuesOfFunctionCall.cpp
new file mode 100644
index 000000000..92cce9372
--- /dev/null
+++ b/lib/StackAnalysis/ABIAnalyses/UsedReturnValuesOfFunctionCall.cpp
@@ -0,0 +1,55 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/GraphTraits.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/iterator_range.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/GlobalVariable.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/Casting.h"
+
+#include "revng/MFP/MFP.h"
+#include "revng/Support/revng.h"
+
+#include "Analyses.h"
+
+namespace ABIAnalyses::UsedReturnValuesOfFunctionCall {
+using namespace llvm;
+using namespace ABIAnalyses;
+
+std::map<const GlobalVariable *, State>
+analyze(const BasicBlock *CallSiteBlock, const GeneratedCodeBasicInfo &GCBI) {
+  using MFI = MFIAnalysis<true, CoreLattice>;
+
+  std::map<const GlobalVariable *, State> RegYes{};
+  MFI Instance{ { getPreCallHook(CallSiteBlock), GCBI } };
+  MFI::LatticeElement InitialValue;
+  MFI::LatticeElement ExtremalValue(CoreLattice::ExtremalLatticeElement);
+  auto *Start = CallSiteBlock->getUniqueSuccessor();
+
+  if (!Start)
+    return RegYes;
+
+  auto
+    Results = MFP::getMaximalFixedPoint<MFI, MFI::GT, MFI::LGT>(Instance,
+                                                                Start,
+                                                                InitialValue,
+                                                                ExtremalValue,
+                                                                { Start },
+                                                                { Start });
+
+  for (auto &[BB, Result] : Results) {
+    for (auto &[GV, RegState] : Result.OutValue) {
+      if (RegState == CoreLattice::Yes) {
+        RegYes[GV] = State::Yes;
+      }
+    }
+  }
+  return RegYes;
+}
+} // namespace ABIAnalyses::UsedReturnValuesOfFunctionCall
diff --git a/lib/StackAnalysis/CMakeLists.txt b/lib/StackAnalysis/CMakeLists.txt
index 2aea78c8f..6053eff7b 100644
--- a/lib/StackAnalysis/CMakeLists.txt
+++ b/lib/StackAnalysis/CMakeLists.txt
@@ -2,31 +2,6 @@
 # This file is distributed under the MIT License. See LICENSE.md for details.
 #
 
-# Check if graph_tool is available
-execute_process(COMMAND python3 -c "import pygraphviz"
-  RESULT_VARIABLE HAS_PYGRAPHVIZ
-  OUTPUT_VARIABLE PYGRAPHVIZ_OUTPUT
-  ERROR_VARIABLE PYGRAPHVIZ_OUTPUT)
-
-if(NOT HAS_PYGRAPHVIZ EQUAL "0")
-  # Don't drop the whitespaces
-  message(FATAL_ERROR "  
-  Cannot find the pygraphviz module: ABIDataFlows.h cannot be generated.
-  Please try one of the following commands:
-  
-  Debian/Ubuntu:
-    apt-get install python3-pygraphviz
-  
-  Fedora/Red Hat/CentOS:
-    yum install python3-pygraphviz
-  
-  pip (current user only):
-    pip3 install --user pygraphviz
-  
-  In case of successful installation, the following command should succeed with no output:
-    python3 -c 'import pygraphviz'")
-endif()
-
 # Generate classes for the ABI data flow analyses
 set(ABIDATAFLOWS_SOURCES
   "${CMAKE_CURRENT_SOURCE_DIR}/ABIDataFlows-header.inc"
@@ -37,13 +12,15 @@ set(ABIDATAFLOWS_SOURCES
   "${CMAKE_CURRENT_SOURCE_DIR}/UsedReturnValuesOfFunctionCall.dot"
   "${CMAKE_CURRENT_SOURCE_DIR}/UsedReturnValuesOfFunction.dot")
 add_custom_command(OUTPUT ABIDataFlows.h
-  COMMAND "${CMAKE_SOURCE_DIR}/scripts/monotone-framework.py"
+  COMMAND "${CMAKE_SOURCE_DIR}/scripts/monotone_framework.py"
     --call-arcs ${ABIDATAFLOWS_SOURCES} > ABIDataFlows.h
-  DEPENDS "${CMAKE_SOURCE_DIR}/scripts/monotone-framework.py"
+  DEPENDS "${CMAKE_SOURCE_DIR}/scripts/monotone_framework.py"
            ${ABIDATAFLOWS_SOURCES}
   VERBATIM)
 add_custom_target(abidataflows DEPENDS ABIDataFlows.h)
 
+add_subdirectory(ABIAnalyses)
+
 revng_add_analyses_library_internal(revngStackAnalysis
   AAWriterPass.cpp
   ABI.cpp
@@ -65,6 +42,7 @@ llvm_map_components_to_libnames(LLVM_LIBRARIES Analysis)
 
 target_link_libraries(revngStackAnalysis
   revngBasicAnalyses
+  revngABIAnalyses
   revngSupport
   revngModel
   ${LLVM_LIBRARIES})
diff --git a/lib/StackAnalysis/StackAnalysis.cpp b/lib/StackAnalysis/StackAnalysis.cpp
index e596dcfec..a584cddf1 100644
--- a/lib/StackAnalysis/StackAnalysis.cpp
+++ b/lib/StackAnalysis/StackAnalysis.cpp
@@ -58,6 +58,7 @@
 #include "revng/Support/IRHelpers.h"
 #include "revng/Support/MetaAddress.h"
 
+#include "ABIAnalyses/ABIAnalysis.h"
 #include "Cache.h"
 #include "InterproceduralAnalysis.h"
 #include "Intraprocedural.h"
@@ -1235,6 +1236,7 @@ llvm::Function *CFEPAnalyzer<FO>::createFakeFunction(llvm::BasicBlock *Entry) {
 template<class FO>
 FunctionSummary CFEPAnalyzer<FO>::analyze(BasicBlock *Entry) {
   using namespace llvm;
+  using namespace ABIAnalyses;
 
   IRBuilder<> Builder(M.getContext());
 
@@ -1244,6 +1246,13 @@ FunctionSummary CFEPAnalyzer<FO>::analyze(BasicBlock *Entry) {
   // Recover the control-flow graph of the function
   auto CFG = collectDirectCFG(&OutlinedFunction);
 
+  // Run ABI-independent data-flow analyses
+  ABIAnalysesResults
+    ABIResults = ABIAnalyses::analyzeOutlinedFunction(OutFunc,
+                                                      *GCBI,
+                                                      PreHookMarker,
+                                                      PostHookMarker);
+
   // The analysis aims at identifying the callee-saved registers of a function
   // and establishing if a function returns properly, i.e., it jumps to the
   // return address (regular function). In order to achieve this, the IR is
diff --git a/scripts/monotone-framework.py b/scripts/monotone_framework.py
similarity index 72%
rename from scripts/monotone-framework.py
rename to scripts/monotone_framework.py
index 3317edc21..8fa84cab4 100755
--- a/scripts/monotone-framework.py
+++ b/scripts/monotone_framework.py
@@ -9,16 +9,17 @@
 # Additionally, one of the nodes should have a double border ("peripheries=2")
 # to represent it's the initial node.
 #
-# This script works and should keep working on Python 2.7 and Python 3.
+# This script works and should keep working on Python 3.6 .
 
 # Standard imports
 import sys
 import argparse
 from itertools import product
 from collections import defaultdict
+from typing import List, Mapping, Tuple
 
-# pygraphviz
-from pygraphviz import AGraph
+# networkx
+import networkx
 
 # numpy (optional)
 try:
@@ -34,23 +35,21 @@ except ImportError:
 out = lambda string: sys.stdout.write(string)
 log = lambda string: sys.stderr.write(string + "\n")
 
-def enumerate_graph(graph):
+def enumerate_graph(graph: networkx.MultiDiGraph):
   # Assign an identifier to each node
-  index = 0
-  for vertex in graph.nodes_iter():
-    vertex.attr["index"] = str(index)
-    index += 1
+  for i, vertex in enumerate(graph.nodes()):
+    graph.nodes[vertex]["index"] = str(i)
 
 def get_unique(container):
   assert len(container) == 1
   return container[0]
 
-def extract_lattice(input_graph):
+def extract_lattice(input_graph: networkx.MultiDiGraph):
   # Compute the lattice graph from the input graph. In practice we remove all
   # the edges that have a label, since they represent a transfer function
-  return drop_edge_if(input_graph, lambda edge: edge.attr["label"])
+  return drop_edge_if(input_graph, lambda edge, edge_data: "label" in edge_data)
 
-def compute_reachability_matrix(graph):
+def compute_reachability_matrix(graph: networkx.MultiDiGraph):
   # Build the adjacency matrix
   vertices = graph.number_of_nodes()
   edges = graph.number_of_edges()
@@ -61,9 +60,9 @@ def compute_reachability_matrix(graph):
     adj[x][x] = 1
 
   # Set to 1 all the cells representing a pair of adjacent vertices
-  for edge in graph.edges_iter():
-    x = int(edge[0].attr["index"])
-    y = int(edge[1].attr["index"])
+  for src, dst in graph.edges():
+    x = int(graph.nodes[src]["index"])
+    y = int(graph.nodes[dst]["index"])
     adj[x][y] = 1
 
   # Build the reachability matrix
@@ -81,11 +80,11 @@ def compute_reachability_matrix(graph):
 
   return reachability
 
-def is_cyclic(graph, entry):
+def is_cyclic(graph: networkx.MultiDiGraph, entry):
   visited = set()
   path = [object()]
   path_set = set(path)
-  stack = [graph.successors_iter(entry)]
+  stack = [graph.successors(entry)]
   while stack:
     for v in stack[-1]:
       if v in path_set:
@@ -94,24 +93,24 @@ def is_cyclic(graph, entry):
         visited.add(v)
         path.append(v)
         path_set.add(v)
-        stack.append(iter(graph.successors_iter(v)))
+        stack.append(iter(graph.successors(v)))
         break
     else:
       path_set.remove(path.pop())
       stack.pop()
   return False
 
-def check_lattice(lattice):
+def check_lattice(lattice: networkx.MultiDiGraph):
   # Check we have a single top and a single bottom
   top = None
   bottom = None
-  for v in lattice.nodes_iter():
+  for v in lattice.nodes():
     if lattice.in_degree(v) == 0:
-      assert bottom == None
+      assert bottom is None
       bottom = v
 
     if lattice.out_degree(v) == 0:
-      assert top == None
+      assert top is None
       top = v
   assert top is not None
   assert bottom is not None
@@ -121,29 +120,25 @@ def check_lattice(lattice):
 
   return top, bottom
 
-def drop_edge_if(graph, condition):
+def drop_edge_if(graph: networkx.MultiDiGraph, condition):
   new_graph = graph.copy()
 
-  for edge in new_graph.edges():
-    new_graph.remove_edge(edge)
-
-  for edge in graph.edges_iter():
-    if not condition(edge):
-      new_graph.add_edge(edge[0], edge[1], None, **edge.attr)
-
+  for src, dst, key, edge_data in list(new_graph.edges(keys=True, data=True)):
+    if condition((src, dst), edge_data):
+      new_graph.remove_edge(src, dst, key)
   return new_graph
 
-def extract_transfer_function_graph(input_graph, call_arcs):
+def extract_transfer_function_graph(input_graph: networkx.MultiDiGraph, call_arcs):
   # Build the transfer function graph. Drop all the edges without a label (those
   # representing the lattice).
-  tf_graph = drop_edge_if(input_graph, lambda edge: not edge.attr["label"])
+  tf_graph = drop_edge_if(input_graph, lambda edge, edge_data: "label" not in edge_data)
 
   # Add the ReturnFrom... arcs
   if call_arcs:
-    edge_labels = set(edge.attr["label"] for edge in tf_graph.edges())
-    for v in tf_graph.nodes_iter():
+    edge_labels = set(edge_data["label"] for _, _, edge_data in tf_graph.edges(data=True))
+    for v in tf_graph.nodes():
 
-      return_edge_name = "ReturnFrom" + v.name
+      return_edge_name = "ReturnFrom" + v
 
       # Check if the ReturnFrom edge has already been explicitly provided
       if return_edge_name in edge_labels:
@@ -154,39 +149,38 @@ def extract_transfer_function_graph(input_graph, call_arcs):
       assert len(source) <= 1
       if source:
         source = list(source)[0]
-        tf_graph.add_edge(source, v)
-        new_edge = tf_graph.get_edge(source, v)
+        edge_key = tf_graph.add_edge(source, v)
+        new_edge = tf_graph.edges[(source, v, edge_key)]
       else:
-        tf_graph.add_edge(v, v)
-        new_edge = tf_graph.get_edge(v, v)
-      new_edge.attr["label"] = return_edge_name
+        edge_key = tf_graph.add_edge(v, v)
+        new_edge = tf_graph.edges[(v, v, edge_key)]
+      new_edge["label"] = return_edge_name
 
   return tf_graph
 
-def check_transfer_functions(tf_graph, reachability, transfer_functions):
+def check_transfer_functions(tf_graph: networkx.MultiDiGraph,
+                             reachability: List[List[float]],
+                             transfer_functions: Mapping[str, List[Tuple[str, str]]]):
   tf_graph = tf_graph.copy()
   # Automatically add self-loops where required
   all_vertices = set(tf_graph.nodes())
   for name, edges in transfer_functions.items():
     no_self = set()
-    for edge in edges:
-      no_self.add(edge[0])
+    for source, _ in edges:
+      no_self.add(source)
     need_self = all_vertices - no_self
     for vertex in need_self:
-      tf_graph.add_edge(vertex, vertex)
-      new_edge = tf_graph.get_edge(vertex, vertex)
-      new_edge.attr["label"] = name
-      edges.append(new_edge)
+      tf_graph.add_edge(vertex, vertex, label=name)
+      edges.append((vertex, vertex))
 
   result = True
-  s = lambda edge: int(edge[0].attr["index"])
-  d = lambda edge: int(edge[1].attr["index"])
+  s = lambda edge: int(tf_graph.nodes[edge[0]]["index"])
+  d = lambda edge: int(tf_graph.nodes[edge[1]]["index"])
   lte = lambda a, b: reachability[a][b] != 0
   for name, edges in transfer_functions.items():
     for a, b in product(edges, edges):
       if a == b:
         continue
-
       if lte(s(a), s(b)) and not lte(d(a), d(b)):
         result = False
         log("The transfer function {} is not monotone:\n".format(name))
@@ -196,10 +190,26 @@ def check_transfer_functions(tf_graph, reachability, transfer_functions):
                                               b[1].name))
 
   return result
+def load_graph(path: str) -> networkx.MultiDiGraph:
+  '''
+  Loads a networkx.MultiDiGraph from a dot file
+  Notes:
+  - pydot treats every attribute as a string, so we need to manually unquote 
+    strings
+  '''
+  graph = networkx.MultiDiGraph(networkx.nx_pydot.read_dot(path))
+  for _, _, data in graph.edges(data=True):
+    for key, val in data.items():
+      if isinstance(val, str):
+        if len(val) > 2:
+          if val[0] == '"' and val[-1] == '"':
+            val = val[1:-1]
+            data[key] = val
+  return graph
 
 def process_graph(path, call_arcs):
   out = ""
-  input_graph = AGraph(path)
+  input_graph = load_graph(path)
 
   enumerate_graph(input_graph)
 
@@ -213,14 +223,13 @@ def process_graph(path, call_arcs):
   tf_graph = extract_transfer_function_graph(input_graph, call_arcs)
 
   transfer_functions = defaultdict(lambda: [])
-  for edge in tf_graph.edges_iter():
-    transfer_functions[edge.attr["label"]].append(edge)
+  for src, dst, edge_data in tf_graph.edges(data=True):
+    transfer_functions[edge_data["label"]].append((src, dst))
 
   # Check the monotonicity of the transfer function
   assert check_transfer_functions(tf_graph, reachability, transfer_functions)
 
   name = input_graph.name
-
   # Generate C++ class
   out += ("""class {} {{
 public:
@@ -231,23 +240,21 @@ public:
 """)
 
   # Get the default lattice element (has the "peripheries" property)
-  default = [v.name
-             for v in lattice.nodes_iter()
-             if v.attr["peripheries"]][0]
-
+  default = [v
+             for v, v_data in lattice.nodes(data=True)
+             if "peripheries" in v_data][0]
   # Get all the names
-  values = sorted([v.name for v in lattice.nodes_iter()])
+  values = sorted([v for v in lattice.nodes()])
   out += ("    " + ",\n    ".join(values) + "\n")
   out += ("""  };
 
 """)
-
   # Print the enumeration of all the possible transfer functions
   out += ("""  enum TransferFunction {{
 """.format())
 
   # Get all the transfer function names
-  tfs = [e.attr["label"] for e in tf_graph.edges_iter()]
+  tfs = [e_data["label"] for _, _, e_data in tf_graph.edges(data=True)]
   out += ("    " + ",\n    ".join(sorted(tfs)) + "\n")
   out += ("""  };
 
@@ -266,22 +273,22 @@ public:
     return {};
   }}
 
-""".format(name, bottom.name, name, default))
+""".format(name, bottom, name, default))
 
   # Emit the combine operator
   out += ("""  void combine(const {} &Other) {{
 """.format(name))
 
   node_by_index = lambda index: get_unique([x
-                                            for x in lattice.nodes_iter()
-                                            if x.attr["index"] == str(index)])
+                                            for x, x_data in lattice.nodes(data=True)
+                                            if x_data["index"] == str(index)])
 
   result = defaultdict(lambda: [])
-  for v1 in lattice.nodes_iter():
-    for v2 in lattice.nodes_iter():
+  for v1, v1_data in lattice.nodes(data=True):
+    for v2, v2_data in lattice.nodes(data=True):
       if v1 != v2:
-        i1 = int(v1.attr["index"])
-        i2 = int(v2.attr["index"])
+        i1 = int(v1_data["index"])
+        i2 = int(v2_data["index"])
         nonzero = lambda i: set([x[0]
                                  for x in enumerate(reachability[i])
                                  if x[1] != 0])
@@ -300,9 +307,9 @@ public:
     else:
       out += (""" else if (""")
     conditions = []
-    for this, other in sorted(pairs, key=lambda x: (x[0].name, x[1].name)):
+    for this, other in sorted(pairs, key=lambda x: (x[0], x[1])):
       condition = "(Value == {} && Other.Value == {})"
-      condition = condition.format(this.name, other.name)
+      condition = condition.format(this, other)
       conditions.append(condition)
     conditions[0] = conditions[0].lstrip()
     conditions_string = ("\n        || "
@@ -311,7 +318,7 @@ public:
     out += conditions_string.join(conditions)
     out += (""") {{
       Value = {};
-    }}""".format(output.name))
+    }}""".format(output))
     first = False
 
   out += ("""
@@ -322,17 +329,17 @@ public:
   # Emit the comparison operator of the lattice
   out += ("""  bool lowerThanOrEqual(const {} &Other) const {{
     return Value == Other.Value
-      || """.format(name, name))
+      || """.format(name))
 
   result = []
-  for v1 in sorted(lattice.nodes_iter(), key=lambda x: x.name):
-    for v2 in sorted(lattice.nodes_iter(), key=lambda x: x.name):
+  for v1 in sorted(lattice.nodes()):
+    for v2 in sorted(lattice.nodes()):
       if v1 != v2:
-        i1 = int(v1.attr["index"])
-        i2 = int(v2.attr["index"])
+        i1 = int(lattice.nodes[v1]["index"])
+        i2 = int(lattice.nodes[v2]["index"])
         if reachability[i1][i2] != 0:
           condition = """(Value == {} && Other.Value == {})"""
-          condition = condition.format(v1.name, v2.name)
+          condition = condition.format(v1, v2)
           result.append(condition)
 
   out += ("\n      || ".join(result))
@@ -341,12 +348,12 @@ public:
 
 """)
 
-  tf_names = sorted([e.attr["label"] for e in tf_graph.edges_iter()])
+  tf_names = sorted([e_data["label"] for _, _, e_data in tf_graph.edges(data=True)])
 
   # Emit the transfer function implementation
   out += ("""  void transfer(TransferFunction T) {{
     switch(T) {{
-""".format(name))
+""".format())
   for tf in tf_names:
     out += ("""    case {}:
       switch(Value) {{
@@ -372,7 +379,7 @@ public:
   # Emit the transfer function implementation
   out += ("""  void transfer(GeneralTransferFunction T) {{
     switch(T) {{
-""".format(name))
+""".format())
   for tf in tf_names:
     out += ("""    case GeneralTransferFunction::{}:
       switch(Value) {{
@@ -428,7 +435,7 @@ public:
     return {}({});
   }}
 
-""".format(name, name, top.name))
+""".format(name, name, top))
 
   # Accessor for the current value
   out += ("""  Values value() const { return Value; }
@@ -441,7 +448,7 @@ public:
   template<typename T>
   void dump(T &Output) const {{
     switch(Value) {{
-""".format(name, name, name, top.name))
+""".format())
 
   for value in values:
     out += ("""    case {}:
diff --git a/scripts/monotone_framework_lattice.py b/scripts/monotone_framework_lattice.py
new file mode 100755
index 000000000..556ec1252
--- /dev/null
+++ b/scripts/monotone_framework_lattice.py
@@ -0,0 +1,242 @@
+#!/usr/bin/env python3
+
+# This script generates C++ classes from a GraphViz file representing a monotone
+# framework and a template file.
+#
+# The graph should meet the same requirements as monotone_framework.py
+#
+
+import argparse
+import sys
+from collections import defaultdict
+
+import importlib
+import monotone_framework
+
+def gen_combine_values(lattice, reachability):
+  out = ''
+
+  # Emit the combine operator
+  out += """LatticeElement combineValues(const LatticeElement &LHS, const LatticeElement &RHS) {
+"""
+
+  node_by_index = lambda index: monotone_framework.get_unique([x
+                                            for x, x_data in lattice.nodes(data=True)
+                                            if x_data["index"] == str(index)])
+
+  result = defaultdict(lambda: [])
+  for v1, v1_data in lattice.nodes(data=True):
+    for v2, v2_data in lattice.nodes(data=True):
+      if v1 != v2:
+        i1 = int(v1_data["index"])
+        i2 = int(v2_data["index"])
+        nonzero = lambda i: set([x[0]
+                                 for x in enumerate(reachability[i])
+                                 if x[1] != 0])
+
+        output = max(nonzero(i1) & nonzero(i2),
+                     key=lambda i: reachability[i1][i] + reachability[i2][i])
+        output = node_by_index(output)
+
+        result[output].append((v1, v2))
+        assert output in result
+
+  first = True
+  for output, pairs in sorted(result.items(), key=lambda x: x[0]):
+    if first:
+      out += ("""  if (""")
+    else:
+      out += (""" else if (""")
+    conditions = []
+    for this, other in sorted(pairs, key=lambda x: (x[0], x[1])):
+      condition = "(LHS == LatticeElement::{} && RHS == LatticeElement::{})"
+      condition = condition.format(this, other)
+      conditions.append(condition)
+    conditions[0] = conditions[0].lstrip()
+    conditions_string = ("\n      || "
+                         if first
+                         else "\n             || ")
+    out += conditions_string.join(conditions)
+    out += (""") {{
+    return LatticeElement::{};
+  }}""".format(output))
+    first = False
+
+  out += ("""
+  return LHS;
+}
+
+""")
+  return out
+
+def gen_is_less_or_equal(lattice, reachability):
+  out = ''
+
+  # Emit the comparison operator of the lattice
+  out += ("""bool isLessOrEqual(const LatticeElement &LHS, const LatticeElement &RHS) {
+  return LHS == RHS
+    || """)
+
+  result = []
+  for v1, v1_data in lattice.nodes(data=True):
+    for v2, v2_data in lattice.nodes(data=True):
+      if v1 != v2:
+        i1 = int(v1_data["index"])
+        i2 = int(v2_data["index"])
+        if reachability[i1][i2] != 0:
+          condition = """(LHS == LatticeElement::{} && RHS == LatticeElement::{})"""
+          condition = condition.format(v1, v2)
+          result.append(condition)
+
+  out += ("\n    || ".join(result))
+  out += (""";
+}
+
+""")
+  return out
+
+def gen_transfer_function(tf_names, transfer_functions):
+  out = ''
+
+  # Emit the transfer function implementation
+  out += """LatticeElement transfer(TransferFunction T, const LatticeElement &E) {
+  switch(T) {
+"""
+  for tf in tf_names:
+    out += ("""  case TransferFunction::{}:
+    switch(E) {{
+""".format(tf))
+    for edge in transfer_functions[tf]:
+      source, destination = edge
+      out += ("""    case LatticeElement::{}:
+      return LatticeElement::{};
+""".format(source, destination))
+    out += ("""    default:
+      revng_abort("Invalid LatticeElement value found");
+    }
+
+""")
+
+  out += ("""  default:
+    return E;
+  }
+}
+
+""")
+  return out
+
+def gen_lattice_element_enum(lattice):
+  out = ''
+
+  # Print the enumeration of all the possible lattice values
+  out += ("""enum LatticeElement {
+""")
+
+  # Get all the names
+  values = [v for v in lattice.nodes()]
+  out += ("  " + ",\n  ".join(values) + "\n")
+  out += ("""};
+""")
+  return out
+
+def gen_transfer_function_enum(tf_graph):
+  out = ''
+
+  # Print the enumeration of all the possible transfer functions
+  out += ("""enum TransferFunction {
+""")
+
+  # Get all the transfer function names
+  tfs = [e_data["label"] for _, _, e_data in tf_graph.edges(data=True)]
+  out += ("  " + ",\n  ".join(sorted(tfs)) + "\n")
+  out += ("""};
+
+""")
+  return out
+
+def process_graph(path, call_arcs):
+  input_graph = monotone_framework.load_graph(path)
+
+  monotone_framework.enumerate_graph(input_graph)
+
+  lattice = monotone_framework.extract_lattice(input_graph)
+
+  # Check that the lattice is valid for a monotone framework
+  _ = monotone_framework.check_lattice(lattice)
+
+  reachability = monotone_framework.compute_reachability_matrix(lattice)
+
+  tf_graph = monotone_framework.extract_transfer_function_graph(input_graph, call_arcs)
+
+  transfer_functions = defaultdict(lambda: [])
+  for src, dst, edge_data in tf_graph.edges(data=True):
+    transfer_functions[edge_data["label"]].append((src, dst))
+
+  # Check the monotonicity of the transfer function
+  assert monotone_framework.check_transfer_functions(tf_graph, reachability, transfer_functions)
+
+  tf_names = sorted([edge_data["label"] for _, _, edge_data in tf_graph.edges(data=True)])
+
+  extremal_lattice_element = [v
+            for v, v_data in lattice.nodes(data=True)
+            if "peripheries" in v_data][0]
+
+  return {
+    'transfer_function_names': tf_names,
+    'lattice_name': input_graph.name,
+    'lattice_elements_enums': gen_lattice_element_enum(lattice),
+    'extremal_lattice_element': extremal_lattice_element,
+    'transfer_function_enums': gen_transfer_function_enum(tf_graph),
+    'is_less_or_equal_definition': gen_is_less_or_equal(lattice, reachability),
+    'combine_values_definition': gen_combine_values(lattice, reachability),
+    'transfer_function_definition': gen_transfer_function(tf_names, transfer_functions)
+  }
+
+def main():
+  parser = argparse.ArgumentParser(description="Generate C++ code from dot \
+  files representing a monotone framework.")
+  parser.add_argument("--call-arcs",
+                      action="store_true",
+                      help="Add call arcs.")
+  parser.add_argument("template",
+                      metavar="TEMPLATE",
+                      help="""Lattice template file.
+                      you can use the keywords:
+                      - %LatticeName% the name of the lattice extracted from the graph name
+                      - %LatticeElement% the C++ enum definition for the elements in the lattice `enum LatticeElement {...}`
+                      - %ExtremalLatticeElement% the name for the default value for a lattice element
+                      - %TransferFunction% the C++ enum definition for the possible transfer functions `enum TransferFunction {...}`
+                      - %isLessOrEqual% the C++ function with signature `bool isLessOrEqual(const LatticeElement &LHS, const LatticeElement &RHS)`
+                      - %combineValues% the C++ function with signature `bool combineValues(const LatticeElement &LHS, const LatticeElement &RHS)`
+                      - %transfer% the C++ function with signature `bool transfer(TransferFunction T, const LatticeElement &RHS)`
+                      """)
+  parser.add_argument("inputs",
+                      metavar="GRAPH",
+                      nargs="+",
+                      help="GraphViz input file.")
+  args = parser.parse_args()
+
+  # Print the template file
+  with open(args.template) as template_file:
+    template = template_file.read()
+
+  # Process each input graph
+  all_transfer_functions = set()
+  for path in args.inputs:
+    generated_code = process_graph(
+        path, args.call_arcs)
+    all_transfer_functions |= set(generated_code['transfer_function_names'])
+
+  monotone_framework.out(template.replace('%LatticeName%', generated_code['lattice_name'])
+                                 .replace('%LatticeElement%', generated_code['lattice_elements_enums'])
+                                 .replace('%ExtremalLatticeElement%', generated_code['extremal_lattice_element'])
+                                 .replace('%TransferFunction%', generated_code['transfer_function_enums'])
+                                 .replace('%isLessOrEqual%', generated_code['is_less_or_equal_definition'])
+                                 .replace('%combineValues%', generated_code['combine_values_definition'])
+                                 .replace('%transfer%', generated_code['transfer_function_definition']))
+
+
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main())