Kunjian Song

> Do you have a simple test that doesn't work because of the model? @mikhailramalho Currently all test cases in `esbmc-cpp/string` fail due to `PARSING ERROR` when using clang-cpp-frontend. The...

> No, what I meant to ask is if you are using the system's cstring/string headers in whatever test you're running, i.e, run the tests without the "-I ". >...

Managed to get rid of all the errors. However, still loads of warnings. [output.log](https://github.com/esbmc/esbmc/files/9302196/output.log) Some of them should NOT be ignored, e.g. return a reference to a local variable on...

> Do these changes enable some regression tests? If not, shall we add some regression tests? Nope. These changes just fixed the parsing errors in the operational model, allowing more...

>I wonder why we don't just refer to the C-models when they're available, e.g., for memmove, strtok and friends. +1 `src/c2goto/library/string.c` and `src/cpp/library/cstring` --- they look very similar. Some functions...

> @kunjsong01: can I ask you you for the status of this PR? There are two TODOs at the moment: 1. restructuring the include as discussed in the comments above...

Hi @feliperodri , I usually add `-I /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/` on macOS. ``` ./esbmc main.c \ -I /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/ \ --partial-loops --unwind 10 ``` But this is just a quick workaround. I got...

> Why is this necessary for macOS in the first place? Clang in ESBMC uses the search list below: ``` #include "..." search starts here: #include search starts here: /var/folders/0c/0485rl0x48b3xy7dz5mgy2z00000gn/T/esbmc.34ba-d6fc-f5ca/headers...

> I assume the clang output you posted comes from a pre-built clang on macos that esbmc is not linked against, yes? Yes the "correct search list" was printed by...

> Maybe we can find a way on macos to build against the system clang directly. I reckon this will resolve the issue of lib search path. However, depending on...