Skip to content

Commit

Permalink
Updated printing
Browse files Browse the repository at this point in the history
  • Loading branch information
Yiannis128 committed Dec 9, 2024
1 parent 832d72d commit 5778aed
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 17 deletions.
2 changes: 1 addition & 1 deletion config.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ name = "esbmc"
path = "~/.local/bin/esbmc"
params = [
"--interval-analysis",
"--memory-leak-check",
"--goto-unwind",
"--unlimited-goto-unwind",
"--k-induction",
Expand All @@ -21,7 +22,6 @@ params = [
"2",
"--floatbv",
"--unlimited-k-steps",
"--compact-trace",
"--context-bound",
"2",
]
Expand Down
2 changes: 1 addition & 1 deletion esbmc_ai/__about__.py
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Author: Yiannis Charalambous

__version__ = "v0.6.0.dev1"
__version__ = "v0.6.0.dev2"
__author__: str = "Yiannis Charalambous"
8 changes: 3 additions & 5 deletions esbmc_ai/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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")
Expand Down
22 changes: 12 additions & 10 deletions esbmc_ai/commands/fix_code_command.py
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand Down Expand Up @@ -105,6 +105,8 @@ def print_raw_conversation() -> None:
)
# End of handle kwargs

printv(f"Temperature: {temperature}")

verifier: BaseSourceVerifier = VerifierRunner().verifier

match message_history:
Expand Down Expand Up @@ -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.
Expand All @@ -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:
Expand Down

0 comments on commit 5778aed

Please sign in to comment.