Commit 7336b7bc authored by Nadim Kobeissi's avatar Nadim Kobeissi 💾
Browse files

Fix crash on undefined constant in auth. query

As reported by Friedrich Wiemer:
https://lists.symbolic.software/pipermail/verifpal/2020/000319.html
parent c268c773
Pipeline #718 passed with stages
in 3 minutes and 4 seconds
......@@ -222,6 +222,14 @@ func sanityQueriesConfidentiality(query Query, valKnowledgeMap KnowledgeMap) err
}
func sanityQueriesAuthentication(query Query, valKnowledgeMap KnowledgeMap) error {
i := valueGetKnowledgeMapIndexFromConstant(valKnowledgeMap, query.Message.Constants[0])
if i < 0 {
return fmt.Errorf(
"authentication query (%s) refers to unknown constant (%s)",
prettyQuery(query),
prettyConstant(query.Message.Constants[0]),
)
}
if len(query.Message.Constants) != 1 {
return fmt.Errorf(
"authentication query (%s) has more than one constant",
......@@ -255,7 +263,7 @@ func sanityQueriesUnlinkability(query Query, valKnowledgeMap KnowledgeMap) error
i := valueGetKnowledgeMapIndexFromConstant(valKnowledgeMap, c)
if i < 0 {
return fmt.Errorf(
"unlinkability query (%s) refers to unknown value (%s)",
"unlinkability query (%s) refers to unknown constant (%s)",
prettyQuery(query),
prettyConstant(c),
)
......
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