Home

* **Welcome to the Map2Check wiki** This wiki will try to guide you through some of the project structure and common usages. Map2Check works by transforming the C code into LLVM bytecode and reasoning about this bytecode using transformations to inject custom functions and behaviours. Finally it links this bytecode with a custom C library, then executes this code and checks for the behaviour, generating a test case for invalid programs. Map2Check has the following features: - Memory, Reachability, Signed Overflow, Assert verification - Non-deterministic number generation - Witness generation - Test-case generation * Project Architecture Map2Check works by using LLVM pass to instrument bytecode (Backend-Pass), then implements those functions on Backend-Library, finally the frontend works by processing generated files