Entry point for bounds checking.
(pred ast.PredicateSym)
| 1047 | |
| 1048 | // Entry point for bounds checking. |
| 1049 | func (bc *BoundsAnalyzer) inferAndCheckBounds(pred ast.PredicateSym) error { |
| 1050 | decl, ok := bc.programInfo.Decls[pred] |
| 1051 | if !ok { |
| 1052 | return nil // This should not happen. |
| 1053 | } |
| 1054 | if !decl.IsSynthetic() { |
| 1055 | return bc.checkClauses(decl) |
| 1056 | } |
| 1057 | _, err := bc.inferRelTypes(pred) |
| 1058 | return err |
| 1059 | } |
| 1060 | |
| 1061 | // checkRelTypes takes a pred that has a declaration supplied by the user. |
| 1062 | // It checks every clause, including unit clauses ("initial facts"). |
no test coverage detected