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

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