Skip to content

Report One Error Per Path, Recover From Pure Assertions#575

Merged
mschwerhoff merged 79 commits into
viperproject:masterfrom
tschoesi:final_merge_with_upstream
Sep 9, 2021
Merged

Report One Error Per Path, Recover From Pure Assertions#575
mschwerhoff merged 79 commits into
viperproject:masterfrom
tschoesi:final_merge_with_upstream

Conversation

@tschoesi

@tschoesi tschoesi commented Sep 5, 2021

Copy link
Copy Markdown
Contributor

This PR contains the following changes

  • Report one error per path
  • Recover from pure assertion
  • Enable reporting of branch conditions
  • Specify number of errors after which Silicon stops

Silver PR 538 needs to be merged for those changes as well.

tschoesi and others added 30 commits May 2, 2021 23:15
(TODO: fix state consolidation for magic wands)
(TODO: fix state consolidation for magic wands)
(TODO: fix state consolidation for magic wands)
…i/silicon into feature/report_branch_conditions
…i/silicon into feature/recover_from_failed_pure
also:
 * some cosmetic changes
 * usage of util "BigAnd" instead of reduce
 * use ast.Exp to avoid confusion
tschoesi and others added 26 commits July 4, 2021 20:36
…h_master

# Conflicts:
#	src/main/scala/rules/Consumer.scala
#	src/main/scala/rules/Evaluator.scala
#	src/main/scala/rules/Executor.scala
#	src/main/scala/rules/Joiner.scala
#	src/main/scala/rules/Producer.scala
#	src/main/scala/rules/SymbolicExecutionRules.scala
programs with multiple members might report too many errors
some cosmetic changes
logic fix
…upstream

# Conflicts:
#	src/main/scala/rules/Executor.scala
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants