diff --git a/config.toml b/config.toml index b573fb2..6ba9e55 100644 --- a/config.toml +++ b/config.toml @@ -12,6 +12,7 @@ name = "esbmc" path = "~/.local/bin/esbmc" params = [ "--interval-analysis", + "--memory-leak-check", "--goto-unwind", "--unlimited-goto-unwind", "--k-induction", @@ -21,7 +22,6 @@ params = [ "2", "--floatbv", "--unlimited-k-steps", - "--compact-trace", "--context-bound", "2", ] diff --git a/esbmc_ai/__about__.py b/esbmc_ai/__about__.py index 9daf356..2289d7a 100644 --- a/esbmc_ai/__about__.py +++ b/esbmc_ai/__about__.py @@ -1,4 +1,4 @@ # Author: Yiannis Charalambous -__version__ = "v0.6.0.dev1" +__version__ = "v0.6.0.dev2" __author__: str = "Yiannis Charalambous" diff --git a/esbmc_ai/__main__.py b/esbmc_ai/__main__.py index 0964550..5738094 100755 --- a/esbmc_ai/__main__.py +++ b/esbmc_ai/__main__.py @@ -135,13 +135,10 @@ def _run_esbmc(source_file: SourceFile, anim: BaseLoadingWidget) -> str: # ESBMC will output 0 for verification success and 1 for verification # failed, if anything else gets thrown, it's an ESBMC error. if not Config().get_value("allow_successful") and verifier_result.successful(): - printv("Success!") - print(verifier_result.output) - sys.exit(0) - elif verifier_result.return_code != 0 and verifier_result.return_code != 1: printv(f"ESBMC exit code: {verifier_result.return_code}") printv(f"ESBMC Output:\n\n{verifier_result.output}") - sys.exit(1) + print("Sample successfuly verified. Exiting...") + sys.exit(0) return verifier_result.output @@ -304,6 +301,7 @@ def main() -> None: printvv("Loading main config") Config().init(args) + printv(f"Config File: {Config().cfg_path}") check_health() # Load addons printvv("Loading addons") diff --git a/esbmc_ai/commands/fix_code_command.py b/esbmc_ai/commands/fix_code_command.py index c289428..4d901f4 100644 --- a/esbmc_ai/commands/fix_code_command.py +++ b/esbmc_ai/commands/fix_code_command.py @@ -22,7 +22,7 @@ from .chat_command import ChatCommand from ..msg_bus import Signal from ..loading_widget import BaseLoadingWidget -from ..logging import print_horizontal_line, printv, printvv +from ..logging import print_horizontal_line, printv, printvvv class FixCodeCommandResult(CommandResult): @@ -105,6 +105,8 @@ def print_raw_conversation() -> None: ) # End of handle kwargs + printv(f"Temperature: {temperature}") + verifier: BaseSourceVerifier = VerifierRunner().verifier match message_history: @@ -182,11 +184,11 @@ def print_raw_conversation() -> None: break # Print verbose lvl 2 - printvv("\nESBMC-AI Notice: Source Code Generation:") - print_horizontal_line(2) - printvv(source_file.latest_content) - print_horizontal_line(2) - printvv("") + printvvv("\nESBMC-AI Notice: Source Code Generation:") + print_horizontal_line(3) + printvvv(source_file.latest_content) + print_horizontal_line(3) + printvvv("") # Pass to ESBMC, a workaround is used where the file is saved # to a temporary location since ESBMC needs it in file format. @@ -196,10 +198,10 @@ def print_raw_conversation() -> None: source_file.assign_verifier_output(verifier_result.output) # Print verbose lvl 2 - printvv("\nESBMC-AI Notice: ESBMC Output:") - print_horizontal_line(2) - printvv(source_file.latest_verifier_output) - print_horizontal_line(2) + printvvv("\nESBMC-AI Notice: ESBMC Output:") + print_horizontal_line(3) + printvvv(source_file.latest_verifier_output) + print_horizontal_line(3) # Solution found if verifier_result.return_code == 0: