feat(0.1): incorporate PR #44 nondet-generator + fix GoogleTest tag

- Cherry-pick 68cd2eb from fuzzer-option branch (PR #44)
- Adds --nondet-generator CLI option (fuzzer/symex)
- Fix GoogleTest GIT_TAG to release-1.12.1 for CMake compat
- Build OK (50/50), unit tests 7/7 passed
- Migration report: docs/migration/0.1-pr44-nondet-generator.md

Author: GuilhermeBn198

cmake/CMakeLists.txt.googletest

@@ -5,7 +5,7 @@ project(googletest-download NONE)
 include(ExternalProject)
 ExternalProject_Add(googletest
   GIT_REPOSITORY    https://github.com/google/googletest.git
-  GIT_TAG           master
+  GIT_TAG           release-1.12.1
   SOURCE_DIR        "${CMAKE_CURRENT_BINARY_DIR}/googletest-src"
   BINARY_DIR        "${CMAKE_CURRENT_BINARY_DIR}/googletest-build"
   CONFIGURE_COMMAND ""

docs/migration/0.1-pr44-nondet-generator.md

@@ -0,0 +1,55 @@
+# 0.1 — Incorporar PR #44 (`--nondet-generator`)
+
+**Data:** 17/05/2026
+**Status:** ✅ Concluída
+
+## O que foi feito
+
+Cherry-pick do commit `68cd2eb0` da branch `origin/fuzzer-option` (PR #44) para a branch `feat-update`, que já continha as mudanças da PR #46 (`--target-function-name`).
+
+A PR #44 adiciona a opção `--nondet-generator` ao CLI do Map2Check, permitindo selecionar explicitamente o motor de geração de valores não-determinísticos:
+- `--nondet-generator symex` → usa apenas KLEE (symbolic execution)
+- `--nondet-generator fuzzer` → usa apenas LibFuzzer
+- Sem a flag → comportamento padrão: tenta LibFuzzer primeiro, depois KLEE
+
+### Arquivos alterados
+- `modules/frontend/map2check.cpp` — 37 inserções, 4 remoções
+
+### Método de integração
+```bash
+git cherry-pick 68cd2eb0 --no-commit
+# Auto-merge sem conflitos com as mudanças da PR #46
+```
+
+## Testes executados
+
+### Build
+| Teste | Resultado | Observações |
+|:------|:---------|:------------|
+| `make-release.sh` (50 targets) | ✅ Build OK | Sem erros, 3 warnings esperados (enumeration switch) |
+
+### Testes unitários (7/7)
+| Teste | Resultado | Observações |
+|:------|:---------|:------------|
+| HelloGTest | ✅ Passed | 0.00s |
+| AllocationLogTest | ✅ Passed | 0.00s |
+| HeapLogTest | ✅ Passed | 0.00s |
+| ContainerReallocTest | ✅ Passed | 0.00s |
+| BTreeTest | ✅ Passed | 0.16s |
+| ContainerBTreeTest | ✅ Passed | 0.15s |
+| MemTrackTest | ✅ Passed | 0.00s |
+
+### Testes da funcionalidade PR #44
+| Teste | Resultado | Observações |
+|:------|:---------|:------------|
+| `--nondet-generator symex` (test-0158_1-1.c) | ✅ VERIFICATION SUCCEEDED | Usa apenas KLEE |
+| `--nondet-generator fuzzer` (test-0158_1-1.c) | ✅ Timeout (esperado) | Usa apenas LibFuzzer, timeout é comportamento normal |
+| `--nondet-generator invalid` | ✅ Erro adequado | Mensagem: "Selected generator don't exist, available: fuzzer symex" |
+| Sem flag (comportamento padrão) | ✅ VERIFICATION SUCCEEDED | LibFuzzer → KLEE sequencial, como antes |
+
+## Problemas encontrados
+- Nenhum conflito no cherry-pick
+- O warning `[-Wswitch]` em `witness.hpp:107` é pré-existente (enumeration `MEMSAFETY` não tratada) — não é causado pelas mudanças da PR #44
+
+## Próximos passos
+- **Tarefa 0.2:** Executar suite completa de regressão (9 testes) e registrar baseline definitivo da branch de trabalho (com PRs #44 + #46 integradas)

modules/frontend/map2check.cpp

@@ -297,6 +297,9 @@ int main(int argc, char **argv) {
         ("debug", "\tdebug mode")
         ("input-file", po::value<std::vector<std::string>>(),
                       "\tspecifies the files")
+        ("nondet-generator", po::value<std::string>(),
+                      R"(specifies the nondet-generator, valid values are fuzzer (libFuzzer),
+symex (Klee))")
         ("smt-solver", po::value<std::string>()->default_value("z3"),
                       R"(specifies the smt-solver, valid values are stp (STP),
 z3 (Z3 is default), btor (Boolector), and yices2 (Yices))")
@@ -410,6 +413,31 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))")
       Map2Check::Log::Debug("Current path:");
       system("echo $MAP2CHECK_PATH");
     }
+    if (vm.count("nondet-generator")) {
+      string generatorname = vm["nondet-generator"].as<string>();
+      std::transform(generatorname.begin(), generatorname.end(),
+                     generatorname.begin(), [](unsigned char c){
+                     return std::tolower(c); });
+
+      std::vector<std::string> available_generators = {"fuzzer", "symex"};
+
+      if ( !std::count(available_generators.begin(), available_generators.end(), generatorname) ) {
+        std::cout << "Selected generator don't exist, available: ";
+        for(auto &s : available_generators) {
+          std::cout << " " << s << " ";
+        }
+        std::cout << desc << "\n";
+        return ERROR_IN_COMMAND_LINE;
+      } else {
+        std::cout << "Adopting " + generatorname + " nondet-generator... \n";
+        if(generatorname == available_generators[0])
+          args.generator = Map2Check::NonDetGenerator::LibFuzzer;
+        if(generatorname == available_generators[1])
+          args.generator = Map2Check::NonDetGenerator::Klee;
+      }
+    } else {
+      args.generator = Map2Check::NonDetGenerator::None;
+    }
     if (vm.count("input-file")) {
       std::string pathfile;
       pathfile = accumulate(
@@ -420,10 +448,15 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))")
       // std::cout << pathfile << std::endl;
       fs::path absolute_path = fs::absolute(pathfile);
       args.inputFile = absolute_path.string();
-      args.generator = Map2Check::NonDetGenerator::LibFuzzer;
-      map2check_execution(args);
-      if (!foundViolation) {
-        args.generator = Map2Check::NonDetGenerator::Klee;
+      if(args.generator == Map2Check::NonDetGenerator::None) {
+        args.generator = Map2Check::NonDetGenerator::LibFuzzer;
+        map2check_execution(args);
+        if (!foundViolation) {
+          args.generator = Map2Check::NonDetGenerator::Klee;
+          map2check_execution(args);
+        }
+      }
+      else {
         map2check_execution(args);
       }
     }