Skip to content

Commit

Permalink
checker improvement
Browse files Browse the repository at this point in the history
  • Loading branch information
adharshkamath committed Dec 29, 2023
1 parent 84b36bd commit 30912a6
Showing 1 changed file with 29 additions and 28 deletions.
57 changes: 29 additions & 28 deletions src/frama_c.py
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,7 @@ def houdini(
input_code = "\n".join(code_lines)
code_queue.append(input_code)

elif use_json_dump_for_invariants:
else:
non_inductive_invariant_line_nos = (
self.get_non_inductive_invariant_line_nos(
checker_message, input_code
Expand All @@ -330,33 +330,34 @@ def houdini(
code_lines[line_no] = ""
code_queue.append("\n".join(code_lines))

else:
# What about TIMEOUT?
# If any invariant causes a Timeout, it's marked as "Unknown"
# because the prover could not prove it. So removing it.
unknown_inv_lines = self.get_unknown_inv_no_from_error_msg(
checker_message
)
if len(unknown_inv_lines) > 0:
for line_no in unknown_inv_lines:
code_lines[line_no] = ""
code_queue.append("\n".join(code_lines))
else:
# Push code with one "Partially proven" invariant removed to the queue
partially_proven_inv_line_nos = (
self.get_partially_proven_inv_from_error_msg(checker_message)
)
if self.get_invariants_count(input_code) == len(
partially_proven_inv_line_nos
):
# If all invariants are partially proven, then we can't afford
# to prune further. example, there's an assertion inside the loop which is Unknown
break

# for line_no in partially_proven_inv_line_nos:
# code_lines__ = deepcopy(code_lines)
# code_lines__[line_no] = ""
# code_queue.append("\n".join(code_lines__))
# This section would be used if we want to use the CSV dump instead of the JSON report
# else:
# # What about TIMEOUT?
# # If any invariant causes a Timeout, it's marked as "Unknown"
# # because the prover could not prove it. So removing it.
# unknown_inv_lines = self.get_unknown_inv_no_from_error_msg(
# checker_message
# )
# if len(unknown_inv_lines) > 0:
# for line_no in unknown_inv_lines:
# code_lines[line_no] = ""
# code_queue.append("\n".join(code_lines))
# else:
# # Push code with one "Partially proven" invariant removed to the queue
# partially_proven_inv_line_nos = (
# self.get_partially_proven_inv_from_error_msg(checker_message)
# )
# if self.get_invariants_count(input_code) == len(
# partially_proven_inv_line_nos
# ):
# # If all invariants are partially proven, then we can't afford
# # to prune further. example, there's an assertion inside the loop which is Unknown
# break

# # for line_no in partially_proven_inv_line_nos:
# # code_lines__ = deepcopy(code_lines)
# # code_lines__[line_no] = ""
# # code_queue.append("\n".join(code_lines__))

num_frama_c_calls += 1

Expand Down

0 comments on commit 30912a6

Please sign in to comment.