Chenfeng Wei

[Coverage] Support Condition Coverage

7

This PR aims to support condition coverage in ESBMC. Most importantly, we should be able to support short-circuit evaluation. example 1 ```c++ int main() { int a = 1; int...

Cmake Option to unset ESBMC_CHERI_CLANG?

2

I was trying to build ESBMC with the command I have been using. However, I met this issue recently when trying to run CMake ```sh -- Clang is CHERI-enabled, enabling...

Fix the missing contract name in the symbol id. ```solidity contract Base { function test() public { uint xx; } } ``` Result: ```sh #before sol:@C@@F@test@xx#13 #after sol:@C@Base@F@test@xx#13 ``` Thank...

Command: `esbmc file.c --incremental-bmc (--k-induction) --multi-property` These two examples work correctly. ```c++ void func() { assert(0 && "1"); } void func2() { assert(0 && "2"); } int main() { func();...

[C] ESBMC shows false positive(?) comparing to CBMC

9

- I am testing a mapping library from [rxi/map](https://github.com/rxi/map) which I am planning to implement in Solidity ```c++ struct map_node_t; typedef struct map_node_t map_node_t; typedef struct { map_node_t **buckets; unsigned...

[multi-property] Partially bug fixed for multi-property with kind and incr

7

Related issue: #1902 So the issue is caused by that, the claims (`dereference failure`) being added during the symex process, which cannot be removed permanently from the goto_functions. Thus, every...

Previously, we do not support Contract type due to that we do not support struct type. Since we already support struct now, we should be able to parse Contract type...

Changed as suggested in #1769

[Condition Coverage] Update Condition Coverage Calculation Strategy

1

We now count all the conditions, instead of only the guard of the if-expr. This includes the condition within `ASSERT`, `ASSUME`, `ASSIGN`, `GOTO`, `RETURN`, `FUNCTION_CALL` and `OTHER`. E.g. ```c++ int...