ESBMC-AI

[kaixin6321]

Hi yiannis,

Hi yiannis, I am a master student of Prof. Lucas and I chose to study his ESBMC-AI framework. so I was wondering if I could ask you some questions on this topic.

After I successfully downloaded and deployed the latest version of ESBMC and the ESBMC-AI framework, I wasn't able to operate as you did in the youtube video. My output: none. i don't know why this is happening.

Warm regards,
kaixin

[Yiannis128]

Hi, can you send a picture? Also, did you read the Initial Setup instructions in the wiki?

[kaixin6321]

Yes I followed the tutorial. It's all configured too. Attached is a picture of mine.

[kaixin6321]

Maybe I don't know enough about frames, I don't know how you managed to get to that step inside your youtube video.

[Yiannis128]

Do you mind sending me the file you're trying to debug? I can try, and it would help resolve the problem faster.

[kaixin6321]

To be precise, my test script isn't finished yet. Just ran into these problems. Can you send me a script that will test the code? I'm not sure that my code is able to call the functions of the esbmc-ai framework.

[kaixin6321]

Now it seems I just don't know how this step works. It's that esbmc_ai.py script.

[kaixin6321]

The tool I use is pycharm

[kaixin6321]

I actually kind of don't quite understand what the esbmc_ai.py script does. Isn't it possible to call the framework directly via the [esbmc-ai samples/optimise-code/mult.c] directive to inspect the program?

[Yiannis128]

You can, but you would need to install it globally to call it as ./esbmc-ai, instead on Linux/macOS call: ./esbmc-ai and on Windows you can do python3 -m esbmc_ai to launch it.

[kaixin6321]

I feel as if I've solved the problem. Right now there is just no quota for openai company APIs

[Yiannis128]

I think that you may need to either buy some credits to use OpenAI LLMs or simply switch to an open source alternative like Falcon :)

[kaixin6321]

I have purchased llm from openai. having some problems with the optimise code step.

[kaixin6321]

So what should be done next to optimise this framework and what needs to be done.

[Yiannis128]

Optimize code has been removed as it was very unstable. I advise against using it until a better implementation is complete. However, it seems that you don't have your C standard libraries installed, if assert.h is not found.

[kaixin6321]

I've already installed it. But I don't know why I can only find the location by assigning a value. I've also added it to the environment variable, but highlighting the incloud path, he still fails to find the location of the standard library.

[Yiannis128]

Does this work with ESBMC only?

[kaixin6321]

I don't think so. I think there may be a problem somewhere in the configuration of the environment that prevents the location of the standard library from being automatically located. But I have deployed one location of the standard library in the environment variables, so it doesn't make sense that it would have any effect on the other locations of the standard library (this part I think may be caused by the fact that I've downloaded and installed the standard library several times, so I've forgotten what folder some of the locations are in, and I feel like maybe it's a duplication problem).

[kaixin6321]

Hi, yiannis.How to use this framework further next to consider the detection and repair of errors in the C++ programming language. I made a script to summarise the output using a group of 10 C programs. The framework is further updated for multiple sets of output reports. Do you think this is correct?