Mikhail R. Gadelha
Mikhail R. Gadelha
I'm using the `vc_bvConstExprFromStr` methods to create some large bitvectors (width > 64), but is there a way to get its value from the model also as an array of...
#### 53f69675260a10f451d85a91dee1fa6ba1cae633 [ARMv7][32bit] ASSERTION FAILED: CacheableIdentifier::isCacheableIdentifierCell(fieldNameValue) https://bugs.webkit.org/show_bug.cgi?id=242640 Reviewed by NOBODY (OOPS!). This patch adds AccessType::GetPrivateNameById, the corresponding slow path code, and changes compileGetPrivateNameById to use it when calling cachedGetById. The...
I've found this by accident: 1. We ignore malloc: https://github.com/esbmc/esbmc/blob/master/src/goto-programs/builtin_functions.cpp#L177 2. Even worse, we assert(0) in new: https://github.com/esbmc/esbmc/blob/master/src/goto-programs/builtin_functions.cpp#L270
Our simplification code has some design flaws that hurt performance: 1. It is performed top-down: we try to simplify the top expr, then the operands, then the top expr again...
* Fixed globals assignments being printed after main * Implemented enter_function node * Implemented returnFrom node * Don't print duplicated assignments
I've found this repo that implements correctly rounded fp operations. Maybe we can port them to esbmc: https://gitlab.inria.fr/core-math/core-math/-/tree/master/
This is a very weird piece of code that I don't really understand why it should be there. Pushed here to check the regressions, @rafaelsamenezes can you run this patch...
Without a doubt, the slowest part of the compilation is the model generation, so an improvement would be making it run in parallel: instead of passing a list of c...
I recently came across this great blog post: https://blog.m-ou.se/floats/ The blog post describes a conversion from u128 to f64, but the github repo has them all: https://github.com/m-ou-se/floatconv/blob/main/src/soft.rs. The generated assemblies...
The new message interface already removes several throws in favor of log_error + abort, we should finish the job.