Class RequirePredicateReader
require preconditions — use this, do not re-derive one.
A require is a declared boundary predicate: it states, on the callable's own
surface, which arguments the contract admits. That makes it usable by anything reasoning about a
callable's inputs without reading its body — the symbolic engine discharging an obligation
across a call, and equally a test-data generator deciding which values it may legitimately pass.
Both need the same extraction, so it lives here rather than in either of them.
🔑 Driven by a parse CONTEXT, never by name. The caller supplies the construct's own
subtree and its call parameters, so this works for a function, method, constructor, operator or
dynamic function alike — none of the by-name relocation that limits other parts of the symbolic
layer to FunctionSymbol.
Only the simple decidable shape is modelled, matching FunctionSummary: one parameter
compared against an integer literal. Anything compound or opaque is omitted, never
guessed — an omitted precondition costs a redundant test, whereas an invented one silently
deletes a case.
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionstatic LongTHE integer-literal reader for a relational operand, shared withSymbolicEngine's division, guard and constraint paths.static StringnormaliseOperator(String glyph) THE normalisation of a relational operator glyph, shared by every analysis that reads one — require preconditions here, andSymbolicEngine's guard and constraint paths.read(org.antlr.v4.runtime.tree.ParseTree constructCtx, List<ISymbol> callParameters, ParsedModule module) Read every modellablerequireprecondition inconstructCtx.
-
Constructor Details
-
RequirePredicateReader
public RequirePredicateReader()
-
-
Method Details
-
read
public List<FunctionSummary.RequirePredicate> read(org.antlr.v4.runtime.tree.ParseTree constructCtx, List<ISymbol> callParameters, ParsedModule module) Read every modellablerequireprecondition inconstructCtx.- Parameters:
constructCtx- the construct's parse subtree — its body is walked for require statementscallParameters- the construct's parameters, in declaration order, for index mappingmodule- the parsed module, to resolve the compared symbol- Returns:
- the preconditions found, possibly empty; never null
-
normaliseOperator
THE normalisation of a relational operator glyph, shared by every analysis that reads one — require preconditions here, andSymbolicEngine's guard and constraint paths.- Parameters:
glyph- the operator's source text- Returns:
- the normalised operator, or null when it is not a modelled relational comparison
-
literalLongOf
THE integer-literal reader for a relational operand, shared withSymbolicEngine's division, guard and constraint paths. Underscore digit separators are stripped.- Parameters:
expr- the operand expression- Returns:
- the literal value, or null when the operand is not an integer literal
-