Gyula Sallai

Currently we do not have support 'malloc' (or dynamic memory allocation in general) in the flat memory model. Even though parts of the required API exist, we should add full,...

Consider the following code: ```c #include int nondet1(); int nondet2(); int nevercalled() { return nondet2(); } int main(void) { int x = nondet1(); assert(x != 0); return 0; } ```...

Translating the following program results in a segmentation fault: ```c int *a; int b; int c(int e, int *g) { for (;;) for (b = 1; e; b++) if (a[b])...

The expression transformer in `tools/gazer-theta/lib/ThetaExpr.cpp` does not handle `Rem` expressions, resulting in warnings and invalid Theta CFAs, e.g.: ``` Unhandled expr Int Rem(Int main/main/bb1165/a17.0_inlined0,71) Unhandled expr Int Rem(Int main/main/bb1165/a17.0_inlined0,299872) Unhandled...

Currently we can only write test harnesses in the LLVM bitcode or LLVM IR assembly formats. We could extend this with a more human-readable C program output.

Our CFA construction algorithm assumes that each function has a _reducible_ control flow, i.e. each loop has a single dominating loop header, otherwise the CFA generation process will crash. While...

EbsInstanceBlockDevice has invalid status field

1

Hey, According to the [docs](https://docs.aws.amazon.com/AWSEC2/latest/APIReference/API_EbsInstanceBlockDevice.html), the possible valid value for the `status` field in `EbsInstanceBlockDevice` is one of `attaching | attached | detaching | detached`. Using `describe_instances` in Moto (v5.1.18)...