Verified Commit 50c97f6f authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Further improve query results summary

parent 7e815027
Pipeline #625 passed with stages
in 2 minutes and 8 seconds
......@@ -113,7 +113,7 @@ func infoVerifyResultSummary(
}
if len(optionsSummary) == 0 {
optionsSummary = fmt.Sprintf(
"%s Furthermore, the following options are contradicted:\n",
"%s Furthermore, the following query options fail:\n",
" ",
)
}
......@@ -259,7 +259,11 @@ func infoQueryMutatedValues(
pn[2] = aurora.BrightYellow(pa).Italic().Underline().String()
pn[3] = aurora.Red("← obtained by Attacker").Italic().String()
} else if valPrincipalState.Mutated[i] {
pn[3] = aurora.Red("← mutated by Attacker").Italic().String()
pn[3] = aurora.Red(
fmt.Sprintf("← mutated by Attacker (originally %s)",
prettyValue(valKnowledgeMap.Assigned[i]),
),
).Italic().String()
}
} else {
pn[0] = pc
......@@ -269,7 +273,9 @@ func infoQueryMutatedValues(
if isTargetValue && !valPrincipalState.Mutated[i] {
pn[3] = "← obtained by Attacker"
} else if valPrincipalState.Mutated[i] {
pn[3] = "← mutated by Attacker"
pn[3] = fmt.Sprintf("← mutated by Attacker (originally %s)",
prettyValue(valKnowledgeMap.Assigned[i]),
)
}
}
mutatedInfo = fmt.Sprintf("%s\n %s%s%s %s",
......
......@@ -341,7 +341,7 @@ func queryPrecondition(
if sender == option.Message.Sender && recipientKnows {
oResult.Resolved = true
oResult.Summary = fmt.Sprintf(
"%s sends %s to %s despite the query being contradicted.",
"%s sends %s to %s despite the query failing.",
option.Message.Sender,
prettyConstant(option.Message.Constants[0]),
option.Message.Recipient,
......
......@@ -153,19 +153,28 @@ func verifyGetResultsCode(valVerifyResults []VerifyResult) string {
func verifyEnd(m Model) ([]VerifyResult, string, error) {
var err error
valVerifyResults, fileName := verifyResultsGetRead()
completed := time.Now().Format("03:04:05 PM")
noResolved := true
for _, verifyResult := range valVerifyResults {
if verifyResult.Resolved {
noResolved = false
break
}
}
fmt.Fprint(os.Stdout, "\n\n")
InfoMessage(fmt.Sprintf(
"Verification completed for '%s' at %s.", fileName, completed,
"Verification completed for '%s' at %s.",
fileName, time.Now().Format("03:04:05 PM"),
), "verifpal", false)
InfoMessage("Summary of contradicted queries, if any, will follow.", "verifpal", false)
if noResolved {
InfoMessage("All queries pass.", "verifpal", false)
} else {
InfoMessage("Summary of failed queries will follow.", "verifpal", false)
}
fmt.Fprint(os.Stdout, "\n")
for _, verifyResult := range valVerifyResults {
if verifyResult.Resolved {
InfoMessage(fmt.Sprintf(
"%s — %s",
prettyQuery(verifyResult.Query),
verifyResult.Summary,
InfoMessage(fmt.Sprintf("%s — %s",
prettyQuery(verifyResult.Query), verifyResult.Summary,
), "result", false)
}
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment