lang: funcs: core: fmt: Add more invariants to printf

These don't seem to change the number of passing tests, but add them in
case we hit some situation that benefits from them.
This commit is contained in:
James Shubin
2023-08-29 19:28:00 -04:00
parent 45e126bf07
commit 0b972c5b4b

View File

@@ -116,6 +116,12 @@ func (obj *PrintfFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant, erro
}
invariants = append(invariants, invar)
invar = &interfaces.EqualityInvariant{
Expr1: dummyFormat,
Expr2: dummyOut,
}
invariants = append(invariants, invar)
// dynamic generator function for when the format string is dynamic
dynamicFn := func(fnInvariants []interfaces.Invariant, solved map[interfaces.Expr]*types.Type) ([]interfaces.Invariant, error) {
for _, invariant := range fnInvariants {
@@ -137,6 +143,13 @@ func (obj *PrintfFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant, erro
var invariants []interfaces.Invariant
var invar interfaces.Invariant
// add the relationship to the format string arg
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Expr,
Expr2: dummyFormat,
}
invariants = append(invariants, invar)
// add the relationship to the returned value
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Expr,
@@ -227,6 +240,13 @@ func (obj *PrintfFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant, erro
var invariants []interfaces.Invariant
var invar interfaces.Invariant
// add the relationship to the format string arg
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Expr,
Expr2: dummyFormat,
}
invariants = append(invariants, invar)
// add the relationship to the returned value
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Expr,